Many-sorted logic

When reasoning about biological organisms, it is useful to distinguish two sorts: ${\displaystyle \mathrm {plant} }$ and ${\displaystyle \mathrm {animal} }$. While a function ${\displaystyle \mathrm {mother} \colon \mathrm {animal} \to \mathrm {animal} }$ makes sense, a similar function ${\displaystyle \mathrm {mother} \colon \mathrm {plant} \to \mathrm {plant} }$ usually does not. Many-sorted logic allows one to have terms like ${\displaystyle \mathrm {mother} (\mathrm {lassie} )}$, but to discard terms like ${\displaystyle \mathrm {mother} (\mathrm {my\_favorite\_oak} )}$ as syntactically ill-formed.

The algebraization of many-sorted logic is explained in an article by Caleiro and Gonçalves,[1] which generalizes abstract algebraic logic to the many-sorted case, but can also be used as introductory material.

While many-sorted logic requires two distinct sorts to have disjoint universe sets, order-sorted logic allows one sort ${\displaystyle s_{1}}$ to be declared a subsort of another sort ${\displaystyle s_{2}}$, usually by writing ${\displaystyle s_{1}\subseteq s_{2}}$ or similar syntax. In the above example, it is desirable to declare

${\displaystyle {\textit {dog}}\subseteq {\textit {carnivore}}}$,

${\displaystyle {\textit {dog}}\subseteq {\textit {mammal}}}$,

${\displaystyle {\textit {carnivore}}\subseteq {\textit {animal}}}$,

${\displaystyle {\textit {mammal}}\subseteq {\textit {animal}}}$,

${\displaystyle {\textit {animal}}\subseteq {\textit {organism}}}$,

${\displaystyle {\textit {plant}}\subseteq {\textit {organism}}}$,

and so on.

Wherever a term of some sort ${\displaystyle s}$ is required, a term of any subsort of ${\displaystyle s}$ may be supplied instead (Liskov substitution principle). For example, assuming a function declaration ${\displaystyle {\textit {mother}}:{\textit {animal}}\longrightarrow {\textit {animal}}}$, and a constant declaration ${\displaystyle {\textit {lassie}}:{\textit {dog}}}$, the term ${\displaystyle {\textit {mother}}({\textit {lassie}})}$ is perfectly valid and has the sort ${\displaystyle {\textit {animal}}}$. In order to supply the information that the mother of a dog is a dog in turn, another declaration ${\displaystyle {\textit {mother}}:{\textit {dog}}\longrightarrow {\textit {dog}}}$ may be issued; this is called function overloading, similar to overloading in programming languages.

Order-sorted logic can be translated into unsorted logic, using a unary predicate ${\displaystyle p_{i}(x)}$ for each sort ${\displaystyle s_{i}}$, and an axiom ${\displaystyle \forall x(p_{i}(x)\rightarrow p_{j}(x))}$ for each subsort declaration ${\displaystyle s_{i}\subseteq s_{j}}$. The reverse approach was successful in automated theorem proving: in 1985, Christoph Walther could solve a then benchmark problem by translating it into order-sorted logic, thereby boiling it down an order of magnitude, as many unary predicates turned into sorts.[2]

In order to incorporate order-sorted logic into a clause-based automated theorem prover, a corresponding order-sorted unification algorithm is necessary, which requires for any two declared sorts ${\displaystyle s_{1},s_{2}}$ their intersection ${\displaystyle s_{1}\cap s_{2}}$ to be declared, too: if ${\displaystyle x_{1}}$ and ${\displaystyle x_{2}}$ are variables of sort ${\displaystyle s_{1}}$ and ${\displaystyle s_{2}}$, respectively, the equation ${\displaystyle x_{1}{\stackrel {?}{=}}\,x_{2}}$ has the solution ${\displaystyle \{x_{1}=x,\;x_{2}=x\}}$, where ${\displaystyle x:s_{1}\cap s_{2}}$.

Smolka generalized order-sorted logic to allow for parametric polymorphism.[3][4] In his framework, subsort declarations are propagated to complex type expressions. As a programming example, a parametric sort ${\displaystyle {\textit {list}}(X)}$ may be declared (with ${\displaystyle X}$ being a type parameter as in a C++ template), and from a subsort declaration ${\displaystyle {\textit {int}}\subseteq {\textit {float}}}$ the relation ${\displaystyle {\textit {list}}({\textit {int}})\subseteq {\textit {list}}({\textit {float}})}$ is automatically inferred, meaning that each list of integers is also a list of floats.

Schmidt-Schauß generalized order-sorted logic to allow for term declarations.[5] As an example, assuming subsort declarations ${\displaystyle {\textit {even}}\subseteq {\textit {int}}}$ and ${\displaystyle {\textit {odd}}\subseteq {\textit {int}}}$, a term declaration like ${\displaystyle \forall i:{\textit {int}}.\;(i+i):{\textit {even}}}$ allows to declare a property of integer addition that could not be expressed by ordinary overloading.

• Categorical logic
• Many-sorted first-order logic#Many-sorted logic

Early papers on many-sorted logic include:

• Wang, Hao (1952). "Logic of many-sorted theories". Journal of Symbolic Logic. 17: 105–116. doi:10.2307/2266241., collected in the author's Computation, Logic, Philosophy. A Collection of Essays, Beijing: Science Press; Dordrecht: Kluwer Academic, 1990.
• Gilmore, P.C. (1958). "An addition to "Logic of many-sorted theories"" (PDF). Compositio Mathematica. 13: 277–281.
• A. Oberschelp (1962). "Untersuchungen zur mehrsortigen Quantorenlogik". Mathematische Annalen. 145 (4): 297–333. doi:10.1007/bf01396685. Archived from the original on 2015-02-20. Retrieved 2013-09-11.
• F. Jeffry Pelletier (1972). "Sortal Quantification and Restricted Quantification" (PDF). Philosophical Studies. 23: 400–404. doi:10.1007/bf00355532.

• "Many-sorted Logic", the first chapter in Lecture Notes on Decision Procedures by Calogero G. Zarba