## 1. Syntax and Semantics


### 1.1 Examples



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


#### Example: Euclid's first principle



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



*A straight line can be drawn joining any two points.*



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

 
\[\forall x\;\forall y(x\not=y\rightarrow \exists X(\Join(Xxy)\land \forall Y(\Join(Yxy)\rightarrow X=Y)))\]


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

 
\[\Join(Yxy):= Y \textrm{ joins } x \textrm{ and } y\]


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


#### Example: Binary relations



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



*Every asymmetric binary relation is also anti-symmetric.*



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

 
\[\Asymm(R):=\forall x\, \forall y(Rxy\rightarrow \lnot Ryx)\]


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

 
\[\Antisymm(R):=\forall x\,\forall y(Rxy\land Ryx\rightarrow x=y)\]


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

 
\[\Asymm(R)\rightarrow \Antisymm(R)\]


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



\[\forall X^{2}(\Asymm(X^{2})\rightarrow \Antisymm(X^{2}))\]


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

 
\[\Asymm(X^{2}):=\forall x\,\forall y(\epsilon \_{2} xyX^{2}\rightarrow \lnot \epsilon\_{2} yxX^{2})\]


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



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

 
\[\forall X^{2}(\Asymm(X^{2})\rightarrow \Antisymm(X^{2}))\]


is a theorem of the many-sorted theory mentioned.


#### Example: Comprehension Axiom



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



*Every property has a negation.*



we could use second order logic and write:

 
\[\forall X\,\exists Y\,\forall x(Yx\leftrightarrow \lnot Xx)\]


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



\[\forall X\,\exists Y\,\forall x(\epsilon \_{1}xY\leftrightarrow \lnot \epsilon \_{1}xX)\]


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



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



\[\exists Y^{n}\,\forall x\_{1}\ldots\forall x\_{n}(Y^{n}x\_{1}\ldots x\_{n}\leftrightarrow \varphi )\]


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



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




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

 
\[\forall x\,\forall y(x\not=y\rightarrow \exists X(\Join(Xxy)\land \forall Y(\Join(Yxy)\rightarrow X=Y)))\]


now becomes

 
\[\begin{multline}
\forall x\,\forall y(Px\land Py\land x\not=y\rightarrow \\
 \exists z((Lz\land \Join(zxy))\land \forall w((Lw\land \Join(wxy))\rightarrow z=w))) 
\end{multline}\]


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

 
\[\forall x(Px\rightarrow \exists y(Py\land \forall z(Oz\rightarrow (\epsilon \_{1}zx\leftrightarrow \lnot \epsilon \_{1}zy))))\]


where

 
\[\begin{align}
Px & :=\text{ asserts that }x\text{ is a property}\\
 Ox&:=\text{ asserts that }x\text{ is an object} \\
 \epsilon \_{1}zx &:=\text{ asserts that }z\text{ belongs to (exemplifies or instantiates) }x 
\end{align}\]


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

 
\[\forall x\,\forall y(\epsilon \_{1}xy\rightarrow Ox\land Py)\\
 \forall x(Px\rightarrow \lnot Ox)\]

### 1.2 Fundamental Ideas



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


* **Structures:** A many-sorted structure has several
non-empty domains, one for each sort, and variables of a given sort
take values over the corresponding domain. An *n*-ary relation
could be freely established between elements of different domains or
only between certain ones. These two options are called
*liberal* and *strict*. A liberal relation may relate
objects of arbitrary domains and only the arity (a natural number) has
to be stated. For a strict relation, the sorts
involved 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 a
set called \(\OperSym\), as well as an infinite number of variables
for each sort \(s\_{i}\in \Sort\), and the corresponding sets of
variables are disjoint. An *n*-ary relation symbol \(R\) could
be strict or liberal and, in the first case, we must provide
information about what are the involved sorts. To achieve this
requirement, we define a function \(\Rank\) having as domain the set
\(\OperSym\) and whose values are either natural numbers other than
zero (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 \(\langle
i\_{1},\ldots,i\_{m},i\_{0}\rangle\), with \(i\_{0},i\_{1},\ldots,i\_{m}\in
\Sort\cup \{ 0\}\). When \(f\) is an *m*-ary predicate,
\(i\_{0}=0\), and \(i\_{0}\not=0\) for *m*-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 a *signature \(\Sigma\)* we mean
the ordered triple

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


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



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


### 1.3 Formal Language


#### Terms and Formulas



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



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



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



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


#### Free and bound variables



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


#### Example: The Book of Perfect Emptiness


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





**The Book of Perfect Emptiness:** Tang
of Ying asked Ge: "Did things exist at the dawn of
time?"



Xia Ge answered: "If things had not existed at the dawn of time,
how could they possibly exist today? By the same token, men in the
future could believe that things did not exist today".




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



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



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



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



* \(\alpha :=\) If things exist at a given point in time, then at
any given previous moment in time things must have existed.
* \(\beta :=\) Things exist today.
* \(\gamma :=\) The dawn of time is previous to all else.
* \(\delta :=\) Things existed at the dawn of time.




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

 
\[\begin{align}
\Rank(E) & =\langle i,\tau ,0\rangle,\\
 \Rank(P) & =\langle \tau ,\tau ,0\rangle \textrm{ and}\\
 \Rank(d) & =\tau =\Rank(t).\\
 
\end{align} \]


The argument now reads:

 
\[\begin{align}
\alpha & :=\forall x^{\tau }(\exists y^{i}Ey^{i}x^{\tau }\rightarrow \forall z^{\tau }(Pz^{\tau }x^{\tau }\rightarrow \exists v^{i}Ev^{i}z^{\tau }))\\
 \beta & :=\exists y^{i}Ey^{i}t \\
 \gamma & :=\forall y^{\tau }\ Pdy^{\tau }\\
 \delta & :=\exists x^{i}Ex^{i}d 
\end{align} \]


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


### 1.4 Many-sorted Structures



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



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


#### Examples of many-sorted structures


* An appropriate structure \(\mathcal{E}\) for the example in
**The 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, a
binary relation between objects and instants, and a binary temporal
relation 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-order *standard structure* (or *full
structure*)

 
\[\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 includes
the domain of individuals \(\mathbf{A}\) as well as a family of second
order domains of *n*-ary relations on individuals, \(\wp
(\mathbf{A}^{n})\), for each natural number \(n\). The relations and
functions in \(\langle f^{\mathcal{A}}\rangle \_{f\in \OperSym}\) are
first-order relations and functions defined over the universe of
individuals (for more details about second-order logic, see the entry
on
 second-order and higher-order Logic).
* A second-order *general 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 standard
structures, \(\mathcal{A}\) contains the domain of individuals
\(\mathbf{A}\) as well as domains of *n*-ary relations for each
natural number, \(\mathbf{A}\_{n}\subseteq \wp (\mathbf{A}^{n})\). But
since \(\mathcal{A}\) is a general structure, the universes
\(\mathbf{A}\_{n}\) are not arbitrarily chosen, for the reason that
they must satisfy the *Comprehension Schema*. Therefore, the
universes are closed under definability (more information on general
structures in
 section 4.1).


#### Many-sorted structures



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



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



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


#### Relations of similarity between structures



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

 
\[\pi \left(f^{\mathcal{A}}\left(\mathbf{a}\_{i},\dots ,\mathbf{a}\_{m}\right)\right)=f^{\mathcal{A}^{\prime }}\left(\pi \left(\mathbf{a}\_{i}\right),\dots ,\pi \left(\mathbf{a}\_{m}\right)\right)\]


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



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



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



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


### 1.5 Semantics


#### Denotation of Terms and Satisfaction of Formulas



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



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


#### Denotation of terms



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

 
\[\mathcal{I}(f\ \tau \_{1}\ldots \tau \_{n})=f^{\mathcal{A}}(\mathcal{I}(\tau \_{1})\ldots \mathcal{I}(\tau \_{n})).\]


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




**Definition (Tarski's Truth).** The definition is
nearly the same as in classical first-order logic, see the entry on
 classical logic.



For atomic formulas: \(\mathcal{A}, s\models R\tau \_{1}\ldots \tau
\_{n}\) if and only if

 
\[\langle \mathcal{I}(\tau \_{1}),\ldots ,\mathcal{I}(\tau \_{n})\rangle \in R^{\mathcal{A}},\]


and \(\mathcal{A},s\models \tau \_{1}\approx \tau \_{2}\) if and only if
both terms denote the same object in structure \(\mathcal{A}\);
namely, \(\mathcal{I}(\tau \_{1})=\mathcal{I}(\tau \_{2})\).




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


#### Coincidence lemma



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



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

 
\[\mathcal{A}\models \varphi \left[ \mathbf{x}\_{1},\ldots ,\mathbf{x}\_{n}\right]\]


instead of

 
\[\mathcal{A},s\left( \mathbf{x}\_{1}/x\_{1},\ldots ,\mathbf{x}\_{n}/x\_{n}\right) \models \varphi.\]


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



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



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

 
\[\begin{align}
\Mod(\Gamma ) &=\{ \Sigma \text{ structure }\mathcal{A}:\mathcal{A}\models \Gamma \} \\
 \Th(\mathcal{A}) &= \{ \varphi \in \Sent(L):\mathcal{A}\models \varphi \} 
\end{align}\]

#### Elementary embedding



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

 
\[ \mathcal{A\models \varphi \lbrack }\mathbf{x}\_{1},\ldots, \mathbf{x}\_{n}] \textrm{ if and only if } \mathcal{A}^{\prime }\mathcal{\models \varphi \lbrack }\pi (\mathbf{x}\_{1}),\ldots \pi (\mathbf{x}\_{n})] \]


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



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


#### Satisfiability, Validity, and Consequence



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



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



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




**Theory:** Given a set of sentences \(\Gamma\) of a
language \(L\) we say that \(\Gamma\) *is a
 theory*[6]
 if and only if it is closed under consequence; that is, for every
\(\varphi \in \Sent(L)\): If \(\Gamma \models \varphi\) then \(\varphi
\in \Gamma\).



## 2. Calculus


### 2.1 Deductive Calculi



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



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



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



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



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


#### Maximal consistency and the property of having witnesses



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



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


### 2.2 Completeness Notions



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



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



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


### 2.3 Completeness of Many-sorted Logic



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


1. Every consistent set of formulas can be extended to a maximal
consistent set with witnesses.
2. Once we have the maximal consistent set with witnesses, we use it as a
guide to build the precise model described by formulas of this set.
The reason being that a maximally consistent set is a very detailed
description of a structure.



By doing that we prove:




**Henkin's theorem:** If \(\Gamma \subseteq \
Form(L)\) is consistent, then \(\Gamma\) has a countable
 model.[9]




The completeness theorem




**Strong completeness:** If \(\Gamma \models \varphi\)
then \(\Gamma \vdash \varphi\)




follows easily from it.



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



As corollaries of the previous results one gets:




**Weak completeness:** If \(\models \varphi\) then
\(\vdash \varphi\).





**Compactness theorem:** \(\Gamma\) has a model iff every
finite subset of it has a model.





**Lowenheim-Skolem:** If \(\Gamma\) has a model,
then it has a countable model.




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



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


### 2.4 Automated Theorem Provers



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



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



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



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



Church's simple type theory usually starts with base types
"i" (individuals/entities) and "o" (Booleans)
only and then iteratively defines all function types (such as "\(\text{i}
= > \text{o}\)",  "\(\text{i}=>\text{i}\)",
"\(\text{o}=>\text{o}\)",
"\(\text{i}=>(\text{i}=>\text{o})\)",
etc.) starting from those. But in fact one can have arbitrary many
base types \(i\_1\), \(i\_2\), \(i\_3\),..., \(i\_n\) and apply an
analogous construction. These base types \(i\_1\), \(i\_2\),
\(i\_3\),..., \(i\_n\) can be considered as sorts.



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




thf(sortForObjects, type, (object: $tType)).
  

thf(sortForTimes, type, (time: $tType)).
  

thf(constantDawn, type, (dawn: time)).
  

thf(constantToday, type, (today: time)).
  

thf(constantIsExistsAt, type, 
  
  (existsAt: object\(>\)time\(>\)$o)).
  

thf(constantPrecedesTo, type, 
  
  (precedesTo: time\(>\)time\(>\)$o)).
  

thf(axiom1, axiom, (![X:time]: 
  
  ((?[Y:object]: (existsAt @Y@X))
  
  =\(>\) (![Z:time]: ((precedesTo @Z@X) 
  
  =\(>\) (?[V:object]: (existsAt @V@Z))))))).
  

thf(axiom2, axiom, 
  
  (?[Y:object]: (existsAt @Y@today))).
  

thf(axiom3, axiom, 
  
  (![Y:time]: (precedesTo @dawn@Y))).
  

thf(conjecture1, conjecture, 
  
  (?[X:object]: (existsAt @X@dawn))).




## 3. Many-sorted Logic as a Unifying Framework


### 3.1 Translations



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



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


#### Translations



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


1. From a *proof-theoretical* point of view, the style of
comparing logics will rest upon deductive calculi. The "labelled
deductive systems" of Dov Gabbay (1994 and 1996) emerge.
2. From a *model-theoretical perspective*, one will presumably
compare logics by defining relations between the structures those
logics are attempting to describe, as in the correspondence theory of
Johan van Benthem (1983, 1984a, and 2010).
3. From a *suprastructural* point of view, we define morphisms
between categories. Among the abstract approaches to logic we
highlight the "general logics" of Jose Meseguer
(1989) as well as the "rewriting logic" of Narciso
Marti-Oliet and Jose Meseguer (1994). Da Silva,
D'Ottaviano, and Sette (1999) gave a general definition of
translation between logics according to which logics are characterized
as sets with consequence relations; translations are hence
consequence-relation preserving maps.



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



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



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


### 3.2 Correspondence Language for Basic Modal Language



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



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



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

 
\[\mathcal{A}=\langle \mathbf{W},\mathbf{R},\langle P^{\mathcal{A}}\rangle \_{P\in \Atom}\rangle\]


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

 
\[\begin{align}
\mathcal{A},w & \models P&& \text{ iff } w\in P^{\mathcal{A}}\\
 \mathcal{A},w&\not\models \bot&& \text{ for all } w \\
 \mathcal{A},w&\models \lnot \varphi&& \text{ iff not } \mathcal{A},w\models \varphi\\
 \mathcal{A},w&\models \varphi \land \psi&& \text{ iff } \mathcal{A},w\models \varphi \text{ and } \mathcal{A},w\models \psi \\
 \mathcal{A},w&\models \square \varphi&& \text{ iff for all } v \text{ such that } \langle w,v\rangle \in \mathbf{R}: \mathcal{A},v\models \varphi 
\end{align} \]


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



Blackburn and van Benthem (2007: 5) note



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



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

 
\[\begin{align}
\ST\_{x}(P)& :=Px\\
 \ST\_{x}(\bot ) & :=x\not=x \\
 \ST\_{x}(\lnot \varphi )& :=\lnot \ST\_{x}(\varphi )\\
 \ST\_{x}(\varphi \land \psi )& :=\ST\_{x}(\varphi )\land \ST\_{x}(\psi ) \\
 \ST\_{x}(\square \varphi )& :=\forall y(Sxy\rightarrow \lbrack y/x]\ST\_{y}(\varphi ))\text{, where }y\text{ is a new variable.} 
\end{align} \]


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




**Switch Lemma:** \(\mathcal{A},w\models \varphi\) iff
\(\mathcal{A}\ \models \ST\_{x}(\mathcal{\varphi )}[x:=w]\)




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



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



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



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


* The first relevant result is that *basic propositional modal
logic* can be translated into the two variable
 fragment[13]
 of first-order logic (formulas of first-order logic where only two
variables are used) and the satisfiability problem for the two
variable fragment is decidable.


* The second relevant result is the *Modal Characterization
 Theorem*[14]
 establishing, for any first-order formula with a free variable, the
equivalence between being equivalent to a modal formula and being
invariant under bisimulation (see van Benthem 2010: 26-27 for a
definition). Bisimulation is a useful result as it can be employed to
make a model \(\mathcal{A}\) as small as possible, by *bisimulation
constraction*, as well as to make bigger models.



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



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



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


### 3.3 General Plan



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



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



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



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


### 3.4 Level One: Representation Theorems



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




**Theorem 1:** For every sentence \(\varphi\) of the
\(\XL\) logic,

 
\[\models \_{\Str(\XL)}\varphi \text{ in } \XL \text{ iff } \models \_{\mathfrak{S}^{\ast}}\forall \Trans(\varphi )\text{ in }\MSL\]


where \(\forall \Trans(\varphi )\) is the universal closure of
\(\Trans(\varphi )\) and
\(\mathfrak{S}^{\ast}=\Conv\_{1}\Str(\XL)\).




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




**Representation theorem:** There is a recursive set of
many-sorted sentences \(\Delta\), with \(\mathfrak{S}^{\ast}\subseteq
\Mod(\Delta )\), and such that

 
\[\models \_{\Str(\XL)}\varphi \text{ in } \XL \text{ iff } \Delta \models \_{\Str(\MSL^{\XL})}\forall \Trans(\varphi )\text{ in }\MSL\]


for every sentence \(\varphi\) of the \(\XL\) logic.




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



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


### 3.5 Level Two: the Main Theorem



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




**Lemma 2:** For any \(\varphi \in \Sent(\XL)\) and
\(\mathcal{B} \in \Mod(\Delta )\)

 
\[\Conv\_{2}(\mathcal{B)}\models \varphi \text{ iff } \mathcal{B}\models \forall \Trans(\varphi )\]


where \(\forall \Trans(\varphi )\) is the universal closure of
\(\Trans(\varphi )\).




From the previous results, our Main Theorem follows:




**Main Theorem:** There is a recursive set \(\Delta
\subseteq \Sent(L^{\ast})\) with \(\mathfrak{S}^{\ast}\subseteq
\Mod(\Delta )\), such that

 
\[\Pi \models\_{\Str(\XL)}\varphi \text{ iff } \Trans(\Pi )\cup \Delta \models \_{\Str(\MXL^{\ast})}\Trans(\varphi )\]


for all \(\Pi \cup \{\varphi \}\subseteq \Sent(\XL)\).





**Corollary:** *Compactness* and
*Lowenheim-Skolem* for \(\XL\).




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


### 3.6 Level Three: Deductive Correspondence



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




**Theorem of deductive correspondence:** Let \(\Delta\)
be defined as in the Main Theorem, then:

 
\[\Trans(\Pi )\cup \Delta \vdash \_{\MSL}\Trans(\varphi )\text{ if and only if } \Pi \vdash \_{\XL}\varphi .\]



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

 
\[ \begin{align}
\Trans(\Pi )\cup \Delta \models\_{\Str(\MSL)} \Trans(\varphi ) & \Longleftrightarrow \Pi \models \_{\Str(\XL)}\varphi \tag{\*} \\
 \Updownarrow \qquad\qquad\qquad \tag{\*\*} \\
 \Trans(\Pi )\cup \Delta \vdash\_{\MSL} \Trans(\varphi ) & \Longleftrightarrow \Pi \vdash \_{\XL}\varphi \tag{\*\*\*} \\
 
\end{align} \]



**Corollary:** *Soundness and Strong Completeness*
of \(\XL\):

 
\[\Pi \models \_{\Str(\XL)}\varphi \text{ if and only if }\Pi \vdash \_{\XL}\varphi\]



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


## 4. Second-order Logic as Many-sorted Logic


### 4.1 Second-order Logic



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



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



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

 
\[\forall X(Xc\land \forall x(Xx\rightarrow X\sigma x)\rightarrow \forall xXx)\]


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



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

 
\[\mathfrak{SS}\subseteq \mathfrak{GS}\subseteq \mathfrak{F}\]


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


 
\[\Val\_{\mathfrak{F}}\subseteq \Val\_{\mathfrak{GS}}\subseteq \Val\_{\mathfrak{SS}}\]


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



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

 
\[\exists X^{n}\forall x\_{1}\ldots x\_{n}(X^{n}x\_{1}\ldots x\_{n}\leftrightarrow \varphi )\]


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



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

 
\[\forall X^{n}Y^{n}(X^{n}\approx X^{n}\leftrightarrow \forall x\_{1}\ldots x\_{n}(X^{n}x\_{1}\ldots x\_{n}\leftrightarrow X^{n}x\_{1}\ldots x\_{n}))\]


is added.



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



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


### 4.2 Translation of Formulas and Conversion of Structures



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



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



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



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

 
\[\Trans^{\SOL}(X^{n}x\_{1}\ldots x\_{n}):=\epsilon \_{n}x\_{1}\ldots x\_{n}X^{n}\]


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

 
\[\epsilon \_{n}^{\mathcal{A}^{\ast}}=\{\langle \mathbf{x}\_{1}\mathbf{,\ldots ,x}\_{n}\mathbf{,X}^{n}\rangle \in \mathbf{A}^{n}\times \mathbf{A}\_{n}:\mathbf{\langle x}\_{1}\mathbf{,\ldots ,x}\_{n}\mathbf{\rangle \in X}^{n}\}\]


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



It is easy to prove the following result.




**Proposition:** For every sentence \(\varphi\) of
SOL:

 
\[\models \_{\mathcal{G}.\mathcal{S}}\varphi \text{ in }\SOL\text{ if and only if }\models \_{\mathfrak{S}^{\ast}}\Trans^{\SOL}(\varphi )\text{ in }\MSL^{\SOL}\]


(where \(\models \_{\mathcal{G}.\mathcal{S}}\varphi\) means validity
with general structures and
\(\mathfrak{S}^{\ast}=\Conv\_{1}(\Str(\SOL))\))




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


\[\begin{align}
\Ext^{(n)} & :=\forall X^{n}Y^{n}(\forall x\_{1}\ldots x\_{n}(\epsilon \_{n}x\_{1}\ldots x\_{n}X^{n}\leftrightarrow \epsilon \_{n}x\_{1}\ldots x\_{n}Y^{n})\\
 & \qquad\qquad \rightarrow X^{n}\approx Y^{n}) \\
 \forall \Comph\_{\varphi }^{(n)} & :=\forall \exists X^{n}\forall x\_{1}\ldots x\_{n}(\epsilon \_{n}x\_{1}\ldots x\_{n}X^{n}\leftrightarrow \varphi ) \\
 \Disj\_{n,m} &:=\lnot \exists X^{n}Y^{m}X^{n}\approx Y^{m}\;(\text{for }n\neq m) \\
 
\end{align}\]


*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 of
extensionality and comprehension with disjoint universes. So, they
have 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 need
to be "genuine" membership.
2. From a many-sorted structure \(\mathcal{A}\) of signature \(\Sigma
^{\SOL}\) which is a model of \(\Delta\), we pass to another
many-sorted structure \(\mathcal{B}\) of the same signature but where
universes of sort \(\langle 1,\ldots ,1,0\rangle\) are now subsets of
\(\wp (\mathbf{B}\_{1}^{n})\) and \(\epsilon \_{n}^{\mathcal{B}}\) is
*genuine* 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 a
general second order structure with the genuine membership
 relation.[19]
3. It is easy to see that the new structure \(\mathcal{B}\) is isomorphic
to 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 easy
make-up transformation; namely, erasing the membership relations and
adapting the signature to a second order one. This is just to reverse
the 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.




**Definition:** \(\Conv\_{2}=\Conv\_{1}^{-1}\circ H\).




With all these definitions at hand, we now prove:




**Proposition:** for every many-sorted structure
\(\mathcal{C}\in \Mod(\Delta )\) there is a SOL-structure
\(\Conv\_{2}(\mathcal{C})\in \Str(\SOL)\) such that




\(\Conv\_{2}(\mathcal{C})\) is a model of \(\varphi\) if and only if
\(\mathcal{C}\) is a model of \(\Trans^{\SOL}(\varphi)\)




for all sentences of SOL.



### 4.3 Semantic Theorems Relating SOL and MSL



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




**Representation theorem:** For every sentence
\(\varphi\) of SOL: \(\models \_{\mathfrak{G.S}}\varphi\) in SOL
iff

 
\[\Delta \models\_{\MSL} \Trans^{\SOL}(\varphi )\]


in \(\MSL^{\SOL}.\)





**Main theorem:** \(\Pi \models
\_{\mathfrak{G.S}}\varphi\) in SOL if and only if

 
\[\Trans^{\SOL}(\Pi )\cup \Delta \models \_{\MSL} \Trans(\varphi )\]


in \(\MSL^{\SOL}\).




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




**Theorem:** SOL with general semantics has the following
properties: *Enumerability*, *Compactness* and
*Lowenheim-Skolem*.




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



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


### 4.4 Soundness and Completeness for SOL



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




**Theorem of deductive correspondence**: \(\Pi \vdash
\_{\SOL}\varphi\) in second order calculus iff

 
\[\Trans^{\SOL}(\Pi )\cup \Delta \vdash \_{\MSL} \Trans^{\SOL}\mathbf{(}\varphi \mathbf{)}\]


in many-sorted calculus, MSL.




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




**Strong Completeness and Soundness**: \(\Pi \models
\_{\mathcal{G}. \mathcal{S}}\varphi\) iff \(\Pi \vdash \_{\SOL}\varphi\)
for all \(\Pi \cup \{\varphi \}\subseteq \Sent(L\_{2}).\)



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


### 5.1 General Plan



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



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



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



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


### 5.2 Propositional Modal Logics as Many-sorted Logic



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

 
\[\begin{align}
\Trans(P)[u]& :=Pu \\
 \Trans(\square \varphi )[u]& :=\forall v(Suv\rightarrow \Trans(\varphi )[v]) 
\end{align}\]


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

 
\[\mathcal{A}=\langle \mathbf{W},\mathbf{R},\langle P^{\mathcal{A}}\rangle \_{P\in \Atom}\rangle\]


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

 
\[\mathcal{AG}=\langle \mathbf{W},\mathbf{W}^{\prime },\mathbf{R},\epsilon \_{1}^{\mathcal{A}},\langle P^{\mathcal{A}}\rangle \_{P\in \Atom}\rangle\]


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



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


#### Level one for Modal Logic *K*



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

 
\[\forall \exists X\,\forall u(\varepsilon \_{1}uX\leftrightarrow \varphi )\text{ }\]


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

 
\[\models \varphi \text{ in } \PML \Longleftrightarrow \Delta \_{K}\models \forall u\Trans(\varphi )[u]\text{ in }\MSL\]


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



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


#### Level one for Modal Logic *S*4



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

 
\[\begin{align}
\Delta \_{K} \vdash \MS(T) &\leftrightarrow \textrm{Reflexivity} \\
 \Delta \_{K} \vdash \MS(4) &\leftrightarrow \textrm{Transitivity} 
\end{align}\]


The *Representation Theorem* for *S*4 is easily
obtained




\(\models \_{\mathfrak{D}}\varphi\) in \(\PML \Longleftrightarrow
\Delta \_{S4}\models \forall u\Trans(\varphi )[u]\) in \(\MSL\)




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



These results are relevant when we proceed further to prove the
*Main
 Theorem*.[24]
 From this theorem we get for free *Compactness* and
*Lowenheim-Skolem* for *K* and *S*4.


#### Level three for Modal Logics *K* and *S*4



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

 
\[\begin{align}
\Pi \vdash \_{K}\varphi & \Rightarrow \Trans(\Pi )\cup \Delta \_{K}\vdash \Trans(\varphi ) \\
 \Pi \vdash \_{S4}\varphi & \Rightarrow \Trans(\Pi )\cup \Delta \_{S4}\vdash \Trans(\varphi ) 
\end{align} \]


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



Therefore,

 
\[\begin{align}
\mathcal{B}\_{K}\mathfrak{G}\models \forall u(\Trans(\varphi )[u]) & \Rightarrow \vdash \_{K}\varphi \\
 \mathcal{B}\_{S4}\mathfrak{G}\models \forall u(\Trans(\varphi )[u]) & \Rightarrow \vdash \_{S4}\varphi 
\end{align} \]


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

 
\[\begin{align}
\Pi \vdash \_{K}\varphi & \Longleftrightarrow \Trans(\Pi )\cup \Delta \_{K}\vdash \Trans(\varphi ) \\
 \Pi \vdash \_{S4}\varphi & \Longleftrightarrow \Trans(\Pi )\cup \Delta \_{S4}\vdash \Trans(\varphi ) 
\end{align} \]


and the soundness and completeness of the modal logics under
investigation is reached by following the strategy explained in
 section 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 and
computer programs, it has a complete calculus whose axioms include the
usual ones in modal logic *K* as well as other axioms
describing the composition of programs (see the entry on
 propositional dynamic logic).
 Among them, it is worth highlighting Axiom 5. This axiom is also
known as "induction axiom" and it is the responsible for
one of the characteristic of PDL, its *uncompactness*. For this
reason, the calculus of PDL is sound and complete but only in the weak
sense.



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



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



\[\mathcal{AE}=\langle \mathbf{W},\mathbf{W}^{\prime },\mathbf{W}^{\prime \prime },\mathbf{R},\epsilon \_{1}^{\mathcal{A}},\epsilon \_{2}^{\mathcal{A}},\langle P^{\mathcal{A}}\rangle \_{P\in \Atom}\rangle\]


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



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



\[\begin{align}
\models \varphi & \Longleftrightarrow \Delta \_{\PDL}\models \forall u\Trans(\varphi )[u] \\
 \vdash \_{\PDL}\varphi & \Longleftrightarrow \Delta \_{\PDL}\vdash \_{\MSL}\forall u\Trans(\varphi )[u] 
\end{align} \]


Weak completeness follows
 directly.[27]


## 6. Further Results


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



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



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


#### Syntactic translation



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

 
\[\OperSym^{\ast} = \OperSym\cup \{Q\_{i}:i\in \Sort\}.\]


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



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

 
\[ \Trans(\exists x^{i}\phi ) := \exists x^{i}(Q^{i}x^{i}\land \Trans(\phi )) \]


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

 
\[\begin{align}
Exy & :=x \textit{ exists at instant } y \\
 Pxy & :=x \textit{ is previous to } y \\
 Ox & :=x \textit{ is an object} \\
 Ix & := x \textit{ is a time} \\
 d & := \textit{the dawn of times} \\
 t &:= \textit{today}\\
 
\end{align} \]


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

 
\[\begin{align}
\alpha & :=\forall x(Ix\land \exists y(Oy\land Eyx)\rightarrow \forall z(Iz\land Pzx\rightarrow \exists v(Ov\land Evz))) \label{primerorden} \\
 \beta & :=\exists y(Oy\land Eyt)\\
 \gamma &:=\forall y(Iy\rightarrow Pdy)\\
 \delta & :=\exists x(Ox\land Exd) 
\end{align} \]


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

 

\[\begin{align} \forall x(Ox
&\rightarrow \lnot Ix)\\ \forall x\,\forall y(Exy&\rightarrow
Ox\land Iy) \\ \forall x\,\forall y(Pxy&\rightarrow Ix\land Iy)\\
 
\end{align} \]

#### 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 of
domains".



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



The following theorem holds for any of these extended structures.




**Theorem:** Let \(\mathcal{A}\) be a many-sorted
structure, \(\mathcal{A}^{\ast}\) one of its one-sorted counterparts,
\(L\) a language for \(\mathcal{A}\), and \(\varphi\) some sentence in
\(L\). Then

 
\[\mathcal{A}\models \varphi \ \Longleftrightarrow \ \mathcal{A}^{\ast}\models \Trans(\varphi ).\]



We have seen that many-sorted structures are always convertible into
one-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 problems
that could stop the conversion: the first one is that in a many-sorted
structure all the universes should be nonempty and our idea is to take
for each sort \(i\) the unary relation \(Q\_{i}^{\mathcal{E}}\) as
universe of sort \(i\) and so we need it to be nonempty; the second
difficulty concerns operation symbols with \(\Rank(f)=\langle
i\_{1},\ldots i\_{n},i\_{0}\rangle\) whose interpretation in structure
\(\mathcal{E}\) is just an *n*-ary function, but we need the
values of \(f^{\mathcal{E}}\upharpoonright
(Q\_{i\_{1}}^{\mathcal{E}}\times \ldots \times
Q\_{i\_{n}}^{\mathcal{E}})\) to be in \(Q\_{i\_{0}}^{\mathcal{E}}\).



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


* \(\exists x\ Q\_{i}x\), for each \(i\in \Sort\)
* \(\forall x\_{1}\ldots x\_{n}(Q\_{i\_{1}}x\_{1}\land \ldots \land
Q\_{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 previous
theorem is a model of \(\Pi\). Moreover, a one-sorted model of
\(\Pi\), \(\mathcal{E}\), is easily convertible into a many-sorted
one, \(\mathcal{E}^{\ddag }\). We take \(Q\_{i}^{\mathcal{E}}\) as the
universe of sort \(i\), strict relations and functions are obtained as
restrictions to the corresponding domains to obtain relations and
functions with the desired
 sorts.[29]
 Due to the axioms in \(\Pi\), construction of \(\mathcal{E}^{\ddag
}\) can be carried out. It is now easy to obtain the following
result.




**Main Theorem:** Let \(\Gamma \cup \{\varphi \}\subseteq
\Sent(L)\).

 
\[\Gamma \models \_{\MSL}\varphi \text{ if and only if } \Trans(\Gamma )\cup \Pi \models \_{\FOL}\Trans(\varphi )\]



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



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



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


### 6.2 The Interpolation Theorem



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



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



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



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


1. \(\Rel(\varphi )\cap \Rel(\psi )\not=\varnothing\) implies that
there 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 the
conditional formula \(\varphi \rightarrow \psi\), we make use of what
is today known as an "interpolant", \(\theta\), a kind of
*syllogism middle term* that finally disappears.



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



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



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


### 6.3 Interpretability and Theoretical Equivalence



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



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



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



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


### 6.4 Extension of Many-sorted Logic to Sort Logic



Apart from its reduction to one-sorted logic, many-sorted first-order
logic can be extended. *Sort logic* is a many-sorted
second-order logic in which it is allowed to quantify over new sorts,
"looking outside" the structure where the formula is being
interpreted. Then, besides adding sorts to a second-order logic, we
may include a new logical symbol \(\widetilde{\exists }\) to quantify
over new sorts.



In *Sort logic*, well-formed formulas involving
\(\widetilde{\exists }\) must respect a *New Sort Condition*
(Vaananen 2014: 175) to guarantee that the domains
where free variables in \(\varphi\) are interpreted do not interfere
with the scope of the quantifier \(\widetilde{\exists}\). The only
novelty concerns interpretation of formulas with the new
quantifier,




\(\mathcal{M},s\models \widetilde{\exists }X\varphi\) if and only if
\(\mathcal{M}^{\prime },s(\mathbf{X}/X)\models \varphi\) for some
*X*-expansion \(\mathcal{M}^{\prime }\) of \(\mathcal{M}\) and
some \(\mathbf{X}\in \wp (\mathbf{M}\_{i\_{1}}^{\prime }\times \ldots
\times \mathbf{M}\_{i\_{r}}^{\prime })\) (where variable \(X\) is of
sort \(\langle i\_{1},\ldots ,i\_{r},0\rangle)\)




In this definition, model \(\mathcal{M}^{\prime }\) is considered an
*X*-expansion of \(\mathcal{M}\) iff it includes as many new
universes (\(\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 ones
is \(\mathcal{M}\).



For instance, the formula

 
\[\widetilde{\exists }X\,\forall x\,\forall y(Xxy\land Xyx\rightarrow x=y)\]


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 it
can be exemplified.



An axiomatic calculus for sort logic was introduced in
Vaananen (2014), as an extension of the second-order
case. For this reason, he incorporated a second *Comprehension
Axiom* related to \(\widetilde{\exists}\) together with some
restrictions concerning the rules of proof when formulas with the new
quantifier \(\widetilde{\exists }\) are involved (see 2014:
176-177).



As it occurs in every higher-order logic, completeness and compactness
fail for sort logic with standard semantics. Fortunately, it is
possible to build a *Henkin structure* satisfying both
Comprehension axioms and to move to general semantics. Changing
semantics in this way results in the recovery of completeness for the
mentioned calculus, as Vaananen (2014: 179-80)
has remarked. The proof found its inspiration in that of
Henkin's (1950) for type theory.



Vaananen (2014: 181) applied sort logic to Foundations
of Mathematics. He proposed the notion of truth in a structure
\(\mathcal{A}\) *characterizable in sort logic*, making a new
distinction between general truth \(\models \varphi\) and specific
truth in those structures. Whenever general truth is reduced to
specific truth, we can use the calculus to prove the satisfiability of
a formula. Under certain constraints, any class of structures closed
under isomorphism is definable in sort logic (see Kennedy &
Vaananen 2021, Theorem 19). Thus,
Vaananen argues that sort logic is an
"alternative way of looking at mathematics", where, unlike
set theory, "definition rather than construction is the
focus" (2014: 185). It is also an interesting tool for studying
*Logicality and model classes* (Kennedy &
Vaananen 2021).