Classical logic is the appropriate formal language for describingmathematical structures containing a single universe or domain ofdiscourse. By contrast, many-sorted logic (MSL) allows quantificationover a variety of domains (called sorts). For this reason, it is asuitable vehicle for dealing with statements concerning differenttypes of objects, which are ubiquitous in mathematics, philosophy,computer science, and formal semantics. Each sort groups a uniquecategory of objects (for example, points and straight lines aredifferent types of objects in a 2-sorted structure).

Despite the addition of this expressive resource, many-sorted logic“stays inside” first-order logic, so the main metatheorems(completeness, interpolation, and so on) can be proved. Many-sortedlogic also serves as a unifying framework for translating variouslogical systems; for instance, some intensional and higher-orderlogics have natural translations into many-sorted logic. Many-sortedfirst-order logic can be reduced to one-sorted first-order logic, bothsyntactically and semantically. Many-sorted first-order logic can alsobe extended to a many-sorted second-order logic called “sortlogic”.

An axiomatic calculus for many-sorted logic was introduced by Hao Wangin Wang (1952), where he made a comparison between one-sorted andmany-sorted theories. In 1967, Solomon Feferman gave a sequentcalculus for many-sorted logic, proving not only its completeness butalso the cut elimination and interpolation theorems (Feferman1968). Feferman (2008) summarizes some applications of the many-sortedinterpolation theorems to model theory. (See thesupplement on early history for more information.)

Section 1 lays out the basics of many-sorted logic, presenting someexamples and explaining how the formal language, structures, andsemantics differ or not from classical logic. Section 2 explains howto modify a one-sorted first-order calculus to obtain a many-sortedversion; also, completeness is treated and some automated theoremprovers are mentioned. Section 3 describes a plan on which many-sortedlogic serves as a common framework for translating a variety oflogical systems. Sections 4 and 5 apply this plan to second-orderlogic and non-classical logics (modal and dynamic logic),respectively. Finally, section 6 comments on further results inmany-sorted logic.

• 1. Syntax and Semantics
  • 1.1 Examples
  • 1.2 Fundamental Ideas
  • 1.3 Formal Language
  • 1.4 Many-sorted Structures
  • 1.5 Semantics
• 2. Calculus
  • 2.1 Deductive Calculi
  • 2.2 Completeness Notions
  • 2.3 Completeness of Many-sorted Logic
  • 2.4 Automated Theorem Provers
• 3. Many-sorted Logic as a Unifying Framework
  • 3.1 Translations
  • 3.2 Correspondence Language for Basic Modal Language
  • 3.3 General Plan
  • 3.4 Level One: Representation Theorems
  • 3.5 Level Two: the Main Theorem
  • 3.6 Level Three: Deductive Correspondence
• 4. Second-order Logic as Many-sorted Logic
  • 4.1 Second-order Logic
  • 4.2 Translation of Formulas and Conversion of Structures
  • 4.3 Semantic Theorems Relating SOL and MSL
  • 4.4 Soundness and Completeness for SOL
• 5. Translations Into Many-sorted Logic with a Second-order Appearance
  • 5.1 General Plan
  • 5.2 Propositional Modal Logics as Many-sorted Logic
• 6. Further Results
  • 6.1 Reduction of Many-sorted Logic to One-sorted Logic
  • 6.2 The Interpolation Theorem
  • 6.3 Interpretability and Theoretical Equivalence
  • 6.4 Extension of Many-sorted Logic to Sort Logic
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Syntax and Semantics

1.1 Examples

We start with a few examples to illustrate how common statementsconcerning different types of data can be formalized in many-sortedfirst-order logic.

Example: Euclid’s first principle

Let us begin with geometry, by talking about straight lines andpoints. 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,\)… asvariables for sort \(l\) (straight lines) and \(x,\) \(y,\)… asvariables for sort \(p\) (points). To formulate Euclid’sprinciple we write:

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

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

Example: Binary relations

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

Every asymmetric binary relation is also anti-symmetric.

To formalize the statement as a single logically validsentence we need: (1) to express asymmetry and anti-symmetry,and (2) to quantify over binary relations. In a suitable first-orderlanguage 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 logicallyvalidscheme:

What we get is an infinite set of formulas obtained by replacing \(R\)by any other binary relation symbol. However, we wanted a singlelogically validsentence and so we need to quantify overbinary 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 niceproperties of first-order logic (section 4.1), one could instead go for a two-sorted first-order logic, in whichboth individuals and relations between individuals are first-classcitizens 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 orbinary relations, we need them to perform as second-order variables do. A three-place predicate symbol relating binaryrelations and individuals, \(\epsilon_{2} xyX^{2}\), needs to be addedso that \(\Asymm(X^{2})\) becomes:

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

As we will see insection 4.2, rewriting the second order formula \(X^{2}xy\) as \(\epsilon_{2}xyX^{2}\) is all we do when translating second-order logic intomany-sorted logic; some axioms for predicates \(\epsilon _{n}\) areadded 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.

Example: Comprehension Axiom

Let us introduce another, more philosophical, example. If wewanted 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 \lnotXx)\) is a generalization of an instance of Comprehension Scheme

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

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

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

now becomes

To representEvery property has a negation in one-sortedfirst-order logic we use \(x,y,z,\ldots\) as variables for the uniquesort we now have, and write:

where

Some axioms for predicates \(\epsilon _{1}\) are added, as well asaxioms saying that predicates \(P\) and \(O\) are never interpreted asempty sets, \(\exists xOx\) and \(\exists xPx\). Moreover, the linksbetween predicates \(\epsilon _{1}\), \(P\) and \(O\) are expressedby:

1.2 Fundamental Ideas

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

• Structures: A many-sorted structure has severalnon-empty domains, one for each sort, and variables of a given sorttake values over the corresponding domain. Ann-ary relationcould be freely established between elements of different domains oronly between certain ones. These two options are calledliberal andstrict. A liberal relation may relateobjects of arbitrary domains and only the arity (a natural number) hasto be stated. For a strict relation, the sortsinvolved have to be specified as well as the arity.

• Alphabet: The alphabet of a many-sorted language\(L\) includes all the relation, function, and constant symbols in aset called \(\OperSym\), as well as an infinite number of variablesfor each sort \(s_{i}\in \Sort\), and the corresponding sets ofvariables are disjoint. Ann-ary relation symbol \(R\) couldbe strict or liberal and, in the first case, we must provideinformation about what are the involved sorts. To achieve thisrequirement, we define a function \(\Rank\) having as domain the set\(\OperSym\) and whose values are either natural numbers other thanzero (liberal option) or finite strings of \(\Sort\cup \{ 0\}\)(strict option). For any strict \(f\in \OperSym\), its value\(\Rank(f)\) always has the form \(\langlei_{1},\ldots,i_{m},i_{0}\rangle\), with \(i_{0},i_{1},\ldots,i_{m}\in\Sort\cup \{ 0\}\). When \(f\) is anm-ary predicate,\(i_{0}=0\), and \(i_{0}\not=0\) form-ary function symbols;individual constants are considered as zero-ary function symbols with\(\Rank(f)=\langle i_{0}\rangle\), simplified as \(i_{0}\).

• Signature: By asignature \(\Sigma\) we meanthe ordered triple

  \[\ \Sigma =\langle \Sort,\OperSym,\Rank\rangle\]

  Equality is a binary symbol that could be strict or liberal. In ourlanguage, the equality symbol \(\approx\) with \(\Rank(\approx )=2\)is liberal (having arity 2 and being allowed to work between terms ofany sort).^[2] The quantifier \(\exists x^{i}\) is used for variables \(x^{i}\) ofany sort \(i\).

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

1.3 Formal Language

Terms and Formulas

As we do in classical first-order logic, from the set of finitestrings of elements of the alphabet we select the expressions of\(L\):terms andformulas. The only difference isthat in many-sorted logic terms have sorts and we have to specifyit.

In consequence, theterms of many-sorted logic are definedrecursively 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 termof 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 termsof sorts \(i_{1},\ldots,\) \(i_{m}\), then \(R\tau _{1}\ldots \tau_{m}\) is a formula (when \(R\) is a liberal predicate, we drop thesort 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 notmatter, because our choice of equality symbol is the liberal one.^[3]

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

Free and bound variables

As in classical first-order logic, occurrences of variables in a formula can befree orbound; they are bound when they are underthe scope of a quantifier, otherwise free. A variable is free in aformula if it has at least one free occurrence therein. A formula withno free variables is called asentence. We use \(Sent(L)\) todenote the set of sentences of language \(L\).

Example: The Book of Perfect Emptiness

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

In order to analyze this example, we should identify premises andconclusion; and we easily observe that the initial rhetorical questionis in fact the argument’s conclusion. The considered argument isan enthymeme, for the reason that it seems to be supported in thepermanence of the laws that govern the cosmos (in particular, thoseconcerning the existence of objects). The hidden hypothesis supportingthe argument could be the following law:

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

This rule is not saying that existence of a particular object iseternal, it is saying that the chain of existence goes backforever.

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 atwo sorted language, \(\Sort=\{ i,\tau \}\), includingobjects (sort \(i\)) andinstants of time (sort\(\tau\)). The set \(\OperSym\) contains a binary predicate ofexistence at a given time, \(E\), another binary predicate ofprecedence between instants, \(P\), and two individual constants fortoday (\(t\)) and thedawn of times \((d)\). So, inthis case,

The argument now reads:

In many sorted logic, the conclusion is easily obtained from thesehypotheses by using a deductive calculus (seesection 2). Therefore, the argument is formally correct, once we accept theproblematic hypothesis \(\alpha\). Insection 2.4 we rewrite the argument to use theorem provers LEO-II andLEO-III.

1.4 Many-sorted Structures

The semantics of many-sorted logic is rather similar to that ofclassical first-order logic, because it follows Tarski’s truthdefinition to introduce the concept oftruth in a structure(see Tarski 1933 and Tarski & Vaught 1956; for historicalclarifications, see Hodges 1986 and the entry onTarski’s truth definitions). In our case, theobject language is many-sorted logic andthemetalanguage is set theory. Set theory is the commonlyused metalanguage, where relation symbols are interpreted asrelations defined overuniverses (sets) ofmathematical structures.

In many-sorted first-order logic, a structure is understood as a tuplehaving a family of non-empty sets as domains and a family ofoperations (functions and relations) defined over these domains. Theserelations and functions are defined according to a givensignature.

Examples of many-sorted structures

• An appropriate structure \(\mathcal{E}\) for the example inThe Book of Perfect Emptiness has two universes:instants of time \(\mathbf{A}_{\tau}\) and objects \(\mathbf{A}_{i}\).It also has two distinguished instants, today and the dawn of times, abinary relation between objects and instants, and a binary temporalrelation of precedence.

  \[\mathcal{E}=\langle \langle \mathbf{A}_{i},\mathbf{A}_{\tau }\rangle ,E^{\mathcal{E}},P^{\mathcal{E}},t^{\mathcal{E}},d^{\mathcal{E}}\rangle\]

  In such a structure, \(t^{\mathcal{E}},d^{\mathcal{E}}\in\mathbf{A}_{i}\), \(E^{\mathcal{E}}\subseteq \mathbf{A}_{i}\times\mathbf{A}_{\tau }\) and \(P^{\mathcal{E}}\subseteq \mathbf{A}_{\tau}\times \mathbf{A}_{\tau }\).

• A second-orderstandard structure (orfullstructure)

  \[\mathcal{A}=\langle \mathbf{A},\langle \wp \left(\mathbf{A}^{n}\right)\rangle _{n\in \mathbb{N}},\langle f^{\mathcal{A}}\rangle _{f\in \OperSym}\rangle\]

  is another example of many-sorted structure. This structure includesthe domain of individuals \(\mathbf{A}\) as well as a family of secondorder domains ofn-ary relations on individuals, \(\wp(\mathbf{A}^{n})\), for each natural number \(n\). The relations andfunctions in \(\langle f^{\mathcal{A}}\rangle _{f\in \OperSym}\) arefirst-order relations and functions defined over the universe ofindividuals (for more details about second-order logic, see the entryonsecond-order and higher-order Logic).

• A second-ordergeneral structure \(\mathcal{A}=\langle\mathbf{A},\langle \mathbf{A}_{n}\rangle _{n\in \mathbb{N}},\ldots\rangle\) could also be seen as many-sorted. As in standardstructures, \(\mathcal{A}\) contains the domain of individuals\(\mathbf{A}\) as well as domains ofn-ary relations for eachnatural number, \(\mathbf{A}_{n}\subseteq \wp (\mathbf{A}^{n})\). Butsince \(\mathcal{A}\) is a general structure, the universes\(\mathbf{A}_{n}\) are not arbitrarily chosen, for the reason thatthey must satisfy theComprehension Schema. Therefore, theuniverses are closed under definability (more information on generalstructures insection 4.1).

Many-sorted structures

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: anm-ary relation \(R^{\mathcal{A}}\) foreach relation symbol \(R\), ann-ary function\(f^{\mathcal{A}}\) for everyn-ary function symbol \(f\) anda distinguish element \(c^{\mathcal{A}}\in \mathbf{A}_{i}\) for everyindividual constant \(c\). These relations and functions have to beestablished between elements of the family of domains taking intoaccount their values under function \(\Rank\).^[4]

Using structure \(\mathcal{A}\) we define insection 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 differentdomains. Structures obeying this requirement are called“strict”, otherwise “lax” (or“liberal”). For strict structures we may consider thepossibility of having an equality symbol for each sort, \(\approx_{i}\), each of them with \(\Rank(\approx _{i})=\langlei,i,0\rangle\). We require equality symbols (either strict or liberal)to be interpreted as genuine identity, the prototypical relation thatholds between an object and itself and fails to hold between any twoother objects.

Relations of similarity between structures

For one-sorted structures, it is very common to study differentrelations between them:homomorphisms,embeddings,isomorphisms, substructures andextensions (see Manzano1989 [1999: 19–33]). One can define these relations formany-sorted structures in a similar vein. Anhomomorphismbetween two structures \(\mathcal{A}\) and \(\mathcal{A}^{\prime }\)with the same signature is a function \(\pi\) from the union of theuniverses 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 afunction from \(\mathbf{A}_{i}\) to \(\mathbf{A}_{i}^{\prime }\), foreach \(i\in Sort\). Secondly, if then-tuple of elements\(\langle \mathbf{a}_{i},\dots ,\mathbf{a}_{n}\rangle\) is in then-ary relation \(R^{\mathcal{A}}\) then \(\langle \pi(\mathbf{a}_{i}),\dots ,\pi (\mathbf{a}_{n})\rangle\) is in therelation \(R^{\mathcal{A}^{\prime }}\). Finally,

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

Anembedding is a homomorphism where the involved functionsare injective and the second condition works in both directions. Anisomorphism is an embedding where the defining maps arebijections. When the function \(\pi\) is an isomorphism one says that\(\mathcal{A}\) and \(\mathcal{A}^{\prime }\) areisomorphicand writes \(\mathcal{A}\cong \mathcal{A}^{\prime }\).

We say that \(\mathcal{A}^{\prime }\) is asubstructure of\(\mathcal{A}\) (equivalently, \(\mathcal{A}\) is anextension of \(\mathcal{A}^{\prime }\)) if and only if theinclusion map \(i\) (sending every element to itself) is an embeddingfrom \(\mathcal{A}^{\prime }\) to \(\mathcal{A}\).

All the relationships already mentioned are established betweenstructures of the same signature. We can as well define reductions andexpansions between structures whose signatures are not the same. Givena many-sorted structure \(\mathcal{A}\), areduct\(\mathcal{A}^{\prime }\) of \(\mathcal{A}\) is obtained by simplyremoving some sorts, function or relation symbols from the signatureof \(\mathcal{A}\). If \(\mathcal{A}^{\prime }\) is a reduct of\(\mathcal{A}\), then we say that \(\mathcal{A}\) is anexpansion of \(\mathcal{A}^{\prime}\).

1.5 Semantics

Denotation of Terms and Satisfaction of Formulas

Given a language and a structure, both of them sharing the samesignature, each closed term of the language will denote an element inthe structure and each atomic sentence is either true or false in thestructure. Nevertheless, the scope of our definition is widenedso that each term will receive a denotation and each formula a truthvalue. To achieve that, we define assignments^[5] from the set of variables to the domains of the structure, argumentsand 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 likeassignment \(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 theconcept ofsatisfaction of a formula \(\varphi\) in\(\mathcal{A}\) under assignment \(s\) (noted as\(\mathcal{A},s\models \varphi\)), as well as thedenotationof terms.

Denotation of terms

Let \(\mathcal{A}\) be anL-structure (language and structuresharing signature \(\Sigma\)) and \(s\) an assignment.\(\mathcal{I}=\langle \mathcal{A},s\rangle\) is called aninterpretation. 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 classicalone-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 ofthat sort.

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

Coincidence lemma

As in classical first-order logic, the coincidence lemma holds (seethe entry onclassical 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 variablesare in \(\{ x_{1},\ldots ,x_{n}\}\) one can write

instead of

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

For a set of sentences \(\Gamma\) we say that \(\mathcal{A}\) is amodel 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 alanguage \(L\) and a class of mathematical structures, sharing a givensignature \(\Sigma\). Between these mathematical realities we havejust built a bridge, the notion oftruth in a structure. Inone direction, we circulate from sentences to structures where thesesentences are true; on the other direction, we go from structures tosentences which are true in these structures. In the first case, froma 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 whichare true at structure \(\mathcal{A}\)

Elementary embedding

In the previous section, the relations between structures were definedwithout resorting to the many-sorted formal language. That is not thecase forelementary embedding, another relationship betweenmany-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 andelements with the same sorts.

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

Satisfiability, Validity, and Consequence

Concepts ofsatisfiability,validity andconsequence are defined as in classical first-order logic.Given language \(L\) of signature \(\Sigma\) and a formula \(\varphi\)of \(L\): \(\varphi\) issatisfiable if and only if thereexists a Σ-structure \(\mathcal{A}\) and assignment \(s\) on itsuch that \(\mathcal{A},s\models \varphi\) holds; \(\varphi\) isvalid (\(\models \varphi\)) if and only if\(\mathcal{A},s\models \varphi\) holds for all \(\mathcal{A}\) ofsignature \(\Sigma\) and any assignment \(s\) on \(\mathcal{A}\).

Given a language \(L\) of a given signature \(\Sigma\) we define theconsequence 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 regarda logic as comprising at least three different things: a class ofstructures, a formal language to describe these structures, and asatisfaction relation that determines when a formula of the languageis true with respect to a given structure. A deductive calculus might beadded.

In fact, any calculus for one-sorted first-order logic can be easilyextended to a many-sorted one; the only rules which need to be adaptedare the ones dealing with quantifiers and substitution, as they haveto take into consideration the variety of sorts admitted. In the entryclassical logic the rules that need to be changed are: introduction and eliminationof 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 therules dealing with equality (\(=\mathbf{I}\) and \(=\mathbf{E}\)).

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

As usual, to symbolizederivability of a formula from a setof formulas we write, \(\Delta \vdash \varphi\). We will write thederivability sign \(\vdash\) with a subscript when needed; namely,\(\vdash _{\MSL}\). In any of these calculi the notion of proof iseffective in the sense that there is a method by which whenever afinite sequence of sequents of formulas is given, it can always beeffectively determined, whether it is a proof or not. Any of thesecalculi isundecidable, as there is not an algorithm to checkif \(\vdash \varphi\) or not. In fact, it could not be otherwise asthesatisfiability problem (i.e., determining validity, orequivalently, testing for satisfiability of given formulas) formany-sorted logic is undecidable. So, we are in the same situationencountered in one-sorted first-order logic.

Of course, if a calculus is to be helpful it would never allowerroneous reasonings: it is not going to drive us from true hypothesesto false conclusions. It must be asound 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 liketo have astrongly complete calculus. In oursection 2.3 you will find the sketch of such a completeness proof.

Maximal consistency and the property of having witnesses

Also standard are the definitions of the syntactic concepts;^[7] namely those ofconsistency,maximal consistencyand the property ofhaving witnesses. In the presentcircumstance, a set of formulascontains witnesses if eachexistential formula comes with a witness (\(\exists x^{i}\varphi \in\Delta\) implies \(\varphi (t/x^{i})\in \Delta\) for a term \(t\) ofsort \(i\)). All three are properties of formulas and/or sets offormulas and in their definition we use derivability; i.e., thedeductive calculus.

Consistency can be seen as the syntactic counterpart ofsatisfiability, in the same sense as \(\vdash\) and \(\models\) wouldcorrespond to one another. In fact, Henkin’s completeness proofbasically consists in the construction of a model for each consistentset.

2.2 Completeness Notions

Proof and truth are defined by independent methods and it is nottrivial, but necessary, to prove that they are extensionally the same.This is the content of thecompleteness theorem when thisproperty is predicated of asound calculus. There is anothermeaning ofcompleteness, when it is predicate of a theory: Atheory \(\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 calculusestablishes its sufficiency for capturing the logical consequence;namely, whenever a sentence follows logically from a set ofhypotheses, there is a proof of this sentence in the calculus,possibly using some of these hypotheses. In contrast,weakcompleteness says that we have proofs for all validities. In a complete^[8] logic, the expressive power of the language and its computationalstrength are well balanced. Thus the question about completeness isthe question about the equilibrium of the basic components of a logic:its semantics and its logical calculus.

Sometimes, we merely say that alogic is complete and qualifythis property asabstract completeness. In this case, we areonly concerned with the computational characteristics of the set oflogical truths (validities), all we need to know is that they arerecursively enumerable.

Section 3 presents many-sorted logic as a unifier logic and we describe thethree levels process of embedding into MSL as a path to completenessof 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 byfollowing the well known Henkin (1949) strategy for first-order logic.The important issue is to be able to show that each consistent set offormulas has a model, and hence syntactic consistency and semanticsatisfiability are equivalent (assumingSoundness). The proofis performed in basically two steps:

1. Every consistent set of formulas can be extended to a maximalconsistent set with witnesses.

2. Once we have the maximal consistent set with witnesses, we use it as aguide to build the precise model described by formulas of this set.The reason being that a maximally consistent set is a very detaileddescription of a structure.

By doing that we prove:

The completeness theorem

follows easily from it.

To see thatHenkin’s theorem impliesStrong completeness, let us assume the antecedent,\(\Gamma \models \varphi\). Therefore, \(\Gamma \cup \{ \lnot \varphi\}\) is not satisfiable, it has no model. Using Henkin’s theoremwe conclude that \(\Gamma \cup \{ \lnot \varphi \}\) is contradictoryand so \(\Gamma \cup \{ \lnot \varphi \} \vdash \varphi\). Thecalculus 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 provedin its strong sense and for all formulas, not only for sentences.Completeness and its corollaries are proven by following the pathintroduced by Ebbinghaus, Flum, and Thomas (1984).

Is many-sorted logic a proper (or strict) extension of first-orderlogic? Lindström (1969) proves that first-order logic ischaracterizable as the strongest logic to possess simultaneouslyCompactness andLöwenheim-Skolem properties.Moreover, first-order logic is the strongest logic whereLöwenheim-Skolem holds and its set of valid sentences isrecursively enumerable. Therefore, many-sorted logic cannotbe considered as a proper extension of first-order logic.

2.4 Automated Theorem Provers

Many-sorted logic provides a semantical concept of consequence as wellas a deductive calculus to be used in the mathematical process ofobtaining conclusions from hypotheses. Now the issue is to automatethis reasoning process by building a computer program to conductdeductive inferences.

As we have already mentioned, soundness is the essential requirementof a calculus while completeness guarantees that all the semanticalconsequences can be established within the calculus and so the set ofvalidities isrecursively enumerable. The most relevantproperties for automated deduction aredecidability andcomplexity. A logic is decidable when there is an algorithmthat answerYES orNO in a finite time to thequestion:is the formula \(\varphi\) valid? As validity andsatisfiability are interdefinible (\(\models \varphi\) iff \(\lnot\varphi\) is not satisfiable) this problem is often called thesatisfiability problem. Among the basic tasks a computer isasked for aresatisfiability andmodel checking.

Propositional logic is decidable but first-order logic, many-sortedversion included, is undecidable. However, in between propositionaland first-order logic there are decidable logics, likemonadicpredicate logic (first-order logic whose predicates are all unarypredicates), as well as decidable fragments^[10] of the undecidable logic. Moreover, among the decidable problemsthere are degrees of time-space complexity measuring time and memoryregister used by the computer.

Therefore, in a theorem prover for many-sorted calculus there is noguarantee of getting an answer to the question:Does \(\Gamma\models \varphi\)? However, there are efficient theorem proversable to solve the problem in many cases; for instance, when there aredecidable fragments to implement. See the entries onautomated reasoning andChurch’s type theory. Section 4 of the entry on Church’s type theoryis devoted to automation and provides information aboutmachine-oriented proof calculi as well as early proof assistants. Anexcellent selection of theorem provers for Church’s type theoryare presented. Among them are LEO-II and LEO-III, the latter is saidto “cooperate with first-order reasoning tools usingtranslations 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 manybase types \(i_1\), \(i_2\), \(i_3\),…, \(i_n\) and apply ananalogous construction. These base types \(i_1\), \(i_2\),\(i_3\),…, \(i_n\) can be considered as sorts.

Our example from theBook of Perfect Emptiness can beformalized 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 relationshipsbetween and their possible translations into one another a pressingissue. We saw above that many-sorted logic is a natural logic forreasoning about more than one sort of objects. In this section, wewill present it as a unifying framework in which we may situate mostof the many logics available to us. The general plan of translationsinto MSL is described with some details. Three possible levels oftranslations are settled and, at each level, when successfullyreached, one completeness result is gained: abstract completeness atthe first level, strong completeness at the third. Therefore, when alogic is translated into many-sorted logic we only need a uniquedeductive calculus, the many-sorted one, as well as an efficienttheorem prover. In cases likebasic propositional modallogic, where formulas could be translated into a decidablefragment of first-order logic with only two variables, the translationmechanism implies decidability for the modal logic. Moreover, somemetaproperties of many-sorted logic can be transferred to the logicbeing translated.

Translations offer a better understanding of the logics beingtranslated and could be used to compare two logics when they aretransformed into theories of a common target logic, many-sortedfirst-order logic in our case. It is not a positive answer to thequestion“The One Right Logic?” (see the entryclassical logic) as this question was not posed and it is not in the spirit of thistranslation into many-sorted logic. InModal Logic for OpenMinds (van Benthem 2010) translations into first-order logic areextensively treated and there is a section entitled “Discussion:what good is a translation” (2010: 77) where Johan van Benthemanalyzes the balance of expressive power and complexity and advocatesfor a tandem approach to answer the questionDoes the translationST mean that we can forget the modal language and just do first-orderlogic?

Translations

Translations between logics have been formulated as an ambitiousparadigm whose tools would serve for handling the existingmultiplicity of logics. Some methodologies are proof-oriented, othersare model-oriented, and finally some others are conceived in purelyabstract suprastructural terms.

1. From aproof-theoretical point of view, the style ofcomparing logics will rest upon deductive calculi. The “labelleddeductive systems” of Dov Gabbay (1994 and 1996) emerge.

2. From amodel-theoretical perspective, one will presumablycompare logics by defining relations between the structures thoselogics are attempting to describe, as in the correspondence theory ofJohan van Benthem (1983, 1984a, and 2010).

3. From asuprastructural point of view, we define morphismsbetween categories. Among the abstract approaches to logic wehighlight the “general logics” of José Meseguer(1989) as well as the “rewriting logic” of NarcisoMartı́-Oliet and José Meseguer (1994). Da Silva,D’Ottaviano, and Sette (1999) gave a general definition oftranslation between logics according to which logics are characterizedas sets with consequence relations; translations are henceconsequence-relation preserving maps.

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

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

Given any intensional logic, a complete possible-worlds semantics ofthe usual variety may be viewed as a faithful embedding of that logicinto some suitably augmented many-sorted predicate logic (withquantification over possible worlds), perhaps provided with somesimple auxiliary special-purpose theory for“accessibility”, “reversal”, and so on. Ispredicate logic universal in this respect, in that every effectivelyaxiomatized 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 logicoccupies the first position as its history goes back to Aristotle, aswell as Megarians, Stoics, and other Greek philosophers. Over theyears it has been used to talk about necessity and possibility, time,and computer programs. See the entry onmodal 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-sortedlogic are that truth can be qualified (or relativized) and that modalmodels include a universe of what are called “possibleworlds”. The classical semantical concept oftruth in amodel, written as \(\mathcal{A}\models \varphi\) is now replacedbytruth at a world \(w\) in a model \(\mathcal{A}\), writtenas \(\mathcal{A},w\models \varphi\).

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

having a non-empty domain \(\mathbf{W}\) of states or worlds, a binaryaccessibility relation \(\mathbf{R}\) defined over it, and acollection of subsets of \(\mathbf{W}\) for each atomic propositionsymbol \(P\). A modal formula \(\varphi\) is true at world \(w\) inmodel \(\mathcal{A}\) (\(\varphi\) issatisfied in\(\mathcal{A}\) at world \(w\)) when the following inductiveconditions apply:

A formula \(\varphi\) isglobally true in a model\(\mathcal{A}\) if it is satisfied at all worlds in \(\mathcal{A}\)(\(\mathcal{A}\models \varphi\)). A formula \(\varphi\) isvalid 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) arethe validities of thebasic modal logic, also calledminimal modal logic orSystemK.^[12]

Blackburn and van Benthem (2007: 5) note

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

as modal formulas are evaluated at certain points. The intuition isthat the modal operator \(\square\) is a kind of universal quantifier andmodal structures are first-order relational structures with a binaryrelation and a collection of subsets of the universe. In a first-orderlanguage, to talk about these structures one needs a binary relationsymbol, \(S\), as well as a collection of unary relation symbols. Thislanguage is calledfirst-order correspondence languagebecause every basic modal formula corresponds to a first-orderformula. The standard translation of a modal formula \(\varphi\) is afirst-order formula with one free variable expressing the semantics ofmodal formulas:

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

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

From this lemma it is possible to deriveCompactness,Löwenheim-Skolem andEnumerability theorems forthe basic modal logic (Blackburn & van Benthem 2007: 11) justusing the corresponding properties of first-order logic.

The set of validities ofbasic modal logic is not onlyrecursively enumerable (as the enumerability theorem proves) but thesatisfiability problem is also decidable.We wonder, what is thegain in translating a decidable logic into an undecidable one? Are weloosing decidability? The answer is that we don’t loosedecidability; in fact, one can use translations to prove decidabilityforbasic modal logic.

Concerning translation ofbasic modal logic into first-ordercorrespondence language, there are at least two results tohighlight:

• The first relevant result is thatbasic propositional modallogic can be translated into the two variable fragment^[13] of first-order logic (formulas of first-order logic where only twovariables are used) and the satisfiability problem for the twovariable fragment is decidable.

• The second relevant result is theModal Characterization Theorem^[14] establishing, for any first-order formula with a free variable, theequivalence between being equivalent to a modal formula and beinginvariant under bisimulation (see van Benthem 2010: 26–27 for adefinition). Bisimulation is a useful result as it can be employed tomake a model \(\mathcal{A}\) as small as possible, bybisimulationconstraction, as well as to make bigger models.

However, these results apply tobasic modal logic; in thatlogic we are talking aboutsatisfiability as meaning“satisfiable on some model”, no restrictions (liketransitivity) are imposed on the accessibility relation. And for anymodal logic other thansystemK we are looking formodels with additional properties. It is true that similar method canbe applied with other propositional systems when the relevantproperties can be expressed by first-order formulas with only twovariables. Nevertheless, transitivity is a clear counter case.

Insection 5.2, a variety of modal systems are treated (includingS4, whoseaccessibility relation is reflexive and transitive) and severalmetatheorems are proved for them, by using the MSL reservoir. Thetranslation is defined into a many-sorted first-order logic with asecond-order flavor, as the many-sorted structures used in thatsection contain the relevant categories of mathematical sets (andrelations) definable in the modal logic being translated.

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

3.3 General Plan

The general plan is as follows: The signature of the logic beingstudied (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 thestructures of the logic \(\XL\) are converted into many-sortedstructures. Thus, we need to define a recursive function \(\Trans\) todo the translation and a direct conversion of structures,\(\Conv_{1}.\)

With the direct conversion of structures we want to obtain as a resultthe equivalence of validity in the original structures for \(\XL\),call them simply \(\Str(\XL)\), with validity of a certain class ofmany-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 bereplaced by the models of a set \(\Delta\) of many-sorted formulas.Thus, the key to both definitions, \(\Trans\) and \(\Conv_{1}\), is tosimplify the proof of the semantic equivalence, and in this respectthe relevance of the results obtained strongly depends on thepossibility of axiomatizing \(\mathfrak{S}^{\ast}\). In case you getsuch 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 consequencefrom \(\Delta\) in \(\MSL^{\XL}\).

In case you get the set \(\Delta\), a reverse conversion ofstructures, \(\Conv_{2}\), should be defined. And so, from many-sortedmodels of \(\Delta\) we get structures in \(\Str(\XL)\). Our goal indefining 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 theuniversal 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 directconversion of structures, \(\Conv_{1}\). Our first goal is to stateand 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 sucha \(\Delta\), at least a set satisfying \(\mathfrak{S}^{\ast}\subseteq\Mod(\Delta )\). To finish level one, one needs to prove aRepresentation theorem; namely, a statement of the followingform:

From Representation theorem it followsEnumerability for thelogic \(\XL\). Namely, the set of validities of \(\XL\) is recursivelyenumerable. Therefore, \(\XL\) is complete in an abstract sense.

Remark: So, we learn that a calculus for \(\XL\) is anatural demand, but we also learn that in MSL we can simulate such acalculus 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 logicalconsequence, we may try to prove theMain theorem; that is,that consequence in \(\XL\) (\(\Pi \models _{\Str(\XL)}\varphi\)) isequivalent to consequence of translations in MSL,modulo thetheory \(\Delta\). To prove the main theorem, the reverse conversionof structures, \(\Conv_{2}\), should be used. Our goal in defining itis to prove the following:

From the previous results, our Main Theorem follows:

Remark: We already haveEnumerability. Now,fromMain Theorem as wellCompactness andLöwenheim-Skolem for \(\MSL\), we easily obtainCompactness andLöwenheim-Skolem for \(\XL\).Therefore, the logic under investigation could have a stronglycomplete calculus. You can either define it or use the many-sortedone.

3.6 Level Three: Deductive Correspondence

When the \(\XL\) logic also comes with a deductive calculus, we cantry to use the machinery of correspondence to prove, if possible,Soundness andCompleteness for \(\XL\). In order toprove these theorems, one needs to prove aTheorem of deductivecorrespondence between the \(\XL\) calculus and the many-sortedone, modulo \(\Delta\). So, the next goal is to prove:

Since we already have theMain theorem (*), plusCompleteness andSoundness for MSL (**), once we getthisTheorem of deductive correspondence (***) the picturebelow gave usSoundness and Strong Completeness of\(\XL\):

Remark: We have reached the end of the road tocompleteness, but it is important to stress that we are using thealready proven completeness results of MSL to prove strongcompleteness 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 whichdiffers from FOL (one-sorted first-order logic) in the followingrespects: (1) alphabet, (2) standard and non-standard semantics and(3) overwhelming expressive power with standard semantics. See theentry onsecond-order and higher-order logic as well as the entry onChurch’s type theory.

The alphabet of second-order logic is obtained by including thefirst-order one-sorted variables and adding relation variables thatcan be quantified. As a result, in addition to the formula \(\forallx\varphi\) saying“for all individuals \(\varphi\) holds”, we haveformulas \(\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 variableswe need new universes whose elements are sets and relations over theuniverse of individuals, say \(\mathbf{A}.\) In the so-calledstandard semantics, a set variable ranges over the power setof the individual’s universe, \(\wp (\mathbf{A})\), and an-ary relation variable ranges over the power set of then-ary Cartesian product of the individual’s universe,\(\wp (\mathbf{A}^{n})\). To put an example of the overwhelmingexpressive 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 paya high price for the expressive power, we sacrifice the logic:Compactness fails,Löwenheim-Skolem fails andCompleteness fails (both strong and weak).

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

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

In thesemantics of frames, both sets and relation variablesare allowed to range over universes which are subsets of standarduniverses. Somehow, this condition alone does not guarantee that wehave enough sets and relations to deal with the second ordercapability. We would like to include in the universes all thedefinable ones in our formal language. This is a rather natural demandimposed to thegeneral models (Henkin models) toobtain completeness.

In fact, with the semantics of frames, the set of validities coincideswith the set of sentences derivable in a second-order calculus whichis just an extension of the first-order one obtained by adding rulesfor the new quantifiers. This many-sorted calculus was isolated byHenkin (1953) in a paper where he introduced theComprehensionSchema

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 tothe universes of the second-order structure is to be subsets ofstandard universes, there is no guarantee that they are models ofComprehension. That is why we need the general structures toobey extra rules, universes have to be closed under definability. Withgeneral structures the set of validities coincides with the set ofsentences derivable in the second-order calculus. So, we go back tothe situation encountered in first-order logic as you recover:Compactness,Löwenheim-Skolem andCompleteness.

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

is added.

What is the conclusion of these results? As you know, a logicis like a balance scale: you have expressive power in one pan andcomputability power in the other. In case you wanted to retain logicalproperties, you had to change the semantics and lose some expressivepower, you cannot have both at a maximum, they are “optimalimpossible”. One can express the same idea in a more technicalway by resorting to Lindström’s results (Lindström1969) mentioned insection 2.3.

For more information on second-order logic, see the entry onsecond-order and higher-order logic, as well as Church 1956 and Enderton 1972. Very recommended is Henkin1996 as well as some of the papers inThe Life and Work of LeonHenkin (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 “Aprilthe 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}\) aswell as two conversions of structures, direct and reverse.

First of all, we realize that second-order structures are in factmany-sorted with certain peculiarities: in most cases they are what wecalledstrict, because the intersection between any twodifferent universes is empty, but all of them are related, as they aredefined over the universe of individuals. Moreover, in the generalstructures the universes obey certain rules, like being models ofExtensionality andComprehension.

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

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

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

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

It is easy to prove the following result.

Now we ask, can we axiomatize \(\mathfrak{S}^{\ast}\)? andthe answer isYES. The structures we want to work with are\(\MSL^{\SOL}\) models ofExtensionality andComprehension withDisjoint 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]

1. The structures we want to work with are \(\MSL^{\SOL}\) models ofextensionality and comprehension with disjoint universes. So, theyhave to be models of \(\Delta\). In such a model the universes of sort\(\langle 1,\ldots ,1,0\rangle\) are not necessarily subsets of \(\wp(\mathbf{A}_{1}^{n}).\) However, \(\mathbf{A}_{1}\) and\(\mathbf{A}_{\langle 1,\ldots ,1,0\rangle }\) are related by\(\epsilon _{n}^{\mathcal{A}}\), but this relation doesn’t needto be “genuine” membership.

2. From a many-sorted structure \(\mathcal{A}\) of signature \(\Sigma^{\SOL}\) which is a model of \(\Delta\), we pass to anothermany-sorted structure \(\mathcal{B}\) of the same signature but whereuniverses of sort \(\langle 1,\ldots ,1,0\rangle\) are now subsets of\(\wp (\mathbf{B}_{1}^{n})\) and \(\epsilon _{n}^{\mathcal{B}}\) isgenuine membership. The new many-sorted structure\(\mathcal{B}\) is obtained by defining a function

   \[H:\Mod(\Delta )\rightarrow \Conv_{1}(\Str(\SOL))\]

   that follows the information given in \(\epsilon _{n}^{\mathcal{A}}\)to build \(\mathbf{B}_{\langle 1,\ldots ,1,0\rangle }\), thus\(\mathcal{B}=H(\mathcal{A})\). The new structure is basically ageneral second order structure with the genuine membership relation.^[19]

3. It is easy to see that the new structure \(\mathcal{B}\) is isomorphicto the original \(\mathcal{A}\), so \(\mathcal{A}\approxeq\mathcal{B}\).

4. From a many-sorted structure \(\mathcal{B}\in \Conv_{1}(\Str(\SOL))\)of the kind mentioned above, we define a SOL structure by an easymake-up transformation; namely, erasing the membership relations andadapting the signature to a second order one. This is just to reversethe transformation done in \(\Conv_{1}\).

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 followingsemantic theorems:

As explained insection 3.5, by usingRepresentation andMaintheorems some important metatheorems of MSL can now be transferred toSOL.

Remark: The enumerability and compactness theoremstaken together tell us that the logic under investigation could have astrongly complete calculus. In fact, we could use the many-sortedtheory \(\Delta\) to derive SOL theorems in the many-sortedcalculus.

However, in case we already had a calculus for SOL we can use themachinery of translations to prove itsSoundness andCompleteness.

4.4 Soundness and Completeness for SOL

We just follow the strategy presented on level three (insection 3.6) of our general plan to proveSoundness andCompleteness for SOL calculus. What needs to be proven is thefollowing theorem.

According to the general plan, from theMain theorem, theDeductive correspondence andSoundness andStrong Completeness of MSL, we getCompleteness andSoundness 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 orderlogic was defined by eliminating someSubstitution Rules fromthe calculus presented in Church 1956^[20] and introducingComprehension Schema. In this paper, Henkindefines two calculi \(F^{\ast}\) and \(F^{\ast \ast}\) (basically,calculi MSL and SOL): the first one is obtained from a first-ordercalculus by adding rules for the new quantifiers, while the second isa proper second-order calculus. Both calculi are incomplete withstandard semantics. Henkin mentioned that we can obtain a completenessresult for the \(F^{\ast}\) calculus with theframesemantics. In fact, we have already seen completeness for MSL andthat the second-order calculus is complete with thegeneralsemantics.

There is another interesting idea, appearing explicitly in the 1953paper, which is also useful. The idea is: If we weaken comprehension,we obtain a calculus between \(F^{\ast}\) and \(F^{\ast \ast}\). Andit 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 becomplete; the main reason being that this class of models is againaxiomatizable.

In what follows, this idea is exploited in several propositional modallogics as well as in propositional dynamic logic withKripkesemantics (see the entry onmodal logic as well as the entry onpropositional dynamic logic).

The second-order appearance mentioned in the title is as follows: whendefining the conversion of structures into MSL we will add newuniverses containing all the categories of mathematical objects youcan talk about in PML (or PDL); therefore, we add all sets andrelations defined in these logics with their respective formulas andprograms. And so, we are somehow shifting to SOL structures. We canadd as well membership relation symbols to the language and membershiprelations to the structures, as we did in the conversion of SOL intoMSL; 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 accessibilityrelation, a membership sign, and equality for individuals and sets.\(\MSL^{\PML}\) contains individual variables as well as variables forsets. The translation is standard (as insection 3.2): we express in the target logic \(\MSL^{\PML}\) the semanticalinterpretation of the formulas being translated.^[21] In particular,

The many-sorted structures we shall use are obtained from the modalstructures 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 }\) containall 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 sameset 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 generalstructures built on modal structures defined as above, our convertedstructures. It is not difficult to prove that validity of \(\varphi\)in PML is equivalent to validity of the universal closure of thetranslation of the formula in the class \(\mathfrak{G}\).

Level one for Modal LogicK

To finish the level one of the translation method, we need toaxiomatize \(\mathfrak{G}\).Is that possible? The answer ispositive for theminimal logicK (basic modallogic) as we can define a theory \(\Delta _{K}\) with theComprehension Axiom

working mainly on many-sorted formulas \(\varphi\) obtained bytranslations of modal formulas. As we wanted a second-orderappearance,Extensionality Axiom is added to \(\Delta _{K}\).As a result, we obtain aRepresentation Theorem for theminimal modal logic,K:

(in logicK the whole class of Kripke structures are used, noconditions are imposed on the accessibility relation)

As explained insection 3.4, from the previous theorem,Enumerability theorem for modallogicK is achieved. In fact, we already know much more, aswe mentioned insection 3.2 that the set of validities in systemK is decidable.

Level one for Modal LogicS4

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

TheRepresentation Theorem forS4 is easilyobtained

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

These results are relevant when we proceed further to prove theMain Theorem.^[24] From this theorem we get for freeCompactness andLöwenheim-Skolem forK andS4.

Level three for Modal LogicsK andS4

In case we wanted to prove that modal calculi forK andS4 (see the entry onmodal logic) are complete by using the completeness of MSL,DeductiveCorrespondence between the modal logic concerned and itsmany-sorted counterpart have to be proved. Proving deductivecorrespondence from propositional modal logic to many-sorted logic iseasy

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

Therefore,

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

and the soundness and completeness of the modal logics underinvestigation is reached by following the strategy explained insection 3.6.

Propositional Dynamic Logic as Many-sorted Logic

A similar method can be applied in Propositional Dynamic Logic (PDL).PDL is a modal logic initially designed to talk about states andcomputer programs, it has a complete calculus whose axioms include theusual ones in modal logicK as well as other axiomsdescribing the composition of programs (see the entry onpropositional dynamic logic). Among them, it is worth highlighting Axiom 5. This axiom is alsoknown as “induction axiom” and it is the responsible forone of the characteristic of PDL, itsuncompactness. For thisreason, the calculus of PDL is sound and complete but only in the weaksense.

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

For the conversion of structures, we follow a procedure similar to theone used in PML: we extend the Kripke model \(\mathcal{A}\) to ageneral 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. Usingthese structures, one can prove that validity of a dynamic formula isequivalent to the validity of the universal closure of its translationin the class \(\mathcal{E}\) of all many sorted structures obtained inthis way. The representation theorem is also available, once we definethe theory \(\Delta _{\PDL}\). This theory includes as axioms themany-sorted abstract conditions for the PDL axioms,Extensionality (both for sets and relations) as well asComprehension axiom for sets and relations defined bytranslations of formulas and programs.

At the end of the process, one can prove not only the semanticalequivalence of validities in PDL with consequences from \(\Delta_{\PDL}\) of the universal closure of their translations, but alsothat the dynamic calculus proves as theorems all the formulas whosetranslations 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) topresent many-sorted logic as easily convertible to one-sortedfirst-order logic. In Hao Wang (1952), the equivalence is built onprovability while in Enderton’s book it has a semanticalcharacter.

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

Syntactic translation

For the syntactic translation (known as “relativization ofquantifiers”), let \(L\) be a many-sorted language of signature\(\Sigma\), and let \(\OperSym\) be its set of operation symbols. Wethus 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-sortedlanguage \(L\) and the corresponding one-sorted one, \(L^{\ast}\), isthat 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 andsorts, in the latter they only have arity.

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

Example: As an example we will use the alreadypresented argument from theBook of PerfectEmptiness. In one-sorted first order logic we can introducethis language:

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

In order to derive the conclusion, we will need as well an extrahypothesis saying thatthe dawn of times andtodayare both times, \((Id\land It)\). We could add several formulasrelating our new predicates:

Conversion of many-sorted structures into one-sorted ones

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

The domain of \(\mathcal{A}^{\ast}\) is the union of the individualsdomains of \(\mathcal{A}\), the interpretation of the new unarypredicates \(Q_{i}\) corresponds to the old domains \(\mathbf{A}_{i}\)and so this information is kept. The interpretation of the rest ofelements in \(\OperSym\) is similar to the one they have in themany-sorted structure \(\mathcal{A}\). The only difficulty concernsoperation symbols with \(\Rank(f)=\langle i_{1},\ldots,i_{n},i_{0}\rangle\) and \(i_{0}\not=0\) because now the universe isthe 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 generatedby the above conversion.^[28]

The following theorem holds for any of these extended structures.

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

Conversion of one-sorted structures into many-sorted ones

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 problemsthat could stop the conversion: the first one is that in a many-sortedstructure all the universes should be nonempty and our idea is to takefor each sort \(i\) the unary relation \(Q_{i}^{\mathcal{E}}\) asuniverse of sort \(i\) and so we need it to be nonempty; the seconddifficulty concerns operation symbols with \(\Rank(f)=\langlei_{1},\ldots i_{n},i_{0}\rangle\) whose interpretation in structure\(\mathcal{E}\) is just ann-ary function, but we need thevalues of \(f^{\mathcal{E}}\upharpoonright(Q_{i_{1}}^{\mathcal{E}}\times \ldots \timesQ_{i_{n}}^{\mathcal{E}})\) to be in \(Q_{i_{0}}^{\mathcal{E}}\).

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

• \(\exists x\ Q_{i}x\), for each \(i\in \Sort\)
• \(\forall x_{1}\ldots x_{n}(Q_{i_{1}}x_{1}\land \ldots \landQ_{i_{n}}x_{n}\rightarrow Q_{i_{0}}(f\ x_{1}\ldots x_{n}))\), where\(\Rank(f)=\langle i_{1},\ldots ,i_{n},i_{0}\rangle\), \(f\in\OperSym\)
• \(Q_{i}c\), for each \(c\in \OperSym\) with \(\Rank(c)=i\).

Notice that the structure \(\mathcal{A}^{\ast}\) of the previoustheorem is a model of \(\Pi\). Moreover, a one-sorted model of\(\Pi\), \(\mathcal{E}\), is easily convertible into a many-sortedone, \(\mathcal{E}^{\ddag }\). We take \(Q_{i}^{\mathcal{E}}\) as theuniverse of sort \(i\), strict relations and functions are obtained asrestrictions to the corresponding domains to obtain relations andfunctions 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 followingresult.

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

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

However, other theorems about many-sorted logic are notstraightforwardly obtained from their one-sorted versions. Inparticular, interpolation in MSL requires its own proof (seesection 6.2). The concept of interpretability plays an important role for acomparison between one-sorted and many-sorted theories (seesection 6.3 and Hook 1985). Unfortunately, interpretablity between many-sortedtheories is not obtained from their one-sorted counterparts.Concerning the comparison, deductions in a many-sorted proof systemare usually shorter than the derivations we get in a one-sortedcalculus, that is one of the reasons why many-sorted logic is sofrequently 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 importantresults such us Beth’s definability theorem and Robinson theoremcould be obtained directly from it (see the entryfirst-order model theory). In the second place, interpolation can be seen as a central logicalproperty which “has been used to reveal a deep harmony betweensyntax and semantics” (Feferman 2008: 341).

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

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

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

1. \(\Rel(\varphi )\cap \Rel(\psi )\not=\varnothing\) implies thatthere is an “intermediate” formula \(\theta\) such that\(\vdash \varphi \rightarrow \theta\) and \(\vdash \theta \rightarrow\psi\) (\(\theta\) is a sentence such that \(\Rel(\theta )\subseteq\Rel(\varphi )\cap \Rel(\psi )\)) and
2. \(\Rel(\varphi )\cap \Rel(\psi )=\varnothing\) implies \(\vdash\lnot \varphi\) or \(\vdash \psi\),

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

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

As in one-sorted logic, the interpolation lemma for a many-sortedlogic 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 acorollary 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 ofinterpretability. Interpretability is a good criterion forfixing a comparison between theories \(T\) and \(T^{\prime }\), for itis characterized either in terms of “uniform definability ofmodels” or of “the existence of an interpretation mapwhich preserves logical form and provability” (Mceldowney 2020:15). It is also helpful for proving consistency, as \(T^{\prime }\) isproved to be consistent when interpreted in a consistent \(T\).However, interpretability between theories of a many-sorted signaturedoes not guarantee interpretability between their (one-sorted)translations.

Mceldowney (2020) argues that the concept of bi-interpretability isthe best measure of theoretical equivalence in MSL. The oldestcriterion for theoretical equivalence between first-order theorieswith the same signature is the notion ofdefinitionalequivalence (see Eilenberg & Mac Lane 1942, 1945 and Glymour1971). Therefore, the necessity of a many-sorted counterpart wasapparent. As a result, a debate on the nature of equivalence in MSLhas taken place since 2016. Barrett and Halvorson (2016) generalizesthe idea of definitional extension to the concept ofMoritaextension: intuitively, \(T^+\) is a Morita extension of \(T\)iff both \(T\) and \(T^+\) are MSL theories and \(T^+\) “says nomore” than the original theory (see 2016: 565 for formaldetails).

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

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

6.4 Extension of Many-sorted Logic to Sort Logic

Apart from its reduction to one-sorted logic, many-sorted first-orderlogic can be extended.Sort logic is a many-sortedsecond-order logic in which it is allowed to quantify over new sorts,“looking outside” the structure where the formula is beinginterpreted. Then, besides adding sorts to a second-order logic, wemay include a new logical symbol \(\widetilde{\exists }\) to quantifyover new sorts.

InSort logic, well-formed formulas involving\(\widetilde{\exists }\) must respect aNew Sort Condition(Väänänen 2014: 175) to guarantee that the domainswhere free variables in \(\varphi\) are interpreted do not interferewith the scope of the quantifier \(\widetilde{\exists}\). The onlynovelty concerns interpretation of formulas with the newquantifier,

In this definition, model \(\mathcal{M}^{\prime }\) is considered anX-expansion of \(\mathcal{M}\) iff it includes as many newuniverses (\(\mathbf{M}_{i_{1}}^{\prime },\ldots,\mathbf{M}_{i_{r}}^{\prime }\)) as the sorts of \(X\) requires.Moreover, the restriction of \(\mathcal{M}^{\prime }\) to the old onesis \(\mathcal{M}\).

For instance, the formula

says that there exists a new sort with a new anti-symmetric relation;somehow we are saying that anti-symmetry is a consistent concept as itcan be exemplified.

An axiomatic calculus for sort logic was introduced inVäänänen (2014), as an extension of the second-ordercase. For this reason, he incorporated a secondComprehensionAxiom related to \(\widetilde{\exists}\) together with somerestrictions concerning the rules of proof when formulas with the newquantifier \(\widetilde{\exists }\) are involved (see 2014:176–177).

As it occurs in every higher-order logic, completeness and compactnessfail for sort logic with standard semantics. Fortunately, it ispossible to build aHenkin structure satisfying bothComprehension axioms and to move to general semantics. Changingsemantics in this way results in the recovery of completeness for thementioned calculus, as Väänänen (2014: 179–80)has remarked. The proof found its inspiration in that ofHenkin’s (1950) for type theory.

Väänänen (2014: 181) applied sort logic to Foundationsof Mathematics. He proposed the notion of truth in a structure\(\mathcal{A}\)characterizable in sort logic, making a newdistinction between general truth \(\models \varphi\) and specifictruth in those structures. Whenever general truth is reduced tospecific truth, we can use the calculus to prove the satisfiability ofa formula. Under certain constraints, any class of structures closedunder isomorphism is definable in sort logic (see Kennedy &Väänänen 2021, Theorem 19). Thus,Väänänen argues that sort logic is an“alternative way of looking at mathematics”, where, unlikeset theory, “definition rather than construction is thefocus” (2014: 185). It is also an interesting tool for studyingLogicality and model classes (Kennedy &Väänänen 2021).

Bibliography

• Abadi, Aharon, Alexander Rabinovich, and Mooly Sagiv, 2007,“Decidable Fragments of Many-Sorted Logic”, inLogicfor Programming, Artificial Intelligence, and Reasoning, NachumDershowitz and Andrei Voronkov (eds.), (Lecture Notes in ComputerScience 4790), Berlin, Heidelberg: Springer Berlin Heidelberg,17–31. doi:10.1007/978-3-540-75560-9_4
• Andréka, Hajnal, István Németi, and Johan vanBenthem, 1998, “Modal Languages and Bounded Fragments ofPredicate Logic”,Journal of Philosophical Logic,27(3): 217–274. doi:10.1023/A:1004275029985
• Andréka, Hajnal, Johan van Benthem, Nick Bezhanishvili, andIstván Németi, 2014, “Changing a Semantics:Opportunism or Courage?”, in Manzano, Sain, and Alonso 2014:307–337. doi:10.1007/978-3-319-09719-0_20
• Aranda, Víctor, 2022, “Completeness: From Husserl toCarnap”,Logica Universalis, 16(1–2):57–83. doi:10.1007/s11787-021-00283-4
• Barrett, Thomas William and Hans Halvorson, 2016, “MoritaEquivalence”,The Review of Symbolic Logic, 9(3):556–582. doi:10.1017/S1755020316000186
• –––, 2017, “Quine’s Conjecture onMany-Sorted Logic”,Synthese, 194(9): 3563–3582.doi:10.1007/s11229-016-1107-z
• Blackburn, Patrick and Johan van Benthem, 2007, “ModalLogic: A Semantic Perspective”, in Blackburn, van Benthem, andWolter 2007: 1–84. doi:10.1016/S1570-2464(07)80004-8
• Blackburn, Patrick, Johan van Benthem, and Frank Wolter (eds.),2007,Handbook of Modal Logic, (Studies in Logic andPractical Reasoning 3), Amsterdam/Boston: Elsevier. [Blackburn, van Benthem, and Wolter 2007 available online]
• van Benthem, Johan, 1983,Modal Logic and ClassicalLogic, (Indices 3), Napoli: Bibliopolis.
• –––, 1984a, “Correspondence Theory”,inHandbook of Philosophical Logic, D. Gabbay and F.Guenthner (eds.), Dordrecht: Springer Netherlands, 167–247.doi:10.1007/978-94-009-6259-0_4
• –––, 1984b, “Review: B. J. Copeland. OnWhen a Semantics Is Not a Semantics: Some Reasons for Disliking theRoutley–Semantics for Relevance Logic.Journal ofPhilosophical Logic, Vol. 8 (1979), pp. 399–413”,Journal of Symbolic Logic, 49(3): 994–995.doi:10.2307/2274161
• –––, 2010,Modal Logic for Open Minds,(CSLI Lecture Notes 199), Stanford, CA: CSLI Publications.
• Carnielli, Walter A., Marcelo E. Coniglio, and Itala M. L.D’Ottaviano, 2009, “New Dimensions on Translations BetweenLogics”,Logica Universalis, 3(1): 1–18.doi:10.1007/s11787-009-0002-5
• Church, Alonzo, 1956,Introduction to Mathematical Logic,Volume 1, (Princeton Mathematical Series 17), Princeton, NJ:Princeton University Press. [Note: this was a new revised edition froma 1944 edition published as anAnnals of Mathematics Studiesvolume (no. 13).]
• Craig, William, 1957a, “Linear Reasoning. A New Form of theHerbrand-Gentzen Theorem”,Journal of Symbolic Logic,22(3): 250–268. doi:10.2307/2963593
• –––, 1957b, “Three Uses of theHerbrand-Gentzen Theorem in Relating Model Theory and ProofTheory”,Journal of Symbolic Logic, 22(3):269–285. doi:10.2307/2963594
• da Silva, Jairo J., Itala Marı́a L. D’Ottaviano,and A. M. Sette, 1999, “Translations between Logics”, inModels, Algebras, and Proofs, Xavier Caicedo and Carlos H.Montenegro (eds.), (Lecture Notes in Pure and Applied Mathematics203), New York: Marcel Dekker, 435–448.
• D’Ottaviano, Itala M. Loffredo and Hércules deAraújo Feitosa, 2019, “Translations Between Logics: ASurvey”, inPhilosophy of Logic and Mathematics: Proceedingsof the 41st International Ludwig Wittgenstein Symposium, GabrieleM. Mras, Paul Weingartner, and Bernhard Ritter (eds.), Boston/Berlin:De Gruyter, 71–90. doi:10.1515/9783110657883-005
• Ebbinghaus, Heinz-Dieter, Jörg Flum, and Wolfgang Thomas,1984,Mathematical Logic, (Undergraduate Texts inMathematics), New York: Springer-Verlag.
• Eilenberg, Samuel and Saunders MacLane, 1942, “GroupExtensions and Homology”,The Annals of Mathematics,43(4): 757–831. doi:10.2307/1968966
• –––, 1945, “General Theory of NaturalEquivalences”,Transactions of the American MathematicalSociety, 58(2): 231–294.
• Enderton, Herbert B., 1972,A Mathematical Introduction toLogic, New York: Academic Press.
• Feferman, Solomon, 1968, “Lectures on Proof Theory”,inProceedings of the Summer School in Logic Leeds, 1967, M.H. Löb (ed.), (Lecture Notes in Mathematics 70),Berlin/Heidelberg: Springer Berlin Heidelberg, 1–107.doi:10.1007/BFb0079094
• –––, 1974, “Applications of many-sortedinterpolation theorems”, inProceedings of the TarskiSymposium, L. Henkin, J. Addison, C. Chang, W. Craig, D. Scottand R. Vaught (eds.), (Proceedings of Symposia in Pure Mathematics,25), Providence, RI: AMS, pp. 205–224.
• –––, 2008, “Harmonious Logic:Craig’s Interpolation Theorem and Its Descendants”,Synthese, 164(3): 341–357.doi:10.1007/s11229-008-9354-2
• –––, 2016, “Many-sorted first-order modeltheory as a conceptual framework for biological and other complexdynamical systems”, Keynote address to theAMS/ASL sessionon applications of Logic, Model Theory, and Theoretical ComputerScience to System Biology, Seattle, 9 January 2016. [Feferman 2016 draft available online]
• Friedman, Harvey and Visser, Albert, 2014, “Whenbi-interpretability implies synonymy”,Logic Group PreprintSeries, 320: 1–19.
• Gabbay, Dov M. (ed.), 1994,What Is a Logical System?,(Studies in Logic and Computation 4), Oxford: Clarendon Press.
• –––, 1996,Labelled Deductive Systems,Volume 1, (Oxford Logic Guides 33), Oxford: Oxford UniversityPress.
• Gilmore, Paul, 1958, “An addition to ‘Logic ofMany-Sorted Theories’”,Compositio Mathematica,13: 277–281.
• Glymour, Clark, 1971, “Theoretical Realism and TheoreticalEquivalence”, inPSA: Proceedings of the Biennial Meeting ofthe Philosophy of Science Association, 1970, Roger C. Buck andRobert S. Cohen (eds.), (Boston Studies in the Philosophy of Science8), Dordrecht: Springer Netherlands, 275–288.doi:10.1007/978-94-010-3142-4_19
• Gödel, Kurt, 1931, “Über formal unentscheidbareSätze der Principia Mathematica und verwandter Systeme I”,Monatshefte für Mathematik und Physik, 38–38(1):173–198. doi:10.1007/BF01700692
• Grzegorczyk, Andrzej, 1955, “The Systems of Leśniewskiin Relation to Contemporary Logical Research”,StudiaLogica, 3(1): 77–95. doi:10.1007/BF02067248
• Henkin, Leon, 1949, “The Completeness of the First-OrderFunctional Calculus”,Journal of Symbolic Logic, 14(3):159–166. doi:10.2307/2267044
• –––, 1950, “Completeness in the Theory ofTypes”,Journal of Symbolic Logic, 15(2): 81–91.doi:10.2307/2266967
• –––, 1953, “Banishing the Rule ofSubstitution for Functional Variables”,Journal of SymbolicLogic, 18(3): 201–208. doi:10.2307/2267403
• –––, 1963a, “A Theory of PrepositionalTypes”,Fundamenta Mathematicae, 52(3): 323–344.doi:10.4064/fm-52-3-323-344
• –––, 1963b, “An Extension of theCraig-Lyndon Interpolation Theorem”,Journal of SymbolicLogic, 28(3): 201–216. doi:10.2307/2271066
• –––, 1996, “The Discovery of MyCompleteness Proofs”,Bulletin of Symbolic Logic, 2(2):127–158. doi:10.2307/421107
• Herbrand, Jacques, 1930,Recherches sur la théorie dela démonstration, PhD thesis, University of Paris.
• Hodges, Wilfrid, 1986, “Truth in a Structure”,Proceedings of the Aristotelian Society, 86(1):135–152. doi:10.1093/aristotelian/86.1.135
• –––, 1993,Model Theory, Cambridge/NewYork: Cambridge University Press. doi:10.1017/CBO9780511551574
• –––, 1998, “The Laws of Distribution forSyllogisms”,Notre Dame Journal of Formal Logic, 39(2):221–230. doi:10.1305/ndjfl/1039293064
• Hook, Julian L., 1985, “A Note on Interpretations ofMany-Sorted Theories”,Journal of Symbolic Logic,50(2): 372–374. doi:10.2307/2274223
• Kennedy, Juliette and Väänänen, Jouko, 2021,“Logicality and Model Classes”,The Bulletin ofSymbolic Logic, 27(4): 385–414.doi:10.1017/bsl.2021.42
• Kreisel, Georg and J. L. Krivine, 1967,Élémentsde logique mathématique, théorie desmodèles (Monographies de la Sociétémathématique de France 3), Paris: Dunod; translated asElements of Mathematical Logic: Model Theory (Studies inLogic and the Foundations of Mathematics), Amsterdam: North Holland,1967.
• Langford, C. H., 1939, “Review: Arnold Schmidt.‘Über deduktive Theorien mit mehreren Sorten vonGrunddingen’,Mathematische Annalen, 115. 4(1938), pp. 485–506”,Journal of Symbolic Logic,4(2): 98–98. doi:10.2307/2269080
• Liezi, (列子,El libro de la perfectavacuidad), Barcelona: Kairos, 1982. Translated directly fromChinese by Iñaki Preciado. Example translated to English forthis Entry by Ulises Tindón.
• Lindström, Per, 1969, “On Extensions of ElementaryLogic”,Theoria, 35(1): 1–11.doi:10.1111/j.1755-2567.1969.tb00356.x
• Lyndon, Roger C., 1959, “An Interpolation Theorem in thePredicate Calculus”,Pacific Journal of Mathematics,9(1): 129–142.
• Manzano, María, 1989 [1999],Teoría demodelos, Madrid: Alianza Editorial. Translated asModelTheory, Ruy J. G. B. de Queiroz (trans.), (Oxford Logic Guides37), Oxford/New York: Clarendon Press ; Oxford University Press,1999.
• –––, 1993, “Introduction to Many-sortedlogic”, Meinke and Tucker 1993: 3–86.
• –––, 1996,Extensions of First OrderLogic, (Cambridge Tracts in Theoretical Computer Science 19),Cambridge/New York: Cambridge University Press.
• –––, 2014a, “April the 19th”, inManzano, Sain, and Alonso 2014: 265–278.doi:10.1007/978-3-319-09719-0_18
• –––, 2014b, “Henkin onCompleteness”, in Manzano, Sain, and Alonso 2014: 149–175.doi:10.1007/978-3-319-09719-0_12
• Manzano, Maria and Enrique Alonso, 2014, “Completeness: FromGödel to Henkin”,History and Philosophy of Logic,35(1): 50–75. doi:10.1080/01445340.2013.816555
• Manzano, María, Ildikó Sain, and Enrique Alonso(eds.), 2014,The Life and Work of Leon Henkin, (Studies inUniversal Logic), Cham: Springer International Publishing.doi:10.1007/978-3-319-09719-0
• Martí-Oliet, Narciso and José Meseguer, 1994,“General Logics and Logical Frameworks”, inWhat Is aLogical System?, Dov M. Gabbay (ed.), Oxford: Clarendon Press,355–391.
• Mceldowney, Paul Anh, 2020, “On Morita Equivalence andInterpretability”,The Review of Symbolic Logic, 13(2):388–415. doi:10.1017/S1755020319000303
• Meinke, Karl and John Tucker (eds.), 1993,Many-Sorted Logicand Its Applications, (Wiley Professional Computing),Chichester/New York: Wiley.
• Meseguer, José, 1989, “General Logics”, inLogic Colloquium’87: Proceedings of the Colloquium Held inGranada, H.-D. Ebbinghaus, J. Fernandez-Prida, M. Garrido, D.Lascar, and M. Rodriquez Artalejo (eds.), (Studies in Logic and theFoundations of Mathematics 129), Amsterdam: North-Holland,275–329. doi:10.1016/S0049-237X(08)70132-0
• Otto, Martin, 2000, “An Interpolation Theorem”,Bulletin of Symbolic Logic, 6(4): 447–462.doi:10.2307/420966
• Quine, Willard Van Orman, 1940,Mathematical Logic, NewYork: W. W. Norton & Company.
• Schmidt, Arnold, 1938, “Über deduktive Theorien mitmehreren Sorten von Grunddingen”,MathematischeAnnalen, 115(4): 485–506. doi:10.1007/BF01448954
• Tarski, Alfred, 1933 [1983],Pojęcie prawdy wjęzykach nauk dedukcyjnych, (Prace Towarzystwa NaukowegoWarszawskiego, Wydzial III Nauk Matematyczno-Fizycznych, 34), Warsaw:Nakładem Towarzystwa Naukowego Warszawskiego. Translated as“The Concept of Truth in Formalized Languages”, J.H.Woodger (trans.), inLogic, Semantics, Metamathematics,second edition, J. Corcoran (ed.), Indianapolis, IN: Hackett, 1983,152–278.
• Tarski, Alfred and Robert Lawson Vaught, 1956, “ArithmeticalExtensions of Relational Systems”,CompositioMathematica, 13: 81–102.
• Väänänen, Jouko, 1979, “Abstract Logic andSet Theory. I. Definability”, inLogic Colloquium ’78:Proceedings of the Colloquium Held in Mons, Maurice Boffa,Dirkvan Dalen, and Kenneth Mcaloon (eds.), (Studies in Logic and theFoundations of Mathematics 97), Amsterdam: Elsevier, 391–421.doi:10.1016/S0049-237X(08)71637-9
• –––, 1982, “Abstract Logic and Set Theory.II. Large Cardinals”,Journal of Symbolic Logic, 47(2):335–346. doi:10.2307/2273145
• –––, 2014, “Sort Logic and Foundations ofMathematics”, inInfinity and Truth, by Chitat Chong,Qi Feng, Theodore A Slaman, and W Hugh Woodin, (Lecture Notes Series,Institute for Mathematical Sciences, National University of Singapore25), Singapore: World Scientific, 171–186.doi:10.1142/9789814571043_0005
• Wang, Hao, 1952, “Logic of Many-Sorted Theories”,Journal of Symbolic Logic, 17(2): 105–116.doi:10.2307/2266241

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

[Please contact the author with suggestions.]

Related Entries

logic: classical |logic: modal |logic: propositional dynamic |logic: second-order and higher-order |model theory |model theory: first-order |reasoning: automated |Tarski, Alfred: truth definitions |type theory: Church’s type theory