1. One might, alternatively, include sort 0, as the sort of truth values. However, including the sort 0 is not mandatory. In general, the truth values are the classical Boolean truth and falsity, but we could consider a many-sorted logic which is also many-valued. In that case we would need to add a domain of sort 0, thereby opening the door to a many-valued, many-sorted logic. Another reason for choosing to add sort 0 would be to get closer to the common presentation of type theory (see the entry on Church’s type theory).

2. Under certain circumstances, it is better to have an equality symbol for each sort \(i\) (strict option), with \(\Rank(\approx _{i})=\langle i,i,0\rangle\).

3. In case you choose the strict option, \(\tau _{1}\approx _{i}\tau _{2}\) is a well formed formula iff \(\tau _{1}\) and \(\tau _{2}\) have the same sort \(i\).

4. The precise definition is as follows. By a structure \(\mathcal{A}\) of signature \(\Sigma =\langle \Sort,\OperSym,\Rank\rangle\) we mean a pair:

\[\mathcal{A}=\langle \langle A_{i}\rangle _{i\in \Sort}\text{, }\langle f^{\mathcal{A}}\rangle _{f\in \OperSym}\rangle,\]

where

• \(\langle A_{i}\rangle _{i\in \Sort}\) is a family of non-empty sets such that, for each \(i\in \Sort\), \(\mathbf{A}_{i}\) is the i^th universe of \(\mathcal{A}\).

• \(\langle f^{\mathcal{A}}\rangle _{f\in \OperSym}\) is a family of functions such that, for every \(f\in \OperSym\) with \(\Rank(f)=\langle i_{1},\ldots,i_{m},i_{0}\rangle\), it holds that

  \[f^{\mathcal{A}}:\mathbf{A}_{i_{1}}\times \ldots\times \mathbf{A}_{i_{m}}\longrightarrow \mathbf{A}_{i_{0}}.\]

  When \(\Rank(R)=n\), then

  \[R^{\mathcal{A}}:\left(\bigcup\limits_{i\in \Sort}\kern-.5em\mathbf{A}_{i}\right)^{n}\longrightarrow \lbrace T,F \rbrace.\]

Logical connectives and equality are standard.

Obviously, when \(\Rank(R)=\langle i_{1},\ldots,i_{m},0\rangle\), the above definition is the same as \(R^{\mathcal{A}}\subseteq \mathbf{A}_{i_{1}}\times \ldots\times \mathbf{A}_{i_{m}}\) because an n-ary relation is just an n-ary function on the set of truth values, \(\{T,F\}\). This function is often called characteristic function. When \(\Rank(c)= i\,\) then \(c^{\mathcal{A}}\in \mathbf{A}_{i}\).

5. The precise definition is as follows. Given a Σ-structure \(\mathcal{A}\), an assignment is a function \(s\) from variables to the corresponding domains in the structure in such a way that a variable of sort \(i\) always get its value in \(\mathbf{A}_{i}\), namely, \(s(x^{i})\in \mathbf{A}_{i}.\) 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 \(s\) except that the value at \(x^{i}\) has to be \(\mathbf{x}\). In other words,

\[s(\mathbf{x}/x^{i})=(s-\{\langle x^{i},s(x^{i})\rangle\})\cup \{\langle x^{i},\mathbf{x}\rangle \}\]

6. There is no agreement on the definition of the term theory. It can be defined as a set of sentences closed under deducibility (or, equivalently, closed under semantical consequence).

A theory can be defined as a set of sentences (see Hodges 1993: 33). According to this definition, the smallest theory corresponds to the empty set. According to our definition, the set of validities is the smallest theory, and the whole \(\Sent(L)\) the biggest (and contradictory) one.

7. A set of formulas is contradictory (not consistent, or inconsistent) if and only if each formula in the language can be deduced from it. A set of formulas is maximally consistent when besides being consistent, each formula not in the set would make it inconsistent, if it were added to the set.

8. For details on the history of the various notions of completeness, see Manzano & Alonso 2014 and Aranda 2022.

9. A model \(\mathcal{A}\) is countable when \(\bigcup\limits_{i\in \Sort}\kern-.5em\mathbf{A}_{i}\) is countable.

10. See “Decidable fragments of many-sorted logic” (Abadi, Rabinovich, & Sagiv 2007).

11. Carnielli, Coniglio and D’Ottaviano (2009) have also studied the concept of abstract contextual translation. In addition to this, D’Ottaviano and Feitosa 2019 is a survey of translations between logics.

12. The set of modal validities in minimal modal logic could be axiomatized by a Hilbert axiomatic system called K including axiom

\[K:=\square (\varphi \rightarrow \psi )\rightarrow (\square \varphi \rightarrow \square \psi )\]

and a modal generalization rule, if \(\vdash \varphi\) then \(\vdash \square \varphi\). See Blackburn and van Benthem (2007: 10)

13. The idea is simple:

Whenever we translate a \(\Diamond\) or a \(\square\), instead of choosing a completely new variable to quantify over accessible points, we use a second fixed variable (say \(y\)). If we later encounter another \(\Diamond\) or \(\square\), we flip back to the original variable \(x\), and so on. (Blackburn & van Benthem 2007: 28)

14. Bisimulation can be defined for formulas \(\varphi (x)\) of a first-order language and we can prove (see Blackburn & van Benthem 2007: 21):

15. For a more detailed explanation see Manzano (1996: 263–276).

16. In fact, the inclusion is strict

\[\Val_{\mathfrak{F}}\subset \Val_{\mathfrak{GS}}\subset \Val_{\mathfrak{SS}}\]

as the following examples show:

1. The comprehension axiom belongs to \(\Val_{\mathfrak{GS}}\) but it is not a valid formula with the semantics of frames.

2. To put an example of a valid sentence in standard structures that fails in some general structures let us take the sentence

   \[\pi _{1}\land \pi _{2}\land \pi _{3}\rightarrow \gamma\]

   where \(\pi _{1}\), \(\pi _{2}\) and \(\pi _{3}\) are the second-order categorical Peano axioms for arithmetic, and \(\gamma\) is the well-known Gödel formula asserting of itself that it is not a theorem of Peano arithmetic.

17. For simplicity we keep the notation \(\langle\underbrace{ 1,\ldots ,1}_n ,0\rangle\) for sorts in \(\MSL^{\SOL}\), but now we do not require the domain of this sort to be of n-ary relations of elements of sort 1.

18. For more details, see Manzano (1996: 285–288).

19. Consider now the following example: from a structure \(\mathcal{A}\) with domains \(\mathbf{A}_{1}=\{ 1,2,3\}\) and \(\mathbf{A}_{\langle 1,0\rangle }=\{ 4,7\}\) where

\[\epsilon _{n}^{\mathcal{A}}=\{ \langle 1,4\rangle ,\langle 2,4\rangle ,\langle 3,4\rangle \},\]

we obtain a structure \(\mathcal{B}\) with \(\mathbf{B}_{1}=\{ 1,2,3\}\) and \(\mathbf{B}_{\langle 1,0\rangle }=\{ \{ 1,2,3\} ,\varnothing \}\) where

\[\epsilon _{n}^{\mathcal{B}}=\{ \langle 1,\{ 1,2,3\} \rangle ,\langle 2,\{ 1,2,3\} \rangle ,\langle 3,\{ 1,2,3\} \rangle \}\]

20. The official publication date by Princeton University Press is 1956, however the book was available in manuscript form before 1956, according to Henkin (1996). More specifically, as noted in the Preface, the 1956 edition is a “revised and much enlarged edition” of an earlier 1944 edition (Church 1956, v).

21. \(\Trans(\varphi )[u]\) is defined by induction on the construction of formulas, \(u\) is an individual variable in MSL whose interpretation is a world in the Kripke model.

\[\begin{align} \Trans(P)[u] &:=Pu\\ \Trans(\perp )[u]&:=u\neq u\\ \Trans(\lnot \varphi )[u]&:=\lnot \Trans(\varphi )[u]\\ \Trans(\varphi \rightarrow \psi )[u]&:=\Trans(\varphi )[u]\rightarrow \Trans(\psi )[u]\\ \Trans(\Box \varphi )[u]&:=\forall v(Suv\rightarrow \Trans(\varphi )[v])\\ \end{align}\]

22. The set \(\Def\) contains the empty set, the whole \(\mathbf{W}\) and all the members in the family \(\langle P^{\mathcal{A}}\rangle _{P\in \Atom}\). It is closed under Boolean operations as well as under this operation

\[\forall \mathbf{T}(\mathbf{T}\in \Def\Rightarrow \Dom(\mathbf{R}\cap (\mathbf{W}\times \mathbf{T}))\in \Def)\]

to guarantee that initial states from accessibility relations leading to definable sets are definable. Outside \(\Def\), but in \(\mathbf{W}^{\prime }\), we have the singletons of all elements of \(\mathbf{W}\). Finally, \(\mathbf{W}^{\prime }\) also obeys the rule

\[\forall w(w\in \mathbf{W}\Rightarrow \Rec(\mathbf{R}\cap (\{ w\} \times \mathbf{W}))\in \mathbf{W}^{\prime }).\]

23. Let us use \(\Delta _{S4}\) to refer to the many-sorted theory obtained by adding to \(\Delta _{K}\) the many-sorted formulas \(\MS(T)\) and \(\MS(4)\).

\[\begin{align} \MS(T)& :=\forall uY(\forall v(Suv\rightarrow \epsilon _{1}vY)\rightarrow \epsilon _{1}uY)\\ \MS(4)&:=\forall uY(\forall v(Suv\rightarrow \epsilon _{1}vY)\rightarrow \forall v(Suv\rightarrow \forall w(Svw\rightarrow \epsilon _{1}wY)))\\ \end{align}\]

24. Main Theorem:

• \(\Pi \models \varphi\) (in the whole class of Kripke structures) \({}\Longleftrightarrow \Trans(\Pi )\cup \Delta _{K}\models \Trans(\varphi )\)
• \(\Pi \models _{\mathfrak{D}}\varphi\) (in the class \(\mathcal{D}\) of reflexive and transitive Kripke structures) \({} \Longleftrightarrow \Trans(\Pi )\cup \Delta _{S4}\models \Trans(\varphi )\)

As in modal logics K and S4 we already have the concept of logical consequence, and we obtain the desired theorem for both, by defining the reverse conversion of structures by getting rid of the domain \(\mathbf{W}'\).

25. For a modal logic B, we define its canonical model \(\mathcal{B}_{B}\), by taking as world \(W\) all the B-maximally consistent sets and defining the accessibility relation in this way

\[\{\langle x,y\rangle \mid\{ \varphi |\Box \varphi \in x\} \subseteq y\}\]

26. The translation for formulas is defined as for formulas of PML with the following additions:

\[\begin{align} \Trans(\left[ a\right] \varphi )[u]&:=\forall v(\Trans(a)[u,v]\rightarrow \Trans(\varphi )[v])\\ \Trans(Q)[u,v]&:=Quv\\ \Trans(a;b)[u,v]&:=\exists w(\Trans(a)[u,w]\land \Trans(a)[w,v])\\ \Trans(a\cup b)[u,v]&:=\Trans(a)[u,v]\lor \Trans(a)[u,v]\\ \Trans(a\ast )[u,v]&:=\forall X^{2}(\Trans(a)\subseteq X^{2}\land \Reflexive (X^{2})\\ & \quad\quad \land \Transitive (X^{2}) \rightarrow \epsilon _{2}uvX^{2})\\ \end{align}\]

This formula is an abbreviation and says that it is the least reflexive and transitive relation containing the translated one.

\[\Trans(\varphi ?)[u,v]:=\Trans(\varphi )[u]\land u=v\]

27. For a more detailed explanation see Manzano (1996: 335–351) as well as Manzano (1993: 72–81).

28. The precise definition of one-sorted structure \(\mathcal{A}^{\ast}\) is obtained by conversion from the many-sorted structure \(\mathcal{A}\) as follows

\[\mathcal{A}^{\ast }=\langle A^{\ast },\langle f_{{}}^{\mathcal{A^{\ast }}}\rangle _{f\in \OperDSym},\langle Q_{i}^{\mathcal{A^{\ast }}}\rangle _{i\in \Sort}\rangle\]

and by means of the following clauses:

• The domain of \(\mathcal{A}^{\ast }\) is the union of the individuals domains of \(\mathcal{A}\), that is, \(\mathbf{A}^{\ast }=\bigcup_{i\in \Sort}\kern-.5em\mathbf{A}_{i}\).

• For each \(f\in \OperDSym\) with \(\Rank(f)=\langle i_{1},\ldots ,i_{n},i_{0}\rangle\) and \(i_{0}\neq 0\), \(f^{\mathcal{A}^{\ast }}\) is any extension of \(f^{\mathcal{A}}\) such that the domain of the function is the whole \((A^{\ast })^{n}\) and the restriction to the old domain is the original \(f^{\mathcal{A}}\), that is

  \[\ f^{\mathcal{A}^{\ast }}\upharpoonright (\mathbf{A}_{i_{1}}\times \ldots \times \mathbf{A}_{i_{n}})=f^{\mathcal{A}}\]

  (where new values in \(f^{\mathcal{A}^{\ast }}\) are chosen arbitrarily).

• For each \(R\in \OperDSym\) with either \(\Rank(R)=\langle i_{1},\ldots ,i_{n},0\rangle\) or \(\Rank(R)=n\), the relations used as interpretation are the same in both structures, \(R^{\mathcal{A}^{\ast }}=R^{\mathcal{A}}\).

• \(Q_{i}^{\mathcal{A^{\ast }}}=\mathbf{A}_{i}\) for each \(i\in \Sort\).

29. The precise definition is as follows. For each sort \(i\), we take \(Q_{i}^{\mathcal{E}}\) as the universe of this sort, that now we know is nonempty. For each predicate symbol \(R\) with \(\Rank(R)=n\), \(R^{\mathcal{E}^{\ddag }}=R^{\mathcal{E}}\), nothing changes. For each predicate symbol \(R\) with \(\Rank(R)=\langle i_{1},\ldots,i_{n},0\rangle\), its interpretation is the restriction to the new local universes,

\[R^{\mathcal{E}^{\ddag }}=R^{\mathcal{E}}\cap (Q_{i_{1}}^{\mathcal{E}}\times \ldots\times Q_{i_{n}}^{\mathcal{E}}).\]

Finally, for each function symbol \(f\) with \(\Rank(f)=\langle i_{1},\ldots,i_{n},i_{o}\rangle\), its interpretation is the restriction to the new local universes,

\[f^{\mathcal{E}^{\ddag }}=f^{\mathcal{E}}\upharpoonright (Q_{i_{1}}^{\mathcal{E}}\times \ldots\times Q_{i_{n}}^{\mathcal{E}}),\]

that is a function of the desired sort.

30. Let us quote Feferman’s (2008) own words:

Interestingly, in a personal communication, Wilfrid Hodges brought to my attention that “t]he Lyndon theorem has a claim to be the twentieth century metatheorem with the longest pedigree, because it is a generalisation of the late medieval laws of distribution for syllogisms. Obviously the theorem itself and any of its proofs would have been way beyond the understanding of any of the medievals, but it does seem to contain the correct formalisation of a number of medieval intuitions.” For elaboration, see Hodges (1998). (2008: 346–347, note 4)

31. Extended Craig-Lyndon’s Interpolation Theorem: If \(\Gamma \models \Delta\), then \(\Gamma \vdash B\) and \(B \vdash \delta\). From this, strong completeness follows immediately (see Henkin 1963b).

32. Feferman’s version of the theorem for MSL includes not only \(\Rel^{+}\) and \(\Rel^{-}\) (which have to be used for Lyndon’s generalized theorem), but also four new sets, \(\Sort\), \(\Free\), \(\Un\) and \(\Ex\):

\[\begin{align} \Sort(\varphi )&=\{ j\in J:\text{a variable of sort }j\text{ occurs in }\varphi \} \\ \Free(\varphi )&= \text{the set of free variables of }\varphi \\ \Un(\varphi )&=\{ j\in J:\text{a }\forall x_{j}\text{ occurs in }\nnf(\varphi )\} \\ \Ex(\varphi )&=\{ j\in J:\text{a }\exists x_{j}\text{ occurs in }\nnf(\varphi )\} \\ \end{align}\] (where \(\nnf(\varphi )\) is the negation normal form of \(\varphi\))

In consequence, the Interpolation Theorem for MSL states that: If \(\vdash \varphi \rightarrow \psi\), then it has an interpolant \(\theta\) with respect to \(\Rel^{+}\), \(\Rel^{-}\), \(\Sort\) and \(\Free\) for which

\[\Un(\theta )\subseteq \Un(\varphi )\text{ and }\Ex(\theta )\subseteq \Ex(\psi ).\]

33. See Hodges (1993: 59) for a description of the concept of explicit definition in one-sorted first-order logic; see Barrett and Halvorson (2016: 560) for the many-sorted case.

34. The official publication date by Princeton University Press is 1956, despite the fact that, in the references of Wang (1952), the date of publication is 1944. We know that early forms of the book were available in manuscript form before 1956 (see Henkin 1996, p. 133). Exercise 55.24 (p. 339) is in Chapter 5 and according to the Preface, the work on Chapters 3, 4, and 5 was done in 1948–1951 (Church 1956, vi).

35. The one-sorted elementary logic Wang refers to is the one presented in Quine 1940.

36. In section 22, Quine says:

We now turn to a connective “\(\epsilon\)” which embodies the principal meaning of the ambiguous word “is”. Sometimes “is” has the sense of “\(=\)” or “is the same as”; such is its sense in “Paris is the capital of France”…. But in “Paris is a city” the word cannot be so construed. In such contexts “is” expresses rather possession of a property, or membership in a class: Paris belongs to the class of cities. (Quine 1940: 119)

Quine also admits:

…there are differences in detail between the notion of membership developed here and the notion of membership that Tarski and Gödel took over from Whitehead and Russell. (Quine 1940: 126)