Movatterモバイル変換

1. One might, alternatively, includesort 0, as the sort of truth values. However, including the sort 0 isnot mandatory. In general, the truth values are the classical Booleantruth and falsity, but we could consider a many-sorted logic which isalso many-valued. In that case we would need to add a domain of sort0, thereby opening the door to a many-valued, many-sortedlogic. Another reason for choosing to add sort 0 would be to getcloser to the common presentation of type theory (see the entry onChurch’s type theory).

2. Under certain circumstances, it is better to have an equality symbolfor 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 apair:

where

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

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

  \[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\), theabove definition is the same as \(R^{\mathcal{A}}\subseteq\mathbf{A}_{i_{1}}\times \ldots\times \mathbf{A}_{i_{m}}\) because ann-ary relation is just ann-ary function on the set oftruth values, \(\{T,F\}\). This function is often calledcharacteristic 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}\), anassignment is a function \(s\) fromvariables to the corresponding domains in the structure in such a waythat a variable of sort \(i\) always get its value in\(\mathbf{A}_{i}\), namely, \(s(x^{i})\in \mathbf{A}_{i}.\) For anyindividual \(\mathbf{x}\in \mathbf{A}_{i}\) and variable \(x^{i}\) ofsort \(i\), we use \(s(\mathbf{x}/x^{i})\) to denote the assignmentwhich is like \(s\) except that the value at \(x^{i}\) has to be\(\mathbf{x}\). In other words,

6. There is no agreement on the definition of the termtheory.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 theempty set. According to our definition, the set of validities is thesmallest theory, and the whole \(\Sent(L)\) the biggest (andcontradictory) one.

7. A set of formulas iscontradictory (not consistent, orinconsistent) if and only if each formula in the language can bededuced from it. A set of formulas ismaximally consistentwhen besides being consistent, each formula not in the set would makeit 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 studiedthe concept of abstract contextual translation. In addition to this,D’Ottaviano and Feitosa 2019 is a survey of translations betweenlogics.

12. The set of modal validities inminimal modal logic could beaxiomatized by a Hilbert axiomatic system calledK includingaxiom

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 ofchoosing a completely new variable to quantify over accessible points,we use a second fixed variable (say \(y\)). If we later encounteranother \(\Diamond\) or \(\square\), we flip back to the originalvariable \(x\), and so on. (Blackburn & van Benthem 2007: 28)

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

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

16. In fact, the inclusion is strict

as the following examples show:

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

2. To put an example of a valid sentence in standard structures thatfails 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-ordercategorical Peano axioms for arithmetic, and \(\gamma\) is thewell-known Gödel formula asserting of itself that it is not atheorem 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 ofn-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}_{\langle1,0\rangle }=\{ 4,7\}\) where

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

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 thePreface, the 1956 edition is a “revised and much enlargededition” of an earlier 1944 edition (Church 1956, v).

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

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

to guarantee that initial states from accessibility relations leadingto 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

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

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}\) ofreflexive andtransitive Kripkestructures) \({} \Longleftrightarrow \Trans(\Pi )\cup \Delta_{S4}\models \Trans(\varphi )\)

As in modal logicsK andS4 we already have the conceptof 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 logicB, we define its canonical model\(\mathcal{B}_{B}\), by taking as world \(W\) all theB-maximally consistent sets and defining the accessibilityrelation in this way

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

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

27. For a more detailed explanation see Manzano (1996: 335–351) aswell 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

and by means of the following clauses:

• The domain of \(\mathcal{A}^{\ast }\) is the union of the individualsdomains 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 thefunction is the whole \((A^{\ast })^{n}\) and the restriction to theold 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 chosenarbitrarily).

• For each \(R\in \OperDSym\) with either \(\Rank(R)=\langlei_{1},\ldots ,i_{n},0\rangle\) or \(\Rank(R)=n\), the relations usedas 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 knowis nonempty. For each predicate symbol \(R\) with \(\Rank(R)=n\),\(R^{\mathcal{E}^{\ddag }}=R^{\mathcal{E}}\), nothing changes. Foreach predicate symbol \(R\) with \(\Rank(R)=\langlei_{1},\ldots,i_{n},0\rangle\), its interpretation is the restrictionto the new local universes,

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

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 tomy attention that “t]he Lyndon theorem has a claim to be thetwentieth century metatheorem with the longest pedigree, because it isa generalisation of the late medieval laws of distribution forsyllogisms. Obviously the theorem itself and any of its proofs wouldhave been way beyond the understanding of any of the medievals, but itdoes seem to contain the correct formalisation of a number of medievalintuitions.” 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 forLyndon’s generalized theorem), but also four new sets,\(\Sort\), \(\Free\), \(\Un\) and \(\Ex\):

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

33. See Hodges (1993: 59) for a description of the concept of explicitdefinition 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 ofpublication is 1944. We know that early forms of the book wereavailable 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 (Church1956, vi).

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

36. In section 22, Quine says:

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

Quine also admits:

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