Many-Sorted Logic

1. Syntax and Semantics

1.1 Examples

We start with a few examples to illustrate how common statements concerning different types of data can be formalized in many-sorted first-order logic.

Let us begin with geometry, by talking about straight lines and points. According to Euclid’s first principle:

A straight line can be drawn joining any two points.

In two sorted first-order logic one can use \(X,\) \(Y,\)… as variables for sort \(l\) (straight lines) and \(x,\) \(y,\)… as variables for sort \(p\) (points). To formulate Euclid’s principle we write:

In this example, \(\Join\) is a 3-place predicate symbol relating a straight line and two points,

Literally our formalization reads: “For any two points there is a unique straight line joining them”.

Another mathematical example is about asymmetry and anti-symmetry, both of which are properties of some binary relations. Suppose we wanted to express the claim:

Every asymmetric binary relation is also anti-symmetric.

To formalize the statement as a single logically valid sentence we need: (1) to express asymmetry and anti-symmetry, and (2) to quantify over binary relations. In a suitable first-order language including \(R\) as a binary relation symbol, to express that \(R\) is asymmetric we write:

and to say that \(R\) is anti-symmetric we write:

In ordinary one-sorted first-order logic, this would be a logically valid scheme:

What we get is an infinite set of formulas obtained by replacing \(R\) by any other binary relation symbol. However, we wanted a single logically valid sentence and so we need to quantify over binary relations. In second-order logic, taking \(X^{2},\) \(Y^{2},\)… as variables for binary relations we write:

But since standard second-order logic lacks some of the nice properties of first-order logic (section 4.1), one could instead go for a two-sorted first-order logic, in which both individuals and relations between individuals are first-class citizens one can quantify over. We would have variables \(x,\) \(y,\ldots\) of sort \(i\) (individuals), and \(X^{2},\) \(Y^{2},\ldots\) of sort \(r\) (binary relations between individuals). However, it is not enough to label our variables as individuals or binary relations, we need them to perform as second-order variables do. A three-place predicate symbol relating binary relations and individuals, \(\epsilon_{2} xyX^{2}\), needs to be added so that \(\Asymm(X^{2})\) becomes:

and similarly for \(\Antisymm(X^{2})\).

As we will see in section 4.2, rewriting the second order formula \(X^{2}xy\) as \(\epsilon_{2}xyX^{2}\) is all we do when translating second-order logic into many-sorted logic; some axioms for predicates \(\epsilon _{n}\) are added and a suitable many-sorted theory for the \(\epsilon _{n}\) relations is introduced. In many-sorted logic formula

is a theorem of the many-sorted theory mentioned.

Let us introduce another, more philosophical, example. If we wanted to formalize:

Every property has a negation.

we could use second order logic and write:

That becomes a many-sorted formula when we rewrite it as:

using \(x,y,\ldots\) as variables of sort \(i\) (individuals) and \(X,Y,\ldots\) of sort \(\pi\) (properties).

Formula \(\forall X\,\exists Y\,\forall x(Yx\leftrightarrow \lnot Xx)\) is a generalization of an instance of Comprehension Scheme

(variable \(Y^{n}\) is not free at \(\varphi\)). Section 4 and section 5 discuss the role played by this scheme in translation from second-order logic into many-sorted first-order logic.

As you will see in section 6.1, each many-sorted formula has a version in a one-sorted first-order language obtained by removing sorts. In this new language all the variables belong to one sort, but we add unary predicates to recover the lost information when passing from the many-sorted expression to the one-sorted one. We also need to guarantee that these new predicates, which represent the lost universes of quantification, are interpreted by non-empty sets, since universes of quantification are non-empty in classical logic.

In Euclid’s example, we add axioms \(\exists xLx\) and \(\exists xPx\) and formula

now becomes

To represent Every property has a negation in one-sorted first-order logic we use \(x,y,z,\ldots\) as variables for the unique sort we now have, and write:

where

Some axioms for predicates \(\epsilon _{1}\) are added, as well as axioms saying that predicates \(P\) and \(O\) are never interpreted as empty sets, \(\exists xOx\) and \(\exists xPx\). Moreover, the links between predicates \(\epsilon _{1}\), \(P\) and \(O\) are expressed by:

1.2 Fundamental Ideas

To specify the syntax of a many-sorted language and associated structures we need first to say what our (countable) set of sorts is. We take \(\Sort=\{ s_{1},\dots ,s_{n}\}\) as the sorts of an n-sorted language.[1]

In Euclid’s example we have two sorts, \(l\) (lines) and \(p\) (points) and a 3-place predicate \(\Join\) with \(\Rank(\Join)=\langle l,p,p,0\rangle\). In the example of binary relations we have two sorts, \(i\) (individuals) and \(r\) (binary relations) and a 3-place predicate symbol \(\epsilon _{2}\) with \(\Rank(\epsilon_{2})=\langle i,i,r,0\rangle\). For the comprehension example we have two sorts, \(i\) (individuals) and \(\pi\) (properties) and a 2-place predicate symbol \(\epsilon_{1}\) with \(\Rank(\epsilon_{1})=\langle i,\pi ,0\rangle\).

1.3 Formal Language

As we do in classical first-order logic, from the set of finite strings of elements of the alphabet we select the expressions of \(L\): terms and formulas. The only difference is that in many-sorted logic terms have sorts and we have to specify it.

In consequence, the terms of many-sorted logic are defined recursively as follows: Each variable or individual constant of sort \(s_{i}\) is a term of the same sort \(s_{i}\). If \(f\in \OperSym\) is such that \(\Rank(f)=\langle i_{1},\ldots,i_{m},i_{0}\rangle\) with \(i_{0}\not=0\) and \(\tau _{1},\ldots,\tau _{m}\) are terms of sorts \(i_{1},\ldots,i_{m}\), then \(f\ \tau _{1}\ldots\tau _{m}\) is a term of sort \(i_{0}\).

Atomic formulas are defined by means of predicates and terms: If \(R\in \OperSym\) is such that \(\Rank(R)=\langle i_{1},\ldots ,i_{m},0\rangle\), and \(\tau _{1},\ldots \),\(\tau _{m}\) are terms of sorts \(i_{1},\ldots,\) \(i_{m}\), then \(R\tau _{1}\ldots \tau _{m}\) is a formula (when \(R\) is a liberal predicate, we drop the sort requirement for terms). For any terms \(\tau _{1}\ \)and \(\tau _{2}\), the expression \(\tau _{1}\approx \tau _{2}\) is a formula. Notice that the sorts of \(\tau _{1}\ \)and \(\tau _{2}\) do not matter, because our choice of equality symbol is the liberal one.[3]

Complex well-formed formulas (wffs) are defined as usual in first-order languages (see the entry on classical logic), except for quantified expressions. The new rule says: If \(\varphi\) is a formula and \(x^{i}\) is a variable of sort \(i\), then \(\exists x^{i}\varphi\) is a formula as well.

As in classical first-order logic, occurrences of variables in a formula can be free or bound; they are bound when they are under the scope of a quantifier, otherwise free. A variable is free in a formula if it has at least one free occurrence therein. A formula with no free variables is called a sentence. We use \(Sent(L)\) to denote the set of sentences of language \(L\).

Consider the following, from Liezi (Book 5, 1–2):

In order to analyze this example, we should identify premises and conclusion; and we easily observe that the initial rhetorical question is in fact the argument’s conclusion. The considered argument is an enthymeme, for the reason that it seems to be supported in the permanence of the laws that govern the cosmos (in particular, those concerning the existence of objects). The hidden hypothesis supporting the argument could be the following law:

If things exist at a given point in time, then at any given previous moment in time things must have existed.

This rule is not saying that existence of a particular object is eternal, it is saying that the chain of existence goes back forever.

Thus, the argument can be reformulated in the following way, where \(\alpha ,\) \(\beta\) and \(\gamma\) are the premises and \(\delta\) is the conclusion:

Now, the premises and the conclusion can be formalized by means of a two sorted language, \(\Sort=\{ i,\tau \}\), including objects (sort \(i\)) and instants of time (sort \(\tau\)). The set \(\OperSym\) contains a binary predicate of existence at a given time, \(E\), another binary predicate of precedence between instants, \(P\), and two individual constants for today (\(t\)) and the dawn of times \((d)\). So, in this case,

The argument now reads:

In many sorted logic, the conclusion is easily obtained from these hypotheses by using a deductive calculus (see section 2). Therefore, the argument is formally correct, once we accept the problematic hypothesis \(\alpha\). In section 2.4 we rewrite the argument to use theorem provers LEO-II and LEO-III.

1.4 Many-sorted Structures

The semantics of many-sorted logic is rather similar to that of classical first-order logic, because it follows Tarski’s truth definition to introduce the concept of truth in a structure (see Tarski 1933 and Tarski & Vaught 1956; for historical clarifications, see Hodges 1986 and the entry on Tarski’s truth definitions). In our case, the object language is many-sorted logic and the metalanguage is set theory. Set theory is the commonly used metalanguage, where relation symbols are interpreted as relations defined over universes (sets) of mathematical structures.

In many-sorted first-order logic, a structure is understood as a tuple having a family of non-empty sets as domains and a family of operations (functions and relations) defined over these domains. These relations and functions are defined according to a given signature.

A many-sorted Σ-structure \(\mathcal{A}\) has several universes (or domains) of objects in a family of non-empty sets \(\mathbf{A}_{i}\) (for each \(i\in Sort\)). Structure \(\mathcal{A}\) contains as well: an m-ary relation \(R^{\mathcal{A}}\) for each relation symbol \(R\), an n-ary function \(f^{\mathcal{A}}\) for every n-ary function symbol \(f\) and a distinguish element \(c^{\mathcal{A}}\in \mathbf{A}_{i}\) for every individual constant \(c\). These relations and functions have to be established between elements of the family of domains taking into account their values under function \(\Rank\).[4]

Using structure \(\mathcal{A}\) we define in section 1.5 the truth of a sentence \(\varphi\) in this structure, noted as \(\mathcal{A}\models \varphi\).

We could add the requirement of empty intersection between different domains. Structures obeying this requirement are called “strict”, otherwise “lax” (or “liberal”). For strict structures we may consider the possibility of having an equality symbol for each sort, \(\approx _{i}\), each of them with \(\Rank(\approx _{i})=\langle i,i,0\rangle\). We require equality symbols (either strict or liberal) to be interpreted as genuine identity, the prototypical relation that holds between an object and itself and fails to hold between any two other objects.

For one-sorted structures, it is very common to study different relations between them: homomorphisms, embeddings, isomorphisms, substructures and extensions (see Manzano 1989 [1999: 19–33]). One can define these relations for many-sorted structures in a similar vein. An homomorphism between two structures \(\mathcal{A}\) and \(\mathcal{A}^{\prime }\) with the same signature is a function \(\pi\) from the union of the universes of \(\mathcal{A}\) to the union of the universes of \(\mathcal{A}^{\prime }\) satisfying the following conditions: Firstly, the restriction of \(\pi\) to \(\mathbf{A}_{i}\) must be a function from \(\mathbf{A}_{i}\) to \(\mathbf{A}_{i}^{\prime }\), for each \(i\in Sort\). Secondly, if the n-tuple of elements \(\langle \mathbf{a}_{i},\dots ,\mathbf{a}_{n}\rangle\) is in the n-ary relation \(R^{\mathcal{A}}\) then \(\langle \pi (\mathbf{a}_{i}),\dots ,\pi (\mathbf{a}_{n})\rangle\) is in the relation \(R^{\mathcal{A}^{\prime }}\). Finally,

and \(\pi (c_{i}^{\mathcal{A}})=c_{i}^{\mathcal{A}^{\prime }}\).

An embedding is a homomorphism where the involved functions are injective and the second condition works in both directions. An isomorphism is an embedding where the defining maps are bijections. When the function \(\pi\) is an isomorphism one says that \(\mathcal{A}\) and \(\mathcal{A}^{\prime }\) are isomorphic and writes \(\mathcal{A}\cong \mathcal{A}^{\prime }\).

We say that \(\mathcal{A}^{\prime }\) is a substructure of \(\mathcal{A}\) (equivalently, \(\mathcal{A}\) is an extension of \(\mathcal{A}^{\prime }\)) if and only if the inclusion map \(i\) (sending every element to itself) is an embedding from \(\mathcal{A}^{\prime }\) to \(\mathcal{A}\).

All the relationships already mentioned are established between structures of the same signature. We can as well define reductions and expansions between structures whose signatures are not the same. Given a many-sorted structure \(\mathcal{A}\), a reduct \(\mathcal{A}^{\prime }\) of \(\mathcal{A}\) is obtained by simply removing some sorts, function or relation symbols from the signature of \(\mathcal{A}\). If \(\mathcal{A}^{\prime }\) is a reduct of \(\mathcal{A}\), then we say that \(\mathcal{A}\) is an expansion of \(\mathcal{A}^{\prime}\).

1.5 Semantics

Given a language and a structure, both of them sharing the same signature, each closed term of the language will denote an element in the structure and each atomic sentence is either true or false in the structure. Nevertheless, the scope of our definition is widened so that each term will receive a denotation and each formula a truth value. To achieve that, we define assignments[5] from the set of variables to the domains of the structure, arguments and values should be of the same sort. For any individual \(\mathbf{x}\in \mathbf{A}_{i}\) and variable \(x^{i}\) of sort \(i\), we use \(s(\mathbf{x}/x^{i})\) to denote the assignment which is like assignment \(s\) except that the value at \(x^{i}\) has to be \(\mathbf{x}\).

To define the important concept of “truth of a sentence \(\varphi\) in a structure \(\mathcal{A}\)” \((\mathcal{A}\models \varphi)\) we need to define previously the concept of satisfaction of a formula \(\varphi\) in \(\mathcal{A}\) under assignment \(s\) (noted as \(\mathcal{A},s\models \varphi\)), as well as the denotation of terms.

Let \(\mathcal{A}\) be an L-structure (language and structure sharing signature \(\Sigma\)) and \(s\) an assignment. \(\mathcal{I}=\langle \mathcal{A},s\rangle\) is called an interpretation. The recursive definition of denotation \(\mathcal{I}(\tau )\) of the term \(\tau\) under the interpretation \(\mathcal{I}\) is defined in the usual way, as in classical one-sorted first-order logic. For atomic and complex terms: \(\mathcal{I}(x^{i})=s(x^{i})\), \(\mathcal{I}(c)=c^{\mathcal{A}}\) and

It is easy to check that terms of a certain sort denote individuals of that sort.

In many-sorted logic the connectives are standard and, therefore, we use the classical definition of satisfaction for formulas built on them. For quantified formulas such as \(\exists x^{i}\varphi\) the definition reads: \(\mathcal{A},s\models \exists x^{i}\varphi\) if and only if there is an \(\mathbf{x}\in \mathbf{A}_{i}\) such that \(\mathcal{A},s(\mathbf{x}/x^{i})\models \varphi\).

As in classical first-order logic, the coincidence lemma holds (see the entry on classical logic): For any formula \(\varphi\) and assignments \(s_{1}\) and \(s_{2}\): if \(s_{1}\) and \(s_{2}\) agree on the free variables in \(\varphi\), then \(\mathcal{A},s_{1}\models \varphi\) if and only if \(\mathcal{A},s_{2}\models \varphi\).

For a formula \(\varphi (x_{1},\ldots ,x_{n})\) whose free variables are in \(\{ x_{1},\ldots ,x_{n}\}\) one can write

instead of

By applying the coincidence lemma, we can get rid of assignments when dealing with sentences, and so we just write \(\mathcal{A}\models \varphi\) (instead of \(\mathcal{A},s\models \varphi\)). In this case we usually say that \(\mathcal{A}\) is a model of \(\varphi\).

For a set of sentences \(\Gamma\) we say that \(\mathcal{A}\) is a model of \(\Gamma\) (for short \(\mathcal{A}\models \Gamma\)), when \(\mathcal{A}\) is a model of every sentence \(\gamma\) in \(\Gamma\). Structures and language share signature.

The abstract schema of semantics could be seen in this way: we have a language \(L\) and a class of mathematical structures, sharing a given signature \(\Sigma\). Between these mathematical realities we have just built a bridge, the notion of truth in a structure. In one direction, we circulate from sentences to structures where these sentences are true; on the other direction, we go from structures to sentences which are true in these structures. In the first case, from a set of sentences \(\Gamma\) of signature \(\Sigma\) we define \(\Mod(\Gamma )\) as the class of structures of signature \(\Sigma\) that are models of \(\Gamma\). In the second, from a structure \(\mathcal{A}\) of signature \(\Sigma\) we define \(\Th(\mathcal{A})\) (the theory of \(\mathcal{A}\) ), the infinite set of sentences which are true at structure \(\mathcal{A}\)

In the previous section, the relations between structures were defined without resorting to the many-sorted formal language. That is not the case for elementary embedding, another relationship between many-sorted structures of the same signature. An elementary embedding \(\pi\) between two Σ-structures \(\mathcal{A}\) and \(\mathcal{A}^{\prime }\) is an embedding satisfying:

for all Σ-formulas \(\mathcal{\varphi (}x_{1},\ldots \mathbf{,}x_{n})\) and elements \(\mathbf{x}_{1},\ldots ,\mathbf{x}_{n}\) in the domains of the structure, variables and elements with the same sorts.

Two structures \(\mathcal{A}\) and \(\mathcal{B}\) are elementarily equivalent if and only if their theories are the same, \(\Th(\mathcal{A})=\Th(\mathcal{B})\).

Concepts of satisfiability, validity and consequence are defined as in classical first-order logic. Given language \(L\) of signature \(\Sigma\) and a formula \(\varphi\) of \(L\): \(\varphi\) is satisfiable if and only if there exists a Σ-structure \(\mathcal{A}\) and assignment \(s\) on it such that \(\mathcal{A},s\models \varphi\) holds; \(\varphi\) is valid (\(\models \varphi\)) if and only if \(\mathcal{A},s\models \varphi\) holds for all \(\mathcal{A}\) of signature \(\Sigma\) and any assignment \(s\) on \(\mathcal{A}\).

Given a language \(L\) of a given signature \(\Sigma\) we define the consequence relation in this way: \(\Gamma \models \varphi\) if and only if for every structure \(\mathcal{A}\ \)(of signature \(\Sigma\) ) and assignment \(s\) such that \(\mathcal{A},s\models \gamma\) for all \(\gamma \in \Gamma\), we have that \(\mathcal{A},s\models \varphi\).

In case \(\Gamma\) and \(\varphi\) were sentences, \(\Gamma \models \varphi\) can be expressed in this way: \(\Mod(\Gamma )\subseteq \Mod(\varphi )\).

2. Calculus

2.1 Deductive Calculi

It is common in model theory to regard a logic as comprising at least three different things: a class of structures, a formal language to describe these structures, and a satisfaction relation that determines when a formula of the language is true with respect to a given structure. A deductive calculus might be added.

In fact, any calculus for one-sorted first-order logic can be easily extended to a many-sorted one; the only rules which need to be adapted are the ones dealing with quantifiers and substitution, as they have to take into consideration the variety of sorts admitted. In the entry classical logic the rules that need to be changed are: introduction and elimination of universal quantifier (\(\forall \mathbf{I}\) and \(\forall \mathbf{E}\)), introduction and elimination of existential quantifier (\(\exists \mathbf{I}\) and \(\exists \mathbf{E}\)) as well as the rules dealing with equality (\(=\mathbf{I}\) and \(=\mathbf{E}\)).

The sequent calculus presented in Manzano (1996: 240–257) is the many-sorted extension of the one in Ebbinghaus, Flum, and Thomas (1984). Hao Wang (1952: 106), one of the pioneering logicians working on many-sorted logic, already introduced an axiomatic calculus for this logic in his seminal work (see the supplement on early history for more information).

As usual, to symbolize derivability of a formula from a set of formulas we write, \(\Delta \vdash \varphi\). We will write the derivability sign \(\vdash\) with a subscript when needed; namely, \(\vdash _{\MSL}\). In any of these calculi the notion of proof is effective in the sense that there is a method by which whenever a finite sequence of sequents of formulas is given, it can always be effectively determined, whether it is a proof or not. Any of these calculi is undecidable, as there is not an algorithm to check if \(\vdash \varphi\) or not. In fact, it could not be otherwise as the satisfiability problem (i.e., determining validity, or equivalently, testing for satisfiability of given formulas) for many-sorted logic is undecidable. So, we are in the same situation encountered in one-sorted first-order logic.

Of course, if a calculus is to be helpful it would never allow erroneous reasonings: it is not going to drive us from true hypotheses to false conclusions. It must be a sound calculus. Further, it is highly desirable that all the consequences of a set \(\Gamma\) of hypotheses could be derived from \(\Gamma\). That is, we would like to have a strongly complete calculus. In our section 2.3 you will find the sketch of such a completeness proof.

Also standard are the definitions of the syntactic concepts;[7] namely those of consistency, maximal consistency and the property of having witnesses. In the present circumstance, a set of formulas contains witnesses if each existential formula comes with a witness (\(\exists x^{i}\varphi \in \Delta\) implies \(\varphi (t/x^{i})\in \Delta\) for a term \(t\) of sort \(i\)). All three are properties of formulas and/or sets of formulas and in their definition we use derivability; i.e., the deductive calculus.

Consistency can be seen as the syntactic counterpart of satisfiability, in the same sense as \(\vdash\) and \(\models\) would correspond to one another. In fact, Henkin’s completeness proof basically consists in the construction of a model for each consistent set.

2.2 Completeness Notions

Proof and truth are defined by independent methods and it is not trivial, but necessary, to prove that they are extensionally the same. This is the content of the completeness theorem when this property is predicated of a sound calculus. There is another meaning of completeness, when it is predicate of a theory: A theory \(\Gamma\) is complete when for each sentence, either \(\varphi\) or \(\lnot \varphi\) is a consequence of \(\Gamma\) (Manzano 1989 [1999: 118]). Strong completeness of a calculus establishes its sufficiency for capturing the logical consequence; namely, whenever a sentence follows logically from a set of hypotheses, there is a proof of this sentence in the calculus, possibly using some of these hypotheses. In contrast, weak completeness says that we have proofs for all validities. In a complete[8] logic, the expressive power of the language and its computational strength are well balanced. Thus the question about completeness is the question about the equilibrium of the basic components of a logic: its semantics and its logical calculus.

Sometimes, we merely say that a logic is complete and qualify this property as abstract completeness. In this case, we are only concerned with the computational characteristics of the set of logical truths (validities), all we need to know is that they are recursively enumerable.

Section 3 presents many-sorted logic as a unifier logic and we describe the three levels process of embedding into MSL as a path to completeness of the logic being studied: abstract completeness at the first level, strong completeness at the third.

2.3 Completeness of Many-sorted Logic

The completeness proof for a many-sorted calculus could be done by following the well known Henkin (1949) strategy for first-order logic. The important issue is to be able to show that each consistent set of formulas has a model, and hence syntactic consistency and semantic satisfiability are equivalent (assuming Soundness). The proof is performed in basically two steps:

By doing that we prove:

The completeness theorem

follows easily from it.

To see that Henkin’s theorem implies Strong completeness, let us assume the antecedent, \(\Gamma \models \varphi\). Therefore, \(\Gamma \cup \{ \lnot \varphi \}\) is not satisfiable, it has no model. Using Henkin’s theorem we conclude that \(\Gamma \cup \{ \lnot \varphi \}\) is contradictory and so \(\Gamma \cup \{ \lnot \varphi \} \vdash \varphi\). The calculus rules allow us to get rid of \(\lnot \varphi\) and infer \(\Gamma \vdash \varphi\).

As corollaries of the previous results one gets:

In Manzano (1996: 245–257), the completeness theorem is proved in its strong sense and for all formulas, not only for sentences. Completeness and its corollaries are proven by following the path introduced by Ebbinghaus, Flum, and Thomas (1984).

Is many-sorted logic a proper (or strict) extension of first-order logic? Lindström (1969) proves that first-order logic is characterizable as the strongest logic to possess simultaneously Compactness and Löwenheim-Skolem properties. Moreover, first-order logic is the strongest logic where Löwenheim-Skolem holds and its set of valid sentences is recursively enumerable. Therefore, many-sorted logic cannot be considered as a proper extension of first-order logic.

2.4 Automated Theorem Provers

Many-sorted logic provides a semantical concept of consequence as well as a deductive calculus to be used in the mathematical process of obtaining conclusions from hypotheses. Now the issue is to automate this reasoning process by building a computer program to conduct deductive inferences.

As we have already mentioned, soundness is the essential requirement of a calculus while completeness guarantees that all the semantical consequences can be established within the calculus and so the set of validities is recursively enumerable. The most relevant properties for automated deduction are decidability and complexity. A logic is decidable when there is an algorithm that answer YES or NO in a finite time to the question: is the formula \(\varphi\) valid? As validity and satisfiability are interdefinible (\(\models \varphi\) iff \(\lnot \varphi\) is not satisfiable) this problem is often called the satisfiability problem. Among the basic tasks a computer is asked for are satisfiability and model checking.

Propositional logic is decidable but first-order logic, many-sorted version included, is undecidable. However, in between propositional and first-order logic there are decidable logics, like monadic predicate logic (first-order logic whose predicates are all unary predicates), as well as decidable fragments[10] of the undecidable logic. Moreover, among the decidable problems there are degrees of time-space complexity measuring time and memory register used by the computer.

Therefore, in a theorem prover for many-sorted calculus there is no guarantee of getting an answer to the question: Does \(\Gamma \models \varphi\)? However, there are efficient theorem provers able to solve the problem in many cases; for instance, when there are decidable fragments to implement. See the entries on automated reasoning and Church’s type theory. Section 4 of the entry on Church’s type theory is devoted to automation and provides information about machine-oriented proof calculi as well as early proof assistants. An excellent selection of theorem provers for Church’s type theory are presented. Among them are LEO-II and LEO-III, the latter is said to “cooperate with first-order reasoning tools using translations to many-sorted logic”.

Church’s simple type theory usually starts with base types “i” (individuals/entities) and “o” (Booleans) only and then iteratively defines all function types (such as “\(\text{i} = > \text{o}\)”, “\(\text{i}=>\text{i}\)”, “\(\text{o}=>\text{o}\)”, “\(\text{i}=>(\text{i}=>\text{o})\)”, etc.) starting from those. But in fact one can have arbitrary many base types \(i_1\), \(i_2\), \(i_3\),…, \(i_n\) and apply an analogous construction. These base types \(i_1\), \(i_2\), \(i_3\),…, \(i_n\) can be considered as sorts.

Our example from the Book of Perfect Emptiness can be formalized and checked using the LEO-II and LEO-III provers.

3. Many-sorted Logic as a Unifying Framework

3.1 Translations

Currently, the proliferation of logical systems used in mathematics, computer science, philosophy, and linguistics makes the relationships between and their possible translations into one another a pressing issue. We saw above that many-sorted logic is a natural logic for reasoning about more than one sort of objects. In this section, we will present it as a unifying framework in which we may situate most of the many logics available to us. The general plan of translations into MSL is described with some details. Three possible levels of translations are settled and, at each level, when successfully reached, one completeness result is gained: abstract completeness at the first level, strong completeness at the third. Therefore, when a logic is translated into many-sorted logic we only need a unique deductive calculus, the many-sorted one, as well as an efficient theorem prover. In cases like basic propositional modal logic, where formulas could be translated into a decidable fragment of first-order logic with only two variables, the translation mechanism implies decidability for the modal logic. Moreover, some metaproperties of many-sorted logic can be transferred to the logic being translated.

Translations offer a better understanding of the logics being translated and could be used to compare two logics when they are transformed into theories of a common target logic, many-sorted first-order logic in our case. It is not a positive answer to the question “The One Right Logic?” (see the entry classical logic) as this question was not posed and it is not in the spirit of this translation into many-sorted logic. In Modal Logic for Open Minds (van Benthem 2010) translations into first-order logic are extensively treated and there is a section entitled “Discussion: what good is a translation” (2010: 77) where Johan van Benthem analyzes the balance of expressive power and complexity and advocates for a tandem approach to answer the question Does the translation ST mean that we can forget the modal language and just do first-order logic?

Translations between logics have been formulated as an ambitious paradigm whose tools would serve for handling the existing multiplicity of logics. Some methodologies are proof-oriented, others are model-oriented, and finally some others are conceived in purely abstract suprastructural terms.

The paradigm of logical translation[11] assumed in this entry belongs to the model-theoretical tradition mentioned in item 2 and the target logic is many-sorted logic.

As far as intensional logic is concerned, let us quote Johan van Benthem:

Given any intensional logic, a complete possible-worlds semantics of the usual variety may be viewed as a faithful embedding of that logic into some suitably augmented many-sorted predicate logic (with quantification over possible worlds), perhaps provided with some simple auxiliary special-purpose theory for “accessibility”, “reversal”, and so on. Is predicate logic universal in this respect, in that every effectively axiomatized intensional logic can be semanticized in this way? (1984b: 995)

3.2 Correspondence Language for Basic Modal Language

Among the so called “non-classical logics”, modal logic occupies the first position as its history goes back to Aristotle, as well as Megarians, Stoics, and other Greek philosophers. Over the years it has been used to talk about necessity and possibility, time, and computer programs. See the entry on modal logic as well as Blackburn and van Benthem (2007) and van Benthem (2010).

The features of modal logic most relevant to this entry on many-sorted logic are that truth can be qualified (or relativized) and that modal models include a universe of what are called “possible worlds”. The classical semantical concept of truth in a model, written as \(\mathcal{A}\models \varphi\) is now replaced by truth at a world \(w\) in a model \(\mathcal{A}\), written as \(\mathcal{A},w\models \varphi\).

Formulas in basic propositional modal language are built from Atoms, classical connectives and modal operators, \(\square\) (box) and \(\Diamond\) (diamond). Modal formulas are interpreted in Kripke structures

having a non-empty domain \(\mathbf{W}\) of states or worlds, a binary accessibility relation \(\mathbf{R}\) defined over it, and a collection of subsets of \(\mathbf{W}\) for each atomic proposition symbol \(P\). A modal formula \(\varphi\) is true at world \(w\) in model \(\mathcal{A}\) (\(\varphi\) is satisfied in \(\mathcal{A}\) at world \(w\)) when the following inductive conditions apply:

A formula \(\varphi\) is globally true in a model \(\mathcal{A}\) if it is satisfied at all worlds in \(\mathcal{A}\) (\(\mathcal{A}\models \varphi\)). A formula \(\varphi\) is valid if it is globally true at all models (\(\models \varphi\)). The set of validities in the whole class of Kripke models (when no restrictions are imposed to the accessibility relation) are the validities of the basic modal logic, also called minimal modal logic or System K.[12]

Blackburn and van Benthem (2007: 5) note

the internal character of modal satisfaction definition: modal formulas talk about Kripke models from the inside

as modal formulas are evaluated at certain points. The intuition is that the modal operator \(\square\) is a kind of universal quantifier and modal structures are first-order relational structures with a binary relation and a collection of subsets of the universe. In a first-order language, to talk about these structures one needs a binary relation symbol, \(S\), as well as a collection of unary relation symbols. This language is called first-order correspondence language because every basic modal formula corresponds to a first-order formula. The standard translation of a modal formula \(\varphi\) is a first-order formula with one free variable expressing the semantics of modal formulas:

The idea behind this definition is to express in the correspondence language the semantic interpretation of the modal formulas: both languages are talking about the same structures, as a Kripke structure can be viewed as a plain first-order relational structure. From this definition the following equivalence is obtained:

(the assignment sends variable \(x\) to world \(w\))

From this lemma it is possible to derive Compactness, Löwenheim-Skolem and Enumerability theorems for the basic modal logic (Blackburn & van Benthem 2007: 11) just using the corresponding properties of first-order logic.

The set of validities of basic modal logic is not only recursively enumerable (as the enumerability theorem proves) but the satisfiability problem is also decidable. We wonder, what is the gain in translating a decidable logic into an undecidable one? Are we loosing decidability? The answer is that we don’t loose decidability; in fact, one can use translations to prove decidability for basic modal logic.

Concerning translation of basic modal logic into first-order correspondence language, there are at least two results to highlight:

However, these results apply to basic modal logic; in that logic we are talking about satisfiability as meaning “satisfiable on some model”, no restrictions (like transitivity) are imposed on the accessibility relation. And for any modal logic other than system K we are looking for models with additional properties. It is true that similar method can be applied with other propositional systems when the relevant properties can be expressed by first-order formulas with only two variables. Nevertheless, transitivity is a clear counter case.

In section 5.2, a variety of modal systems are treated (including S4, whose accessibility relation is reflexive and transitive) and several metatheorems are proved for them, by using the MSL reservoir. The translation is defined into a many-sorted first-order logic with a second-order flavor, as the many-sorted structures used in that section contain the relevant categories of mathematical sets (and relations) definable in the modal logic being translated.

In the following sections we present translations into many-sorted logic as the path to completeness in three stages.[15]

3.3 General Plan

The general plan is as follows: The signature of the logic being studied (call it \(\XL\)) is transformed into a many-sorted signature, the expressions of the logic \(\XL\) are translated into \(\MSL^{\XL}\) (a many-sorted language suited for \(\XL\)) and the structures of the logic \(\XL\) are converted into many-sorted structures. Thus, we need to define a recursive function \(\Trans\) to do the translation and a direct conversion of structures, \(\Conv_{1}.\)

With the direct conversion of structures we want to obtain as a result the equivalence of validity in the original structures for \(\XL\), call them simply \(\Str(\XL)\), with validity of a certain class of many-sorted formulas (the translations) in the class \(\mathfrak{S}^{\ast}\) of converted structures (where \(\mathfrak{S}^{\ast}=\Conv_{1}(\Str(\XL))\)).

Next question to ask is whether or not \(\mathfrak{S}^{\ast}\) can be replaced by the models of a set \(\Delta\) of many-sorted formulas. Thus, the key to both definitions, \(\Trans\) and \(\Conv_{1}\), is to simplify the proof of the semantic equivalence, and in this respect the relevance of the results obtained strongly depends on the possibility of axiomatizing \(\mathfrak{S}^{\ast}\). In case you get such a recursive set of formulas of \(\MSL^{\XL}\), say \(\Delta\), (or at least such that \(\mathfrak{S}^{\ast}\subseteq \Mod(\Delta )\)) we should prove that validity in \(\XL\) is equivalent to consequence from \(\Delta\) in \(\MSL^{\XL}\).

In case you get the set \(\Delta\), a reverse conversion of structures, \(\Conv_{2}\), should be defined. And so, from many-sorted models of \(\Delta\) we get structures in \(\Str(\XL)\). Our goal in defining it is to prove that starting from a many-sorted structure \(\mathcal{B}\) (a model of \(\Delta\)), a formula \(\varphi\) of \(\XL\) is true in \(\Conv_{2}(\mathcal{B)}\) if and only if the universal closure of its translation is true at \(\mathcal{B}\).

3.4 Level One: Representation Theorems

The logic being studied is \(\XL\) and we define a recursive function \(\Trans\) to do translations into \(\MSL^{\XL}\) as well as a direct conversion of structures, \(\Conv_{1}\). Our first goal is to state and prove the following:

We wonder, can validity in the class of structures \(\mathfrak{S}^{\ast}\) be replaced by consequence from a set \(\Delta\) of many-sorted formulas? The next goal is to find such a \(\Delta\), at least a set satisfying \(\mathfrak{S}^{\ast}\subseteq \Mod(\Delta )\). To finish level one, one needs to prove a Representation theorem; namely, a statement of the following form:

From Representation theorem it follows Enumerability for the logic \(\XL\). Namely, the set of validities of \(\XL\) is recursively enumerable. Therefore, \(\XL\) is complete in an abstract sense.

Remark: So, we learn that a calculus for \(\XL\) is a natural demand, but we also learn that in MSL we can simulate such a calculus and then we could use a theorem prover for MSL.

3.5 Level Two: the Main Theorem

When the \(\XL\) logic under scrutiny has a concept of logical consequence, we may try to prove the Main theorem; that is, that consequence in \(\XL\) (\(\Pi \models _{\Str(\XL)}\varphi\)) is equivalent to consequence of translations in MSL, modulo the theory \(\Delta\). To prove the main theorem, the reverse conversion of structures, \(\Conv_{2}\), should be used. Our goal in defining it is to prove the following:

From the previous results, our Main Theorem follows:

Remark: We already have Enumerability. Now, from Main Theorem as well Compactness and Löwenheim-Skolem for \(\MSL\), we easily obtain Compactness and Löwenheim-Skolem for \(\XL\). Therefore, the logic under investigation could have a strongly complete calculus. You can either define it or use the many-sorted one.

3.6 Level Three: Deductive Correspondence

When the \(\XL\) logic also comes with a deductive calculus, we can try to use the machinery of correspondence to prove, if possible, Soundness and Completeness for \(\XL\). In order to prove these theorems, one needs to prove a Theorem of deductive correspondence between the \(\XL\) calculus and the many-sorted one, modulo \(\Delta\). So, the next goal is to prove:

Since we already have the Main theorem (*), plus Completeness and Soundness for MSL (**), once we get this Theorem of deductive correspondence (***) the picture below gave us Soundness and Strong Completeness of \(\XL\):

Remark: We have reached the end of the road to completeness, but it is important to stress that we are using the already proven completeness results of MSL to prove strong completeness for \(\XL.\)

4. Second-order Logic as Many-sorted Logic

4.1 Second-order Logic

Second-order logic, SOL, is a very expressive formal language which differs from FOL (one-sorted first-order logic) in the following respects: (1) alphabet, (2) standard and non-standard semantics and (3) overwhelming expressive power with standard semantics. See the entry on second-order and higher-order logic as well as the entry on Church’s type theory.

The alphabet of second-order logic is obtained by including the first-order one-sorted variables and adding relation variables that can be quantified. As a result, in addition to the formula \(\forall x\varphi\) saying “for all individuals \(\varphi\) holds”, we have formulas \(\forall X\varphi\), \(\forall X^{2}\varphi\), etc. saying “for all properties, \(\varphi\) holds”, “for all binary relations, \(\varphi\) holds”, etc.

From the semantic point of view, to give meaning to the new variables we need new universes whose elements are sets and relations over the universe of individuals, say \(\mathbf{A}.\) In the so-called standard semantics, a set variable ranges over the power set of the individual’s universe, \(\wp (\mathbf{A})\), and a n-ary relation variable ranges over the power set of the n-ary Cartesian product of the individual’s universe, \(\wp (\mathbf{A}^{n})\). To put an example of the overwhelming expressive power of second order logic with standard semantics, Arithmetical induction can be expressed

and second-order Peano arithmetic (\(\PA^{2}\)) becomes categorical, that is, any two models of \(\PA^{2}\) are isomorphic. However, we pay a high price for the expressive power, we sacrifice the logic: Compactness fails, Löwenheim-Skolem fails and Completeness fails (both strong and weak).

Of course, the latter results are obtained with standard semantics. In Henkin 1950 he announces that the incompleteness problem is solvable if “a wider class of models” (non-standard models) is allowed. Therefore, he introduces: standard structures, general structures and frames. The classes of these structures are ordered by set inclusion

and, accordingly, the sets of validities in each class obey the reverse order[16]

In the semantics of frames, both sets and relation variables are allowed to range over universes which are subsets of standard universes. Somehow, this condition alone does not guarantee that we have enough sets and relations to deal with the second order capability. We would like to include in the universes all the definable ones in our formal language. This is a rather natural demand imposed to the general models (Henkin models) to obtain completeness.

In fact, with the semantics of frames, the set of validities coincides with the set of sentences derivable in a second-order calculus which is just an extension of the first-order one obtained by adding rules for the new quantifiers. This many-sorted calculus was isolated by Henkin (1953) in a paper where he introduced the Comprehension Schema

as a way of getting rid of the complex substitution rule of Church (1956). It is clear that, in case the only requirement you impose to the universes of the second-order structure is to be subsets of standard universes, there is no guarantee that they are models of Comprehension. That is why we need the general structures to obey extra rules, universes have to be closed under definability. With general structures the set of validities coincides with the set of sentences derivable in the second-order calculus. So, we go back to the situation encountered in first-order logic as you recover: Compactness, Löwenheim-Skolem and Completeness.

Obviously, SOL with general semantics is less expressive than with standard semantics. For instance, \(\forall X(Xx\leftrightarrow Xy)\) is no longer a definition of genuine identity between individuals. And so we take it as primitive and require equality \(\approx\) to be interpreted as identity. For higher types, Axiom of Extensionality

is added.

What is the conclusion of these results? As you know, a logic is like a balance scale: you have expressive power in one pan and computability power in the other. In case you wanted to retain logical properties, you had to change the semantics and lose some expressive power, you cannot have both at a maximum, they are “optimal impossible”. One can express the same idea in a more technical way by resorting to Lindström’s results (Lindström 1969) mentioned in section 2.3.

For more information on second-order logic, see the entry on second-order and higher-order logic, as well as Church 1956 and Enderton 1972. Very recommended is Henkin 1996 as well as some of the papers in The Life and Work of Leon Henkin (see Manzano, Sain, & Alonso 2014), in particular: “Changing a Semantics, Opportunism or courage?” (Andréka, van Benthem, Bezhanishvili and Németi 2014), “Henkin on Completeness” (Manzano 2014b), and “April the 19th” (Manzano 2014a).

4.2 Translation of Formulas and Conversion of Structures

Following the instructions in the corresponding section (§3.4 or §3.5), we define a syntactical translation from SOL to \(\MSL^{\SOL}\) as well as two conversions of structures, direct and reverse.

First of all, we realize that second-order structures are in fact many-sorted with certain peculiarities: in most cases they are what we called strict, because the intersection between any two different universes is empty, but all of them are related, as they are defined over the universe of individuals. Moreover, in the general structures the universes obey certain rules, like being models of Extensionality and Comprehension.

Let \(L\) be a second-order language with a set \(\OperSym\) of operation symbols. If we compare expressions in SOL with expressions in a many-sorted logic, we realize that \(X^{n}x_{1}\ldots x_{n}\) is not a formula of many-sorted logic since it is only a string of variables. What we do is to introduce a new many-sorted language, \(\MSL^{\SOL}\), where we retain all the symbols in \(\OperSym\) but the signature is now enlarged with new membership relation symbols, \(\epsilon _{n}\), whose interpretations are going to be a kind of membership relations. The many-sorted signature \(\Sigma ^{\SOL}\) includes a set \(\Sorts\) whose elements are the types in the SOL structure; namely, 1, and \(\langle\underbrace{ 1,\ldots ,1}_n ,0\rangle\) for all \(n\geq 1\).[17]

Therefore, the syntactical translation from SOL to this \(\MSL^{\SOL}\) leaves every formula the same except the atomic formulas of the kind mentioned above; i.e.:

Direct conversion of structures (from \(\SOL\) to \(\MSL^{\SOL}\)): Let us define \(\Conv_{1}\) as a function which takes any structure \(\mathcal{A}\in\Str(\SOL)\) and returns a structure \(\mathcal{A}^{\ast}\in \Str(\MSL^{\SOL})\). These structures are basically the same, with the only exception of membership relations we now add. This membership relation symbol of the many-sorted language, \(\epsilon _{n}\), is interpreted as genuine membership,

(where \(\mathbf{A}\) is the universe of individuals, of sort 1, and \(\mathbf{A}_{n}\) is the universe of n-ary relations, of sort \(\langle\underbrace{ 1,\ldots ,1}_n ,0\rangle\), and \(\mathbf{A}^{n}\) is the n-ary Cartesian product of \(\mathbf{A}\))

It is easy to prove the following result.

Now we ask, can we axiomatize \(\mathfrak{S}^{\ast}\)? and the answer is YES. The structures we want to work with are \(\MSL^{\SOL}\) models of Extensionality and Comprehension with Disjoint universes. Thus, let \(\Delta\) be:

Reverse conversion of structures (from \(\MSL^{\SOL}\) to \(\SOL\)): The reverse conversion of structures is done in four steps.[18]

The final result of the reverse conversion is just \(\Conv_{1}^{-1}(H(\mathcal{A}))\) and so we define \(\Conv_{2}\) accordingly.

With all these definitions at hand, we now prove:

4.3 Semantic Theorems Relating SOL and MSL

By applying the previous results, it is easy to prove the following semantic theorems:

As explained in section 3.5, by using Representation and Main theorems some important metatheorems of MSL can now be transferred to SOL.

Remark: The enumerability and compactness theorems taken together tell us that the logic under investigation could have a strongly complete calculus. In fact, we could use the many-sorted theory \(\Delta\) to derive SOL theorems in the many-sorted calculus.

However, in case we already had a calculus for SOL we can use the machinery of translations to prove its Soundness and Completeness.

4.4 Soundness and Completeness for SOL

We just follow the strategy presented on level three (in section 3.6) of our general plan to prove Soundness and Completeness for SOL calculus. What needs to be proven is the following theorem.

According to the general plan, from the Main theorem, the Deductive correspondence and Soundness and Strong Completeness of MSL, we get Completeness and Soundness for SOL with general semantics.

5. Translations Into Many-sorted Logic with a Second-order Appearance

5.1 General Plan

As mentioned already, in Henkin 1953 a new calculus for second order logic was defined by eliminating some Substitution Rules from the calculus presented in Church 1956[20] and introducing Comprehension Schema. In this paper, Henkin defines two calculi \(F^{\ast}\) and \(F^{\ast \ast}\) (basically, calculi MSL and SOL): the first one is obtained from a first-order calculus by adding rules for the new quantifiers, while the second is a proper second-order calculus. Both calculi are incomplete with standard semantics. Henkin mentioned that we can obtain a completeness result for the \(F^{\ast}\) calculus with the frame semantics. In fact, we have already seen completeness for MSL and that the second-order calculus is complete with the general semantics.

There is another interesting idea, appearing explicitly in the 1953 paper, which is also useful. The idea is: If we weaken comprehension, we obtain a calculus between \(F^{\ast}\) and \(F^{\ast \ast}\). And it is easy to find a semantics for the logic thus defined. Of course, this class of structures is placed between \(\mathfrak{F}\) and \(\mathfrak{GS}\). The new logic, call it \(\XL\), will also be complete; the main reason being that this class of models is again axiomatizable.

In what follows, this idea is exploited in several propositional modal logics as well as in propositional dynamic logic with Kripke semantics (see the entry on modal logic as well as the entry on propositional dynamic logic).

The second-order appearance mentioned in the title is as follows: when defining the conversion of structures into MSL we will add new universes containing all the categories of mathematical objects you can talk about in PML (or PDL); therefore, we add all sets and relations defined in these logics with their respective formulas and programs. And so, we are somehow shifting to SOL structures. We can add as well membership relation symbols to the language and membership relations to the structures, as we did in the conversion of SOL into MSL; we will end up in MSL but the inspiration is SOL.

5.2 Propositional Modal Logics as Many-sorted Logic

The first thing we do is to set a many-sorted language \(\MSL^{\PML}\) containing: unary relation symbols for each atomic proposition, \(P\in \Atom\), a binary relation symbol \(S\) to represent the accessibility relation, a membership sign, and equality for individuals and sets. \(\MSL^{\PML}\) contains individual variables as well as variables for sets. The translation is standard (as in section 3.2): we express in the target logic \(\MSL^{\PML}\) the semantical interpretation of the formulas being translated.[21] In particular,

The many-sorted structures we shall use are obtained from the modal structures by adding a universe containing sets of states or worlds. Given a Kripke structure

we say that \(\mathcal{AG}\) is a general structure built on \(\mathcal{A}\) if and only if

where \(\Def \subseteq \mathbf{W}^{\prime }\subseteq \wp (\mathbf{W})\). The sets \(\Def\) and \(\mathbf{W}^{\prime }\) contain all the members in the family \(\langle P^{\mathcal{A}}\rangle _{P\in \Atom}\) and are closed under several operations.[22] It can be proved that the set of worlds where a modal formula \(\varphi\) is true in a modal structure \(\mathcal{A}\) is the same set its translation defines in the general structure \(\mathcal{AG}\) built on \(\mathcal{A}\).

Let us use \(\mathfrak{G}\) to refer to the class of all general structures built on modal structures defined as above, our converted structures. It is not difficult to prove that validity of \(\varphi\) in PML is equivalent to validity of the universal closure of the translation of the formula in the class \(\mathfrak{G}\).

To finish the level one of the translation method, we need to axiomatize \(\mathfrak{G}\). Is that possible? The answer is positive for the minimal logic K (basic modal logic) as we can define a theory \(\Delta _{K}\) with the Comprehension Axiom

working mainly on many-sorted formulas \(\varphi\) obtained by translations of modal formulas. As we wanted a second-order appearance, Extensionality Axiom is added to \(\Delta _{K}\). As a result, we obtain a Representation Theorem for the minimal modal logic, K:

(in logic K the whole class of Kripke structures are used, no conditions are imposed on the accessibility relation)

As explained in section 3.4, from the previous theorem, Enumerability theorem for modal logic K is achieved. In fact, we already know much more, as we mentioned in section 3.2 that the set of validities in system K is decidable.

In case we wanted a similar outcome for another modal logic, say S4, the set \(\Delta _{K}\) can be extended to a set \(\Delta _{S4}\) including as axioms the many-sorted abstract conditions for axioms \(T\) and 4 (i.e., formulas \(\MS(T)\ \)and \(\MS(4)\)[23]). In fact, we can prove that the first-order axioms for reflexivity and transitivity are equivalent to these many-sorted translated sentences.

The Representation Theorem for S4 is easily obtained

(\(\mathfrak{D}\) is the class of reflexive and transitive Kripke models)

These results are relevant when we proceed further to prove the Main Theorem.[24] From this theorem we get for free Compactness and Löwenheim-Skolem for K and S4.

In case we wanted to prove that modal calculi for K and S4 (see the entry on modal logic) are complete by using the completeness of MSL, Deductive Correspondence between the modal logic concerned and its many-sorted counterpart have to be proved. Proving deductive correspondence from propositional modal logic to many-sorted logic is easy

as translations of modal axioms of system K are theorems of the MSL logic, while translations of \(T\) and 4 are theorems of \(\Delta _{S4}\). To prove the reverse deductive correspondence between MSL and PML the canonical model[25] \(\mathcal{B}_{K}\) (or \(\mathcal{B}_{S4}\)) could be used to build the general structure \(\mathcal{B}_{K}\mathfrak{G}\) (or \(\mathcal{B}_{S4}\mathfrak{G}\)). The final step is reached by using the general structure built onto the canonical model. It is easy to prove that the translation of a modal formula \(\varphi\) is true at a world of this structure if and only if formula \(\varphi\) belongs to this world.

Therefore,

The deductive correspondence between a modal logic and its many-sorted counterpart is achieved

and the soundness and completeness of the modal logics under investigation is reached by following the strategy explained in section 3.6.

A similar method can be applied in Propositional Dynamic Logic (PDL). PDL is a modal logic initially designed to talk about states and computer programs, it has a complete calculus whose axioms include the usual ones in modal logic K as well as other axioms describing the composition of programs (see the entry on propositional dynamic logic). Among them, it is worth highlighting Axiom 5. This axiom is also known as “induction axiom” and it is the responsible for one of the characteristic of PDL, its uncompactness. For this reason, the calculus of PDL is sound and complete but only in the weak sense.

The translation of formulas and programs into many-sorted logic is the expected one:[26] we express in the target logic \(\MSL^{\PDL}\) the semantical interpretation of the formulas and programs being translated.

For the conversion of structures, we follow a procedure similar to the one used in PML: we extend the Kripke model \(\mathcal{A}\) to a general structure \(\mathcal{AE}\) built on \(\mathcal{A}\)

The novelty is that now we have another domain \(\mathbf{W}^{\prime \prime }\) to include the binary relations defined by programs. Using these structures, one can prove that validity of a dynamic formula is equivalent to the validity of the universal closure of its translation in the class \(\mathcal{E}\) of all many sorted structures obtained in this way. The representation theorem is also available, once we define the theory \(\Delta _{\PDL}\). This theory includes as axioms the many-sorted abstract conditions for the PDL axioms, Extensionality (both for sets and relations) as well as Comprehension axiom for sets and relations defined by translations of formulas and programs.

At the end of the process, one can prove not only the semantical equivalence of validities in PDL with consequences from \(\Delta _{\PDL}\) of the universal closure of their translations, but also that the dynamic calculus proves as theorems all the formulas whose translations are theorems of our theory \(\Delta _{\PDL}\).

Weak completeness follows directly.[27]

6. Further Results

6.1 Reduction of Many-sorted Logic to One-sorted Logic

It is commonplace (Wang 1952, Feferman 1968, and Enderton 1972) to present many-sorted logic as easily convertible to one-sorted first-order logic. In Hao Wang (1952), the equivalence is built on provability while in Enderton’s book it has a semantical character.

Here we point out that many-sorted reduces to classical first-order logic (one-sorted) in the following sense: given a many-sorted structure \(\mathcal{A}\), every many-sorted sentence true at \(\mathcal{A}\) has a translation into one-sorted first order logic that is true at \(\mathcal{A}^{\ast}\), where \(\mathcal{A}^{\ast}\) is the result of unifying all the sorts in \(\mathcal{A}\). From this result we obtain the equivalence between consequences in both logics, modulo a theory \(\Pi\) easily defined.

For the syntactic translation (known as “relativization of quantifiers”), let \(L\) be a many-sorted language of signature \(\Sigma\), and let \(\OperSym\) be its set of operation symbols. We thus need an one-sorted language \(L^{\ast}\) with

Variables of \(L\) will be treated as variables of \(L^{\ast}\), forgetting about sorts. The difference between the many-sorted language \(L\) and the corresponding one-sorted one, \(L^{\ast}\), is that we add new unary relation symbols \(Q_{i}\), for each \(i\in \Sort\). Moreover, the symbols in \(\OperSym\) of \(L\) are also in \(L^{\ast}\) but while in the former language they have arity and sorts, in the latter they only have arity.

The translation, \(\Trans\), leaves every term and formula unaltered, with the only exception of quantified expressions that are relativized:

Example: As an example we will use the already presented argument from the Book of Perfect Emptiness. In one-sorted first order logic we can introduce this language:

As you see, instead of using different sorts of variables, we add two new unary predicates, \(O\) and \(I\). We formalize the argument as:

In order to derive the conclusion, we will need as well an extra hypothesis saying that the dawn of times and today are both times, \((Id\land It)\). We could add several formulas relating our new predicates:

For any many-sorted structure \(\mathcal{A}\) of signature \(\Sigma\) we construct its corresponding one-sorted structure \(\mathcal{A}^{\ast}\) by something called “unification of domains”.

The domain of \(\mathcal{A}^{\ast}\) is the union of the individuals domains of \(\mathcal{A}\), the interpretation of the new unary predicates \(Q_{i}\) corresponds to the old domains \(\mathbf{A}_{i}\) and so this information is kept. The interpretation of the rest of elements in \(\OperSym\) is similar to the one they have in the many-sorted structure \(\mathcal{A}\). The only difficulty concerns operation symbols with \(\Rank(f)=\langle i_{1},\ldots ,i_{n},i_{0}\rangle\) and \(i_{0}\not=0\) because now the universe is the union of the universes and function \(f^{\mathcal{A}^{\ast}}\) needs to give values to all of then. It is worth noting that for every \(f^{\mathcal{A}}\) there are many different operations extending it, which means that there are different one-sorted structures generated by the above conversion.[28]

The following theorem holds for any of these extended structures.

We have seen that many-sorted structures are always convertible into one-sorted ones and now we consider the other direction.

Is any one-sorted structure \(\mathcal{E}\) of signature \(\Sigma ^{\ast}\) convertible into a many-sorted one of signature \(\Sigma\)? The answer is negative, as there are two problems that could stop the conversion: the first one is that in a many-sorted structure all the universes should be nonempty and our idea is to take for each sort \(i\) the unary relation \(Q_{i}^{\mathcal{E}}\) as universe of sort \(i\) and so we need it to be nonempty; the second difficulty concerns operation symbols with \(\Rank(f)=\langle i_{1},\ldots i_{n},i_{0}\rangle\) whose interpretation in structure \(\mathcal{E}\) is just an n-ary function, but we need the values of \(f^{\mathcal{E}}\upharpoonright (Q_{i_{1}}^{\mathcal{E}}\times \ldots \times Q_{i_{n}}^{\mathcal{E}})\) to be in \(Q_{i_{0}}^{\mathcal{E}}\).

What we do is to formulate in the one-sorted language three conditions whose validity in a model makes it easily convertible into a many-sorted one. Let \(\Pi\) be the set of all sentences of the following forms:

Notice that the structure \(\mathcal{A}^{\ast}\) of the previous theorem is a model of \(\Pi\). Moreover, a one-sorted model of \(\Pi\), \(\mathcal{E}\), is easily convertible into a many-sorted one, \(\mathcal{E}^{\ddag }\). We take \(Q_{i}^{\mathcal{E}}\) as the universe of sort \(i\), strict relations and functions are obtained as restrictions to the corresponding domains to obtain relations and functions with the desired sorts.[29] Due to the axioms in \(\Pi\), construction of \(\mathcal{E}^{\ddag }\) can be carried out. It is now easy to obtain the following result.

We are using \(\models _{\MSL}\) and \(\models _{\FOL}\) to distinguish between consequence in many-sorted logic and in one-sorted logic.

The previous theorem allows us to infer the following three semantic theorems for MSL from the corresponding one-sorted results: Compactness theorem, Enumerability theorem and Löwenheim-Skolem theorem (see Enderton 1972: 281). But we have obtained them already as we have proven completeness for MSL (section 2.3). Obviously, from the many-sorted theorems we get the one-sorted version for free.

However, other theorems about many-sorted logic are not straightforwardly obtained from their one-sorted versions. In particular, interpolation in MSL requires its own proof (see section 6.2). The concept of interpretability plays an important role for a comparison between one-sorted and many-sorted theories (see section 6.3 and Hook 1985). Unfortunately, interpretablity between many-sorted theories is not obtained from their one-sorted counterparts. Concerning the comparison, deductions in a many-sorted proof system are usually shorter than the derivations we get in a one-sorted calculus, that is one of the reasons why many-sorted logic is so frequently used in Computer Science (Meinke & Tucker 1993).

6.2 The Interpolation Theorem

The Interpolation Theorem, which according to Wilfrid Hodges has “the longest pedigree of any theorem of model theory”,[30] plays a relevant role in logic. In the first place, several important results such us Beth’s definability theorem and Robinson theorem could be obtained directly from it (see the entry first-order model theory). In the second place, interpolation can be seen as a central logical property which “has been used to reveal a deep harmony between syntax and semantics” (Feferman 2008: 341).

The one-sorted version of interpolation was proved by William Craig in 1957a. Roger Lyndon (1959) gave a generalization of Craig’s theorem and, in 1968, Feferman extended the latter formulation to many-sorted logic (see Feferman 2008: 349). Obviously, the one-sorted version is a special case of the many-sorted one. However, many-sorted interpolation cannot be straightforwardly transferred from the one-sorted case.

The idea for Craig’s 1957 proof of the Interpolation Theorem rests on the completeness theorem for one-sorted first-order logic. The reason is that interpolation “lies” somehow in the intersection of proof theory (as it follows from some metatheorems about the calculus) and model theory (because of its applications). Henkin showed that the other way round also holds: completeness can be immediately obtained from a extended version[31] of Craig-Lyndon’s theorem.

The syntactical formulation of Craig’s interpolation theorem reads as follows: If \(\varphi\) and \(\psi\) are sentences and \(\vdash \varphi \rightarrow \psi\), then:

where \(\Rel(\alpha)\) is the set of relational symbols in \(\alpha\). The intuition behind is as follows: during the process of proving the conditional formula \(\varphi \rightarrow \psi\), we make use of what is today known as an “interpolant”, \(\theta\), a kind of syllogism middle term that finally disappears.

The theorem cannot be established for many-sorted logic by simply translating \(\varphi\) and \(\psi\) to the corresponding formulas of a one-sorted language. It is easy to see that the logical form of a constructed interpolant for \(\vdash \Trans(\varphi )\rightarrow \Trans(\psi )\) is not necessarily equivalent to a translation of a many-sorted formula. This is why we said that this result could not be straightforwardly transferred from the one-sorted case (see Otto 2000 for more details).

As in one-sorted logic, the interpolation lemma for a many-sorted logic can be proven in model-theoretic style (as in Kreisel & Krivine 1967) or in proof-theoretical style, as in Feferman.[32]

Feferman’s proof of interpolation is obtained directly as a corollary of one of his theorems for sequents (see Feferman 1968: 56–62; Theorem 4.3) and its applications are model-theoretical, what reveals again the peculiar centrality of interpolation.

6.3 Interpretability and Theoretical Equivalence

Another notion not immediately transferable from FOL to MSL is that of interpretability. Interpretability is a good criterion for fixing a comparison between theories \(T\) and \(T^{\prime }\), for it is characterized either in terms of “uniform definability of models” or of “the existence of an interpretation map which preserves logical form and provability” (Mceldowney 2020: 15). It is also helpful for proving consistency, as \(T^{\prime }\) is proved to be consistent when interpreted in a consistent \(T\). However, interpretability between theories of a many-sorted signature does not guarantee interpretability between their (one-sorted) translations.

Mceldowney (2020) argues that the concept of bi-interpretability is the best measure of theoretical equivalence in MSL. The oldest criterion for theoretical equivalence between first-order theories with the same signature is the notion of definitional equivalence (see Eilenberg & Mac Lane 1942, 1945 and Glymour 1971). Therefore, the necessity of a many-sorted counterpart was apparent. As a result, a debate on the nature of equivalence in MSL has taken place since 2016. Barrett and Halvorson (2016) generalizes the idea of definitional extension to the concept of Morita extension: intuitively, \(T^+\) is a Morita extension of \(T\) iff both \(T\) and \(T^+\) are MSL theories and \(T^+\) “says no more” than the original theory (see 2016: 565 for formal details).

Thus, they claim that theoretical equivalence in MSL is to have a common Morita extension (this is called “Morita equivalence”). It is worth recalling at this point that the Morita extension \(T^{+}\) of \(T\) might be constructed by adding new sort symbols to the signature of \(T\) together with the corresponding explicit definitions[33] to the axioms. There are several ways to carry out this extension: the new sort \(\tau\) can be introduced as a subsort, product, coproduct and quotient sort (see Barrett & Halvorson 2016: 563–64). Morita equivalence has also been used to try to clarify what is known in the literature as Quine’s conjecture on many-sorted logic (see Barrett & Halvorson 2017).

Nevertheless, according to Mceldowney (2020), a nuanced concept of Morita equivalence is just a special case of bi-interpretability. For this reason, he opted for a notion of equivalence in MSL based on interpretability rather than Morita extensions (see pp. 404-407 in Mceldowney 2020). In fact, as pointed out in Friedman and Visser (2014), bi-interpretability preserves finite axiomatizability, decidability, and κ-categoricity.