Inclusions and subtypes I: First-order case

The failure to make explicit two different notions of subtype, a subtype as inclusion notion originally proposed by Goguen and a subtype as implicit conversion notion originally proposed by Reynolds, leads to unsatisfactory situations in present approaches to subtyping. Here, it is argued that choosing either notion at the expense of the other would be mistaken and limiting, and a framework is proposed in which two subtype relations τ ≤ τ' (inclusion) and τ ≤: τ' (implicit conversion) are distinguished and integrated. Part I generalizes the first-order equational logic with subtypes as inclusions and overloaded function symbols from its usual set-theoretic semantics to a categorical semantics in the style of Lawvere. This provides a much more general notion of model and supports interpretations of a logic with subtypes in any category having a suitable canonical notion of subobject. Soundness and completeness of the logic in the categorical setting are proved, and the classifying category of a theory, which is the initial model in this context, is constructed in detail. The adjunction between theory presentations and model categories is also proved, shedding light on subtleties of operation overloading not present in the unsorted and many-sorted cases. All this sets the stage for the higher-order categorical semantics of subtypes developed in Part II.