• Entry Contents
• Bibliography
• Academic Tools
• Friends PDF Preview
• Author and Citation Info
• Back to Top

Definition 1 Theformulas of second-orderlogic are defined as follows: Atomic formulas are formulas. If\(\phi\) and \(\psi\) are formulas, then \(\neg\phi\), \(\phi\land\psi\), \(\phi\lor \psi\), \(\phi \to \psi\) and \(\phi\leftrightarrow \psi\) are formulas. If \(\phi\) is a formula,x an individual variable,X a relation variable andF a function variable, then \(\exists x\phi\), \(\forallx\phi\), \(\exists X\phi\), \(\forall X\phi, \exists F\phi\) and\(\forall F\phi\) are formulas.

3. The Semantics of Second-Order Logic

In order to define the semantics of second-order logic we have toagree what ourmetalanguage is. This fact has nothing to dowith second-order logic but is rather a general feature of semantics(Tarski 1933 [1956]). The most commonly used metalanguage forsecond-order logic isset theory. We thus give aset-theoretical interpretation of second-order logic, interpreting“properties” as sets in a domain which itself is a set.This is the most common choice and brings out the main features ofsecond-order logic. We cannot interpretall properties by sets,e.g. the property of being identical to oneself. But if the domainthat the individual variables range over is taken to be a set, then wecan meaningfully interpret properties of individuals in that domain assets. If we want to interpret second-order logic in a domain which istoo large to be a set, we can use the set-theoretical concept of aclass (see entry onset theory for more on classes).

We use the same concept of anL-structure (or equivalently, anL-model) as in first order logic. That is, anL-structure \(\mm\) has adomainM,which is any non-empty set, aninterpretation \(c^\mm \in M\)of any constant symbolc ofL, an interpretation \(R^\mm\subseteq M^n\) of anyn-ary relation symbolR ofL, as well as an interpretation \(H^\mm : M^n \to M\) of anyn-ary function symbolH ofL. In principle, thedomain could be a class but we disregard this possibility here. For adiscussion on the set/class distinction in this context, we refer toShapiro (1991, p. 16).

Convention: Whenever we use upper case Fraktur letters, such as\(\mm,\mn\) etc, to name a structure, we use the upper case Italicversions of those letters, such as \(M,N\) etc, to name the domain ofthe structure.

Given anL-structure \(\mm\), anassignment is afunctions from variables to the domainM of \(\mm\)such that: ifx is an individual variable, then \(s(x) \in M\);ifX is relation variable of arityn, then \(s(X)\subseteq M^n\); ifF is function variable of arityn,then \(s(F) : M^n \to M\). We use \(s(P/X)\) to denote the assignmentwhich is otherwise ass except that the value atX hasbeen changed toP. Similarly \(s(a/x)\) and \(s(f/F)\).

Note that \(0\)-ary relation variables are essentially propositions.Their interpretations under an assignment are the truth values (true,false). \(0\)-ary function variables are essentially individualvariables as an assignment maps a \(0\)-ary function symbol simply toan element of \(M\). A \(0\)-ary relation symbol or variable is at thesame time an atomic formula and a non-logical symbol. We disregards inthe current presentation this potential notational confusion.

The value \(t^\mm\langle s\rangle\) of a termt in a model\(\mm\) under the interpretations is defined as in first orderlogic.

The concept \(\mm\models\phi\) of thetruth of the sentence\(\phi\) in \(\mm\) can now be defined by first defining the auxiliaryconcept \(\mm\models_s\phi\) of the assignment \(s\)satisfying\(\phi\) in \(\mm\) (see entry onTarski’s truth definitions for more details):

In clause 1 of the above definition we follow the common practice ofgiving a set-theoretical interpretation to the predication\(X(t_1,\ldots,t_n)\). Having interpretedX as a subset of\(M^n\), we interpret predication \(X(t_1,\ldots,t_n)\) as membership\((t^\mm_1 \langle s\rangle,\ldots,t^\mm_n \langle s\rangle) \ins(X)\). In clause 2 we interpret quantification over properties andrelations as quantification over subsets of the cartesian product\(M^n\). Respectively, in clause 3 we interpret quantification overfunctions as quantification over sets that are functions \(M^n\to M\)in the set-theoretical sense.

Now that the semantics of second-order logic is defined we can definewhat it means for a formula \(\phi\) to bevalid and for twoformulas \(\phi\) and \(\psi\) to belogically equivalent. Asin logic in general, we say that \(\phi\) is (logically) valid if\(\mm\models_s\phi\) holds for all \(\mm\) and alls. Likewise,we define \(\phi\) and \(\psi\) to be logically equivalent,\(\phi\equiv\psi\), if \(\phi\leftrightarrow\psi\) is valid. Twomodels \(\mm\) and \(\mn\) are said to besecond-orderequivalent, in symbols \(\mm\equiv_{L^2}\mn\) if for allsentences \(\phi\) we have \(\mm\models\phi\iff\mn\models\psi\).

The truth definition involves the concepts “for some \(P\subseteq M^n\)” and “for some \(f:M^n \to M\)”.Since we assume set theory as our metalanguage, we can interpret thesein the sense of set theory. Thus we interpret “for some \(P\subseteq M^n\)” as “for someset \(P \subseteqM^n\)” and “for some \(f:M^n\to M\)” as “forsomeset which is a function \(f:M^n\to M\)”.

For infiniteM the collection of subsets of \(M^n\) and the setof functions \(M^n\to M\) are famously complex. Currently set theory(ZFC) cannot even decide howmany subsets of an infinite setthere are. The situation is quite different with first order logic.The respective concept “for some \(a \in M\)” isunproblematic, relatively speaking. Of course, depending on whatM is, “for some \(a \in M\)” can be quiteproblematic too. To reflect the difficulties involved with finding a\(P \subseteq M^n\) or an \(f:M^n \to M\) we sometimes say we“guess” a \(P \subseteq M^n\) or an \(f:M^n \to M\).

When we use set theory as the metatheory for the semantics offirst order logic, the reliance on the metatheory is of alower degree than when we use set theory as the metatheory for thesemantics ofsecond order logic. The central concept, whichexplains the difference, is that ofabsoluteness. Fordetails, see§6.

4. Properties of Second-Order Formulas

Many syntactic operations that we are used to in first order logicwork equally well in second-order logic. One such is the operation ofrelativization, in which we want to limit what a formulaexpresses to a fixed part of the universe. For example, we mayconsider models where a certain unary predicateU is used forthe set of natural numbers. Then we relativize our axioms ofarithmetic to the predicateU. Some other part of the model maybe used for the power set of the set of natural numbers. Then werelativize our axioms of power set (see§5.3) to that part, and so on.

If \(\mm\) is a structure and \(A\subseteq M\), then \(\mm^{A}\) isobtained by restricting the relations \(R^\mm\) and functions\(F^\mm\) toA. This does not always result in a structure butif it does, it is called therelativization of \(\mm\) toA. Suppose\(\phi=\phi(x_1,\ldots,x_n,X_1,\ldots,X_m,F_1,\ldots,F_k)\) is asecond-order formula andU is a unary relation variable. Thereis a second-order formula \(\phi^{U}\), the relativization of \(\phi\)toU, such that for all \(\mm\) for which \(\mm^{U^\mm}\) is astructure:

Intuitively, \(\phi^{U}\) says about \(U^\mm\) what \(\phi\) saysaboutM. To obtain \(\phi^{U}\) from \(\phi\) one restricts allthe first order quantifiers to elements ofU and second-orderquantifiers to subsets, relations and functions onU.

Hierarchies based on quantifier structure are a useful method tocompare the definability of concepts in different systems. In firstorder logic it was observed very early on that formulas can be broughtinto a logically equivalentPrenex Normal Form in which allquantifiers occur in the beginning of the formula. This is possiblealso in second-order logic and the proof is essentially the same.Moreover, using the equivalence (which is reminiscent of a principleof set theory called Axiom of Choice, to which we return in Section5.4., since in the below formula the relation \(Y\) in a sense choosesone \(X\) for each \(x\) and puts them together into one relation\(Y\) – see entry onAxiom of Choice for more on the topic.)

where the arity ofY is one higher than the arity ofX,and \(\phi'\) is obtained from \(\phi\) by replacing everywhere\(X(t_1,\ldots,t_n)\) by \(Y(x,t_1,\ldots,t_n)\), one can bring everysecond-order logic formula to a logically equivalent normal form

where each \(Q_i\) is either \(\exists\) or \(\forall\) and \(\phi\)is first order. That is, all second order quantifiers of the formulaare in the front.

By restricting what kind of quantifiers the sequence \(Q_1X_1\ldotsQ_nX_n\) of the Prenex Normal Form (\ref{qqq}) can contain we obtainthe classes of \(\Sigma^1_n\)-, \(\Pi^1_n\)- and\(\Delta^1_n\)-formulas, as indicated inTable 1. For example, the second-order formulas (1) and (2) are\(\Pi^1_1\)-formulas.

We have considered above only quantifiers that bind relation variablesbut the situation is exactly the same if we had bound functionvariables.

These classes of formulas have some obvious closure properties: Theyare all closed, up to logical equivalence, under \(\land , \lor\), andfirst order quantifiers. Moreover, the hierarchy is proper in thesense that for all \(n\ge 1\)

which can be proved with a diagonalisation argument. The classes\(\Delta^1_n\) are closed under \(\land , \lor, \neg\) and first orderquantifiers. By Craig’s Interpolation Theorem,\(\Delta^1_1\)-formulas are logically equivalent to first orderformulas^[2].

There is a sense in which \(\Pi^1_1\), or equivalently \(\Sigma^1_1\),already has the full power of second-order logic, although the abovehierarchy result (\ref{kurat}) shows that this cannot literally betrue. To see this, i.e., to see what the reduction of second-orderlogic to its \(\Pi^1_1\)-part means, letL be a vocabulary,E a binary andU a unary relation symbol, both not inL. Let \(\theta\) be the second-order\(\Pi^1_1\)-formula

where

It is easy to see^[3] that models of \(\theta\) are, up to isomorphism, models \(\mm\)where \(M=U^\mm\cup\P(U^\mm)\), \(U^\mm\cap\P(U^\mm)=\emptyset\) andfor all \(a,b\in M\), \(E^\mm(a,b)\leftrightarrow a\in b\). In such amodel monadic second-order formulas \(\phi\) over \(U^\mm\) can bereduced to first order formulas \(\phi^*\) overM. Thisreduction, due to Hintikka (1955) and further developed by Montague(1963), shows that \(\Pi^1_1\)-formulas alone are enough to expressany second-order property with extra predicates. The idea can beextended to third and higher order logic, and also to non-monadicsecond-order logic.

As a consequence, checking the validity of a second-order sentence\(\phi\) can be recursively reduced to checking the validity of the\(\Sigma^1_1\)-sentence \(\theta\to\phi^*\). Likewise checking whethera second-order sentence \(\phi\) has a model of cardinality \(\kappa\)can be reduced to asking whether the \(\Pi^1_1\)-sentence\(\theta\land\phi^*\) has a model of cardinality \(2^\kappa\). Thismeans that the Löwenheim number^[4] and the Hanf number^[5] of the entire second-order logic are the same as those of thefragment \(\Pi^1_1\).

Summing up, upon first inspection the levels \(\Sigma^1_n\) and\(\Pi^1_n\) of the hierarchy of second-order formulas grow strictly inexpressive power asn increases, but a more careful analysisreveals that already the first level \(\Sigma^1_1\cup \Pi^1_1\) hasthe power of all the levels \(\Sigma^1_n, \Pi^1_n\) even if the poweris somewhat implicit and needs to be brought to light.

In set theory there is theLevy-hierarchy of \(\Sigma_n\)-and \(\Pi_n\)-formulas (Lévy 1965). Formulas where allquantifiers are bounded, i.e., of the form \(\forall x\in y\) or ofthe form \(\exists x\in y\) for somex andy, are called\(\Sigma_0\) or equivalently \(\Pi_0\). Formulas of the form \(\forallx\,\phi\), where \(\phi\) is \(\Sigma_n\), are called \(\Pi_{n+1}\).Formulas of the form \(\exists x\,\phi\), where \(\phi\) is \(\Pi_n\),are called \(\Sigma_{n+1}\). This is a strict hierarchy roughly forthe same reason why the hierarchy of second-order \(\Sigma^1_n\)- and\(\Pi^1_n\)-formulas is strict. But there is no known method to reducethe truth of an arbitrary formula to the truth of a formula on the\(\Sigma_1\cup\Pi_1\) level. In fact, if the decision problem,Löwenheim-Skolem number and Hanf number are suitably defined for\(\Sigma_n\cup \Pi_n\)-formulas of set theory, the decision problemgets more and more complicated, and the numbers obtained get biggerand bigger asn increases (seeTheorem 4; Väänänen 1979).

The hierarchy \(\Sigma_n^1\cup \Pi_n^1\) inside second-order logic andthe hierarchy \(\Sigma_n\cup\Pi_n\) in set theory, are furthercompared to each other in§7.

5.1 Putting distance between second- and first-order logic

Second-order logic has some remarkable qualities which we will nowuncover in detail. Above we characterized the structure of the naturalnumbers by means of (\ref{ind}). This application of second-orderlogic is perhaps the most famous and most important. We nowreformulate this in a slightly more general form in order to get morepower out of it. SupposeU is a unary relation variable(“the set of natural numbers”),G a unary functionvariable (“the successor function”), andz anindividual variable (“the zero”). Let\(\theta_{\textrm{PA}}(U,G,z)\) be the sentence

Then \((N,A,g,a)\models\theta_{\textrm{PA}}(U,G,z)\) if and only if\((N,A,g,a)\) is isomorphic to a structure \((M,\oN,s,0)\) where\(\oN\subseteq M\) and \(s(n)=n+1\). Thus we have used second-orderlogic to say that theU-part of any model of\(\theta_{\textrm{PA}}(U,G,z)\), together with the functionGand the individualz are isomorphic to the natural numbers\(\oN\) with their successor function and zero. There are many ways tosee that no first order sentence can have this property. For example,by the Compactness Theorem such a sentence would have also anon-standard model where some element is different from eachin the sequencez, \(G(z)\), \(G(G(z))\), \(G(G(G(z)))\),\(\ldots\). Such a model cannot be isomorphic to the natural numbers\(\oN\) with their successor function and zero. Hereupon we mayconclude that the Compactness Theorem does not hold for second-orderlogic in the form that it holds for first order logic.

In models of \(\theta_{\textrm{PA}}(U,G,z)\) the formula\(\theta_+(U,G,z,H)\)

and the formula \(\theta_\times(U,G,z,H,J)\)

define unique functions \(m+n=H(m,n)\) and \(m\cdot n=J(m,n)\). Afirst order sentence \(\phi(+,\cdot,0)\) of arithmetic is true in\((\oN,+,\cdot,0)\) if and only if

is valid. We know that truth of first order sentences in\((\oN,+,\cdot,0)\) is undecidable, and even non-arithmetical byresults of Gödel (1931 [1986: 144–195]) and Tarski (1933[1956]). This shows that second-order logic is not completelyaxiomatizable by effective means, or decidable even in the emptyvocabulary. That is, there is no decidable second-order theory with aninfinite model. This is in sharp contrast to first order logic wherethe following theories are decidable: first order logic with emptyvocabulary, first order logic with monadic predicates, dense linearorder, Pressburger arithmetic (first order theory of \((\oN,+,0)\)),real closed fields (first order theory of \((\oR,+,\cdot,0,1)\)),theory of algebraically closed fields, and the first order theory of\((\oC,+,\cdot,0,1)\). In second-order logic none of the respectivesecond-order theories are decidable. However, if we restrictsecond-order logic tomonadic second-order logic, we obtainmany important decidable theories (see§8).

5.2 The collapse of the Completeness Theorem

The Completeness Theorem is one of the cornerstones of ourunderstanding of first order logic. Also many extensions of firstorder logic have a Completeness Theorem, most notably the extension offirst order logic by thegeneralized quantifier “There are uncountably many” and theinfinitary language \(L_{\omega_1\omega}\). We shall now see that there is no hope of aCompleteness Theorem for second-order logic. Later in§9.1 we shall modify the semantics so that a Completeness Theorem can beproved.

Behind the failure of the Completeness Theorem is the fact thatsecond-order logic is—almost by definition—able to saythat a set is the power set of another set. What this means is thefollowing: LetL be a vocabulary. LetE be a binary andU a unary relation symbol, both not inL. Let\(\theta_{\textrm{Pow}}(U,E)\) be the second-order formula(\ref{ex6}). Let us consider the conjunction

Models of this formula are, up to isomorphism, of the form\((M,\in,N,g,a)\), where \(\P(N)=M\), \(N\cap\P(N)=\emptyset\) and\(N\) is countably infinite. Thus the models are necessarilyuncountable. This shows that second-order logic, unlike first orderlogic, has sentences with models but only uncountable ones. Thus theDownward Löwenheim-Skolem Theorem fails for second-order logic,as we already noted above. Combining (\ref{papow}) with theobservations in§5.1 yields the following result (by validity we mean the set ofGödel numbers of valid formulas):

In consequence, validity in second-order logic is not \(\Sigma^1_n\)for anyn. Since building power sets in the style of\(\theta_{\textrm{Pow}}(U,E)\) can be iterated, we can see thatvalidity in second-order logic is not \(\Sigma^m_n\) for anymandn. We extend this result further below inTheorem 6.

5.3 “Set theory in sheep’s clothing”

Second-order logic hides in its semantics some of the most difficultproblems of set theory. In the words of Resnik (1988: 75):

In Philosophy of Logic [Quine 1970], W. V. Quine summed up a popularopinion among mathematical logicians by referring to second-orderlogic as “set theory in sheep’s clothing”.

Let us see where this opinion might come from. First we observe that avery simple, indeed a very basic, second-order formula can say thattwo sets have the same cardinality: SupposeP andR areunary relation variables. Let \(\theta_{\le}(P,R)\) be the formula

Now \(\mm\models_s\theta_\le(P,R)\) if and only if \(|s(P)|\le|s(R)|\). Let \(\theta_{\textrm{EQ}}(P,R)\) be the formula\(\theta_{{\le}}(P,R)\land \theta_{{\le}}(R,P)\). Now\(\mm\models_s\theta_{\textrm{EQ}}(P,R)\) if and only if\(|s(P)|=|s(R)|\). Let \(\theta'_{\textrm{EC}}(R)\) be

Now \(\mm\models_s\theta'_{\textrm{EC}}(R)\) if and only if the setsM and \(s(R)\) have the same cardinality. We will use theseformulas to launch an attack on the Continuum Hypothesis, thenotorious problem of set theory, proved independent of ZFC by Cohen in1963 (Cohen 1966).

Let \(\theta_{\textrm{CH}}\) be the sentence

Now \(\theta_{\textrm{CH}}\), which is a sentence of the emptyvocabulary, has a model if and only if the Continuum Hypothesis CHholds. Similarly, there is a sentence \(\theta_{\neg \textrm{CH}}\),which has a model if and only if the Continuum Hypothesis CH does nothold. This shows that the dependence of the semantics of second-orderlogic on the metatheoretic set theory is so deep that even questionsthat ZFC cannot solve can determine the truth or falsity of a sentencein a model.

The curious quality of second-order logic is that the truth of asentence such as \(\theta_{\textrm{CH}}\) in a big enough model of theempty vocabulary is equivalent to the truth of the ContinuumHypothesis in the set-theoretical universe. By the same techniquealmost any set-theoretical statement can be turned into a sentence ofsecond-order logic, the truth of which in a big enough model of theempty vocabulary is equivalent to the truth of the statement in theset-theoretical universe. Somehow second-order logic manages to readthe background set theory correctly. Does this mean that second-orderlogic is set theory in “sheep’s clothing”?

5.4 Does second-order logic depend on the Axiom of Choice?

The Axiom of Choice (AC) is a philosophical puzzle in the foundationsof mathematics. Roughly speaking, this axiom, that originally emergedin set theory, says that if we have a set \(A\) of non-empty disjointsets, then we can form a new set \(B\) which contains exactly oneelement from each set in \(A\). What can be seen as a problem is thefact that when \(A\) is infinite, forming the set \(B\) seems torequire making an infinite number of choices. See entry onAxiom of Choice for a thorough definition and discussion. On the one hand the Axiomof Choice seems magic, for example when it implies that the wildestsets have a well-ordering. On the other hand it seems innocuous, forexample when it implies that the Cartesian product of a family ofnon-empty sets is non-empty. The Axiom of Choice is typically used toconstruct odd “paradoxical” sets, such as a non-Lebesguemeasurable set of real numbers, a well-ordering of the real numbers, aparadoxical decomposition of the sphere (see entry onset theory), and so on. Such sets are usually in one sense or another undefinable.For example, a non-Lebesgue measurable set of real numbershas to be undefinable in second-order logic over\((\oN,+,\cdot)\), if there are sufficiently large cardinals (see theentry onlarge cardinals and determinacy).

The puzzling Axiom of Choice arises also in the middle of second-orderlogic: Let \(\theta\) be the sentence

Then \(\oR\models\theta\) essentially says that if a binary relation\(X\) relates to each \(x\in\oR\) a non-empty set \(\{y\in\oR :X(x,y)\}\), then there is a function \(F\) which chooses for each\(x\in\oR\) some \(y=F(x)\) such that \(X(x,y)\). In set theory thisis one of many equivalent ways of saying that the Axiom of Choiceholds for (continuum size) families of subsets of \(\oR\). The basictenet of second-order logic is that “all” properties ofelements of a fixed domain exist and we can quantify over them. Inset-theoretical terms this means that all subsets, definable or not,of a set of any cardinality exist and we can quantify over them. Inthis spirit the Axiom of Choice seems innocent and is usually acceptedin the literature of second-order logic.

By Cohen’s results (1966) there areN and \(N'\)satisfying the axioms of ZF (without the Axiom of Choice) such that“\(\oN\models\theta\)” holds inN but does not holdin \(N'\). This is a further demonstration of the dependence of thesemantics of second-order logic on the metatheory.

6. Non-Absoluteness of Truth in Second-Order Logic

Absoluteness is one of the most important concepts of logic. It wasused already in 1939 by Gödel in his analysis of the hierarchy ofconstructible sets (1939 [1990: 46]) towards proving the consistencyof the Continuum Hypothesis. It is briefly mentioned by Gödelthree years earlier in connection with the notion of computability(1936 [1986: 397]).

Intuitively speaking, a concept is absolute if its meaning isindependent of the formalism used, or in other words, if its meaningin the formal sense is the same as its meaning in the “realworld”. This may sound very vague and inexact. However,absoluteness has a perfectly exact technical definition in settheory.

Recall that a seta is calledtransitive if everyelement of an element ofa is an element ofa. Atransitive model is a model \((M,\in)\) such thatM istransitive. By the Mostowski Collapsing Lemma (Mostowski 1949) everywell-founded model \((M,E)\) of the Axiom of Extensionality isisomorphic to a unique transitive model. A basic property oftransitive models \((M,\in)\) is that if \(a,b\in M\), then \(M\modelsa\subseteq b\) if and only if \(a\subseteq b\). (If all elements ofa that are inM are inb then all elements ofa are inb, as by transitivity ofM, elements ofa are necessarily elements ofM.) We could express thisby saying that the formula \(x\subseteq y\) is absolute in transitivemodels. More generally, we say that a formula \(\phi(x_1,\ldots,x_n)\)of the first order language of set theory isabsoluterelative to ZFC if there is a finite \(T\subseteq \ZFC\) such that forall transitive models \((M,\in)\) ofT and all\(a_1,\ldots,a_n\in M\) we have

This definition of absoluteness is equivalent to the following moresyntactic condition (Feferman & Kreisel 1966): there are a\(\Sigma_1\)-formula \(\exists y\,\psi(y,x_1,\ldots,x_n)\) and a\(\Pi_1\)-formula \(\forall y\,\theta(y,x_1,\ldots,x_n)\) such that

and

In such a case we say that \(\phi(x_1,\ldots,x_n)\) is\(\Delta_1^{\text{ZFC}}\).

For first order logic it can be proved that“\(\mm\models_s\phi\)” is an absolute property of \(\mm\),s and \(\phi\) relative to ZFC. In fact, this is true even ifZFC is replaced by the weaker Kripke-Platek set theory KP (see Barwise1972a). The usual Tarski Truth Definition of first order logic can bewritten in \(\Delta_1^{\text{ZFC}}\) form. For second-order logic thepropositions “\(\phi\) is a second-order formula”,“\(\mm\) is anL-structure” and “s isan assignment” are all absolute relative to ZFC as well, but“\(\mm\models_s\phi\)” is not, as we shall now see. Thisis a crucial property of second-order logic. One may consider it aweakness, if one thinks of absoluteness as a desirable property, or astrength, if one takes non-absoluteness as a sign of expressive power.Whether a weakness or not, it is an important feature of second-orderlogic and a dominating topic in discussions about it. Second-orderlogic is, however, not the only non-absolute logic. For example,\(L(Q_1)\) (see the entry ongeneralized quantifiers) and \(L_{\omega_1\omega_1}\) (see then entry oninfinitary languages) are non-absolute, while \(L(Q_0)\) and \(L_{\omega_1\omega}\) areabsolute. The reason why \(L(Q_0)\) is absolute is essentially thatthe property of a set being infinite is absolute in transitive modelsof ZFC. Although the set of sentences of \(L_{\omega_1\omega}\) mayvary from one transitive model of ZFC to another, the truth of asentence of \(L_{\omega_1\omega}\) in a model is absolute intransitive models of ZFC essentially because the truth has a simpleinductive definition which only refers to subformulas of the sentenceand elements of the model.

Recall the definition of the sentence \(\theta_{\textrm{EC}}(P,R)\) in§5.3, which says that the interpretations of the predicatesP andR have the same cardinality. Cardinality is not an absoluteproperty. Two sets (even two ordinals) can be of different cardinalityin one transitive model of ZFC and of the same cardinality in atransitive extension. It is easy to see that“\(\mm\models_s\theta_{\textrm{EC}}(P,R)\)”is not absolute relative to ZFC. Essentially, the reason is that twosets have the same cardinality if there is a bijection between them.In a small transitive set it may happen that the sets are there butthe bijection manifesting their equicardinality is not. The bijectionmay be one obtained by the method of forcing. Or the lack of thebijection may be the result of applying the DownwardLöwenheim-Skolem Theorem^[6].

A more serious case of non-absoluteness is the sentence\(\theta_{\textrm{CH}}\) of§5.3. The sentence \(\theta_{\textrm{CH}}\) of the empty vocabulary has amodel if and only if the Continuum Hypothesis is true. If \(T\subseteq\ZFC\) is finite, then there are countable transitive models\(M\subseteq M'\) such that one, sayM, satisfies CH and theother, in this case \(M'\), does not (by Cohen 1966). InM thesentence \(\theta_{\textrm{CH}}\) has a model \(\ma\), that is,\(M\models\textrm{“}\ma\models\theta_{\textrm{CH}}\textrm{”}\). In\(M'\) the same sentence has no models, in particular \(M'\not\models\textrm{“}\ma\models\theta_{\textrm{CH}}\textrm{”}\). Thesituation is similar if the Continuum Hypothesis is replaced by theAxiom of Choice (see§5.4). Thus the property of a model satisfying a second-order sentence isnot absolute relative to ZFC. Even the property of a second-ordersentencehaving a model is not absolute relative to ZFC,because inM the sentence \(\theta_{\textrm{CH}}\) has a modelbut in \(M'\) not. For first order logic the property of a sentence ofhaving a model is co-r.e. and therefore arithmetical. Arithmeticalproperties are always absolute relative to ZFC.

The CH and the AC are central questions of set theory and subjects ofcontinuing debate. While the AC is mostly accepted as an axiom, and ispart of the ZFC axiom system, the CH is widely considered an openproblem. There are even suggestions (e.g., Feferman 1999) that itcannot be solved by any axiom system with the kind of generalacceptance that ZFC has. The formalist position in the foundations ofmathematics goes further and maintains that the question, what thetruth value of CH is, is meaningless. Both CH and its negation areconsistent with ZFC, assuming ZFC itself is consistent. According tothe formalist position the status of CH has been solved with this. Thesemantics of second-order logic depending on these hard questions ofset theory puts second-order logic into the same “basket”with set theory. Criticism of set theory becomes criticism ofsecond-order logic and vice versa.

Another indication of the dependence of second-order logic on settheory as the metatheory is the result of Barwise to the effect thatthe existence of the Hanf number of second-order logic is not provablein set theory without a highly complex use of the Replacement Axiom(for details, see Barwise 1972b).

7. Model Theory of Second-Order Logic

Let us start by noting that there are some trivial consequences ofsecond-order logic being able to quantify over relations. For example,the Craig Interpolation Theorem holds for second-order logic fortrivial reasons: If the finite relational vocabulary of \(\phi\) isL, the finite relational vocabulary of \(\phi'\) is \(L'\) and\(\models\phi\to\phi',\) then there is \(\theta\) such that\(\models\phi\to\theta\text{ and } \models\theta\to\phi'\) and thevocabulary of \(\theta\) is \(L\cap L'\), because we can let\(\theta\) be the sentence \(\exists X_1\ldots\exists X_n\,\phi\),where \(L\setminus L'=\{X_1,\ldots, X_n\}\). We can additionallydemand that every predicate symbol occurring positively in \(\theta\)occurs positively in \(\phi\) and \(\psi\), and every predicate symboloccurring negatively in \(\theta\) occurs negatively in \(\phi\) and\(\psi\) (theLyndon Interpolation Theorem [Lyndon 1959]). Inthe same way the Beth Definability Theorem holds for trivial reasons,also some preservation results^[7] have a trivial proof. For a negative result, see Craig 1965.

However, second-order logic does not have a model theory in the samesense as first order logic does. There is no Compactness Theorem toproduce non-standard models. One reason why first order logic has sucha rich model theory is that first order logic is relatively weak.Countable first order theories that have infinite models have modelsof all infinite cardinalities. This is a consequence of a weakness offirst order logic: its sentences cannot limit the size of the modelunless the size is finite. In model theory this weakness is turned toa strength: the structure of models of first order theories can beanalyzed in interesting ways. See the entry onmodel theory for examples of this.

Second-order theories can typically have just one model up toisomorphism. Thus if we investigate the class of models of asecond-order sentence, the class may very well consist of just onemodel, up to isomorphism. With just one model one cannot reallydevelop a model theory. One ends up investigating the one and onlymodel and there are no compelling reasons to use logic in the study ofit. If the one and only model is an algebraic structure, one shoulduse algebra to study it. If it is an ordered structure, one should usethe general theory of ordered structures to study it, and so on. It isunlikely that being second-order characterizable (see§7.1) tells much about the structure. It reveals more about second-orderlogic in general. For example, being able to characterize thestructure of natural numbers means that the Compactness Theorem andthe Completeness Theorem fail. Being able to characterize the orderedfield of real numbers means that both the Downward and the UpwardLöwenheim-Skolem Theorems fail. It is from thisperspective—to understand second-order logic itself—thatit is interesting to know exactly which structures are second-ordercharacterizable up to isomorphism.

Let us finally compare the two hierarchies, the model theoretichierarchy \(\Sigma_n^1\cup\Pi_n^1\) inside second-order logic and theLevy hierarchy \(\Sigma_n\cup\Pi_n\) in set theory.

In the light of the above theorem second-order logic sits firmly onthe \(\Sigma_2\cup\Pi_2\)-level of set theoretic definability. This isa reason to consider second-order logicweaker than firstorder set theory. This sounds paradoxical. How can second-order logic,with all the power and non-first order properties it has, be weakerthan first order logic based set theory, when first order logic cannoteven express finiteness, countability, uncountability, and so on?Nevertheless the message ofTheorem 4 is undeniable. Perhaps this would not be so puzzling if we thought ofset theory as a very high order logic over the singleton of the emptyset. After all, set theory permits endless iterations of the power setoperation, while second-order logic permits only one iteration.

We start below with a subsection on models that can be characterizedin second-order logic by one sentence up to isomorphism. Anotherapproach to the model theory of second-order logic is to focus onmodels withlarge cardinal (inaccessible, measurable,supercompact cardinals) properties. This is the topic of§7.2. Finally, in§7.3 we consider the possibility of allowing the so-called general modelsintroduced in§9.1. In this case second-order logic becomes very much like first orderlogic. However, general models are mostly interesting when they areso-called Henkin models, i.e., they satisfy the so-calledComprehension Axioms. In Henkin models second-order logic satisfiesthe Compactness Theorem and other principles familiar from first ordermodel theory but no general structure- or classification theory existsyet, perhaps because the Comprehension Axioms bring in a lot ofcomplicated structure into the models.

8. Decidability Results

The second-order theory of even the empty vocabulary is undecidable,as we noted in§5.1. In contrast,monadic second-order logic gives rise to manyimportant decidability results. Let us first observe that (not only inthe empty vocabulary but also) in a monadic vocabulary, i.e., oneconsisting of monadic predicates only, monadic second-order logic iscertainly decidable as proved already in 1915 by Löwenheim (1915)in one of the earliest papers on the mathematical aspects of formallogic. Löwenheim’s result can be proved easily byquantifier elimination, or alternatively by the more recent method ofEhrenfeucht-Fraïssé-games (see§3). However, monadicthird (and higher) order logic in monadicvocabulary, with quantifiers over not only subsets and also over setsof subsets of the domain, is undecidable (Tharp 1973). We now focus onvocabularies which are not merely monadic.

Compared to a monadic vocabulary, the other extreme can be describedas follows: LetP be a ternary predicate (a “pairingfunction”) on a non-empty setS. Suppose that for every\(x,y\in S\) there is \(z\in S\) with \((x, y, z) \in P\) and forevery \(z\in S\) there is at most one pair \((x, y)\) with \((x, y, z)\in P\). Then the true (full) second-order theory ofS isinterpretable in the monadic theory of \((S, P)\) (Gurevich 1985). Inother words, in a context where a pairing function is present, as inset theory and number theory, no special advantage arises fromlimiting second-order logic to its monadic fragment.

The next step from a vocabulary consisting of only monadic predicatesis a vocabulary with exactly one unary function. To describe somehighly non-trivial results in this case we introduce the followingconcept, which has independent interest: Thespectrum of afirst or second-order sentence is the set of cardinalities of itsfinite models. Spectra were introduced by Scholz, see Durand, Jones,Makowsky, and More (2012) for a history. A spectrum is of coursealways recursive. In fact, a set of natural numbers is a spectrum of afirst order sentence iff it is in NEXPTIME, that is, recognizable by anondeterministic Turing machine in exponential time (Jones &Selman 1974). In the case of sentences with just one unary functionsymbol there is a surprising characterization. Let us call a setS of natural numberseventually periodic if there arenatural numbersN andp with \(p > 0\) such that foreveryn with \(n > N\), we have \(n \in S\) iff \(n +p \inS\).

In graphs monadic second-order logic can still express mostinteresting properties. For example, theconnectivity of thegraph (hereE is the edge relation) can be expressed by thesentence

and the3-colorability of the graph by the sentence

There is a wealth of decidability results of monadic second-orderlogic on linear orders, trees and graphs.

The proof goes via a reduction to automata. Anautomaton is arestricted form of a Turing machine. In an automaton the machine neverwrites on the tape, so the tape just contains the input (Rabin &Scott 1959). However, the computation may be infinite. The input isconsideredaccepted in the case of an infinite computation ifan accepting state is reached infinitely many times. (There are alsomore complicated criteria of acceptance). With monadic second-orderlogic we can guess an accepting computation of the automaton. It ispossible but more difficult to show that an automaton can check thetruth of a monadic second-order sentence. The monadic second-ordertheory of ordinals \((\alpha,<)\) have been studied extensivelyfrom the point of view of decidability. For example, the monadicsecond-order theory of all countable ordinals, the theory of\(\omega_1\), and the theory of all ordinals \(<\omega_2\) aredecidable (Büchi 1973), but ZFC cannot decide whether the monadicsecond-order theory of \(\omega_2\) is decidable (Gurevich, Magidor,& Shelah 1983).

9. Axioms of Second-Order Logic

Recall our convention: Whenever we use upper case Fraktur letters,such as \(\ma,\mb,\mm,\mn\) etc, to name a structure, we use the uppercase Italic versions of those letters, such as \(A,B,M,N\) etc, toname the domain of the structure.

The deductive system of second-order logic, presented first explicitlyin Hilbert-Ackermann (Hilbert & Ackermann 1938), is based on theobvious extension of axioms and rules of first order logic togetherwith theComprehension Axiom Schema, defined as follows:Suppose \(\phi(x_1,\ldots,x_n)\) is a second-order formula with\(x_1,\ldots, x_n\) among its free individual variables and thesecond-order variableR isnot free in \(\phi\). Thenthe following formula is an instance of the Comprehension AxiomSchema:

There is a similar schema for second-order formulas that define afunction but we omit it here.

An example of a very simple second-order inference in number theorywould be

A priori (\ref{CA}) might appear very strong as it stipulates theexistence of a relation. However, such anR seems reasonable toaccept because it is definable:

Our Comprehension Axiom Schema isimpredicative in the sensethat the boundn-ary relation variables which may potentiallyoccur in the formula \(\phi(a_1,\ldots, a_n)\) haveR in theirrange. In this sense second-order logic is utterly impredicative. TheComprehension Axiom Schema has weaker forms that are lessimpredicative. In theArithmetic Comprehension Schema weassume \(\phi(a_1,\ldots, a_n)\) is first order. In the\(\Pi^1_1\)-Comprehension Schema we assume \(\phi(a_1,\ldots, a_n)\)is \(\Pi^1_1\). In mathematical practice these two weaker principlesusually suffice, see Simpson (1999 [2009]) and§14.

Hilbert-Ackermann (1938) added to the proof system of second-orderlogic also two different schemas that they callAxioms ofChoice. We are used to thinking of the Axiom of Choice as aset-theoretical principle. But second-order logic has the samesituation with choice principles as set theory. It makes perfect sensein second-order logic to ask whether there is a well-order of thedomain. The existence of such a well-order does in general not followfrom the Comprehension Schema because the well-order may be---and islikely to be---undefinable. So the only way to get a well-order of,say, the real numbers, in second-order logic is to assume some form ofsecond-order Axiom of Choice. The first choice principle is

and the second is

where the formula \(\varphi'\) is obtained from the formula\(\varphi\) by replacing everywhere \(F(t_1,\ldots, t_k)\) by\(F'(t_1\ldots t_k,x_1,\ldots, x_m)\).

The first Axiom of Choice (AC) says intuitively that if a set

is non-empty, then there is a function which picks an element\(a_{n+1}\) from the set, using the parameters \(a_1,\ldots,a_{n}\) asarguments. The second Axiom of Choice (AC′) is a kind ofsecond-order choice: We have for all \(a_1,\ldots,a_n\) a functionF with the property \(\phi\), so in factF depends on\(a_1,\ldots, a_n\) and should be denoted \(F_{a_1\ldots a_n}\). What(AC′) says now is that we can collect the functions\(F_{a_1\ldots a_n}\) together to form just one function \(F'\) ofhigher arity such that

Although \(F'\) appears to be definable, this is not the case, as themapping

may be highly undefinable.

Naturally, we may also want to assume theWell-orderingPrinciple which states that there is a binary relation which is atotal order on the individuals and satisfies the condition that everynon-empty set of individuals has a least element in the order. It iseasy to see that this principle implies (AC′). In ZFC there arehundreds of equivalent formulations of the Axiom of Choice or weakerversions of it. Most of the formulations that are equivalent in ZFCare non-equivalent in second-order logic. This is because set theoryallows free movement between sets and their power sets, butsecond-order logic does not^[11]. To obtain similar equivalence proofs as in set theory, one would haveto move between second-order logic and third order logic, seeGaßner (1994) and Siskind, Mancosu & Shapiro (2023).

9.2 Axioms of infinity

Recall our convention: Whenever we use upper case Fraktur letters,such as \(\ma,\mb,\mm,\mn\) etc, to name a structure, we use the uppercase Italic versions of those letters, such as \(A,B,M,N\) etc, toname the domain of the structure.

The axioms of second-order logic are trivially true in a (full) modelwith just one element. This raises the question how to guarantee thatthere are more than one element in the domain. Of course, we can add,for everyn, an axiom which says that there are more thann elements. There are various ways to say in second-order logicwithone axiom that there areinfinitely manyindividuals. These are equivalent in full models but may benon-equivalent in Henkin models. Some are equivalent if the Axiom ofChoice is assumed. Let us call a second-order sentence \(\phi\) of theempty vocabulary anAxiom of Infinity if

An axiom of infinity can say in second-order logic that a propersubset of the domain has the same cardinality as the entire domain(i.e., that the domain is not Dedekind-finite), or that there is apartial order without a maximal element, or that there is a set with aunary function and a constant which constitute a structure isomorphicto \((\oN,s,0)\), or that the domain is the union of two disjoint setswhich have the same cardinality as the domain, and so on. As is thecase in set theory without the Axiom of Choice, the differentformulations of infiniteness need not be equivalent. In second-orderlogic the situation is even more diffuse because of the variety ofdifferent formulations of the Axiom of Choice. We refer to Asser(1981) for a discussion of the different variants and to Hasenjaeger(1961) for a proof that the various non-equivalent forms of Axioms ofInfinity form in a sense a dense set. For a survey of differentconcepts of finiteness, see de la Cruz (2002).

10. Categoricity

A theory in second (or first) order logic is said to becategorical if any two of its models are isomorphic. A singlesentence (which has a model) is categorical if and only if itcharacterizes some model up to isomorphism (see§7.1). A nice property of a categorical theory \(\Gamma\) is (semantic)completeness: Any sentence \(\phi\) in the language in whichthe theory is written is decided by \(\Gamma\) in the following sense.Either every model of \(\Gamma\) satisfies \(\phi\) or every model of\(\Gamma\) satisfies \(\neg\phi\). In other words, either \(\phi\) or\(\neg\phi\) is a (semantic) logical consequence of \(\Gamma\). Thereason is very simple: \(\Gamma\) has, up to isomorphism, only onemodelM. Since isomorphism preserves truth in second-orderlogic, \(\phi\) or \(\neg\phi\) is a (semantic) logical consequence of\(\Gamma\) according to whether \(\phi\) is true inM or falseinM.

If \(\phi\) is a second-order sentence we defined above \(\Mod(\phi)\)as the class \(\{\mm : \mm\models\phi\}\). If \(\phi\) characterizes\(\mm\) up to isomorphism, then, up to isomorphism,

The project of axiomatizing mathematical structures with second-ordersentences was so successful in the first quarter of the twentiethcentury that Carnap even proposed, inspired by Fraenkel (1919 [1928]),see Awodey and Reck 2002 for more on this, thateverymathematical structure is determined, up to isomorphism, by itssecond-order theory. There are trivial cardinality reasons why thiscould not possibly hold for all models of size \(2^\omega\) andlarger. There are simply not enough second-order theories incomparison with the number of non-isomorphic models. However, theproposal of Carnap is trivially true for finite models, and notentirely unreasonable for countable models. In fact Ajtai (1979)showed that it is consistent with ZFC, provided ZFC itself isconsistent, that any two countable structures in a finite vocabularythat satisfy the same second-order sentences are isomorphic. Ajtaishowed that it is also consistent with ZFC, provided ZFC itself isconsistent, that there are two countable structures in a finitevocabulary that satisfy the same second-order sentences without beingisomorphic. Thus Carnap’s conjecture (for countable models) isindependent of ZFC.

Solovay has made a posting in FOM (2006 [Other Internet Resources]) in which he shows that the related statement that every completesecond-order sentence is categorical, is independent of ZFC. Saarinen,Väänänen and Woodin (2024 [Other Internet Resources]) show that large cardinals, at least up to a supercomapct cardinals,cannot decide whether every complete second-order sentence iscategorical,

There is a strong form of categoricity which holds for Henkinstructures in important cases and agrees with the usual concept ofcategoricity in the case of full Henkin models. It builds on theremarkable ability of second-order logic to express its owncategoricity. The isomorphism \((M,R)\cong(M',R')\) of two structures\((M,R)\) and \((M',R')\), where the predicatesR and \(R'\)are, say, binary, can be expressed in second-order logic as follows,letting \(\ma=(A,M,M',R,R')\), whereA is any set containing\(M\cup M'\), \(M=U^\ma\), \(M'={U'}^\ma\), \(R=P^\ma\) and\(R'=P'^\ma\). Now

where \(\isom(U,P,U',P')\) is the sentence

This suggests that the categoricity of a sentence \(\theta(P)\) with abinary predicate symbolP can be redefined equivalently,^[18] letting \(\categ(\theta(P))\) be the sentence

as

In fact, this is how Tarski defines categoricity in Tarski (1956),(page 387). This leads us to define:

Internal categoricity could also be calledprovablecategoricity. The phrase ‘internal categoricity’ wasintroduced in the context of arithmetic in Walmsley (2002). It wasadvocated more generally in Väänänen (2012), with moredetails in Väänänen and Wang (2015). We refer to Buttonand Walsh (2016) as well as Maddy and Väänänen (2023) for a recentdiscussion on this concept.

Note that (\ref{internal}) is stronger than (\ref{redef}) becauseprovable sentences are certainly valid. Owing to the CompletenessTheorem we can rewrite (\ref{internal}) as

Thus internal categoricity means categoricity not only for ordinarymodels, i.e., full Henkin models, but categoricity inside an arbitraryHenkin model. Note that categoricity is a meta-theoretical concept asit refers to the semantics of second-order logic. In\(\categ(\theta(P))\) the categoricity of \(\theta(P)\) is written inthe language of second-order logic. That is, the categoricity, despitebeing a meta-theoretical concept, is written in the object language.It can be asked, whether this leads us to a different concept? Be thatas it may, when the meaning of \(\categ(\theta(P))\) is uncovered byconsidering its semantics in the meta-theory, the meaning is the sameas the meaning we give to the categoricity of \(\theta(P)\). In theconcept of internal categoricity we take advantage of this situationby switching from semantical meaning to proof-theoretic meaning: Weinsist that \(\categ(\theta(P))\) is (not only valid but even)provable. Proof-theory requires less meta-theory than semantics. Wecan investigate provability of second-order sentences even in numbertheory by using numbers to code sentences and proofs, as Gödeldid in his proof of the Incompleteness Theorem. Of course, theCompleteness Theorem brings us back to the semantics.

To verify the categoricity of a second-order sentence one has to gothrough infinite structures in a way which essentially calls for settheory. The situation with internal categoricity is different. Toverify the internal categoricity of a second-order sentence one justhas to produce a proof. So there is a dramatic difference. And stillinternal categoricity is stronger than categoricity. So it would befoolish to establish categoricity if one could establish even internalcategoricity. Fortunately, the classical examples of categoricalsentences are all internally categorical:

The concept of internal categoricity provides a bridge between fullsemantics and Henkin semantics. It works in the same way in both casesand shows that the full semantics is a limit case of Henkin semanticsbut does not have a monopoly when it comes to categoricity.

12. Higher Order Logic vis-à-vis Type Theory

There are many ways to further extend second-order logic. The mostobvious is third, fourth, and so on order logic. The generalprinciple, already recognized by Tarski (1933 [1956]), is that inhigher order logic one can formalize the semantics—definetruth—of lower order logic. Therefore one certainly gainsexpressive power by using higher order logic. Let us take numbertheory as an example. With first order logic we can express propertiessuch as “n is a prime number” and propositions suchas “there are infinitely many prime numbers”,Fermat’s Last Theorem and Goldbach’s Conjecture. Firstorder properties of natural numbers fall into a natural hierarchycalled thearithmetical hierarchy the levels of which aredenoted \(\Sigma^0_n\) and \(\Pi^0_n\). With second-order logic we cantalk about properties of sets of natural numbers, or in other words,properties of real numbers. In particular, we can define therationals. A continuous function on the real numbers is determined byits values on rationals. Also, an open set is determined by whichrational points it contains. Using these observations we can talkabout continuous functions and open sets of reals. Basic facts incalculus, such as Bolzano’s Theorem stating that “If acontinuous function has values of opposite sign inside an interval,then it has a root in that interval” are expressible insecond-order logic over the structure \((\oN,+,\cdot)\) of naturalnumbers. Second-order properties of natural numbers fall into anatural hierarchy called theanalytical hierarchy and itslevels are denoted \(\Sigma^1_n\) and \(\Pi^1_n\). With third orderlogic we can talk aboutsets of real numbers. We can writethe Continuum Hypothesis in third order logic and ask the hardquestion, whether the model \((\oN,+,\cdot)\) satisfies this sentence.Third order properties of natural numbers have again a naturalhierarchy and its levels are denoted \(\Sigma^2_n\) and\(\Pi^2_n\).

It is obvious that if we keep a base model, such as \((\oN,+,\cdot)\)fixed, and move to higher and higher order logic, we can express moreand more complicated concepts and propositions. However,third order logic over

is nothing more thansecond order logic over

where \(E\subseteq \oN\times\P(\oN)\) is the relation \(nEr\iff n\inr\), which again is nothing more thanfirst order logic over

where \(E'\subseteq \P(\oN)\times\P(\P(\oN)\) is the relation\(rE'X\iff r\in X\). Moreover, second-order logic over \(\mn_1\) isnothing more than first order logic over \(\mn_2\). When this line ofthought is taken to its limit we can see that first order logic overthe cumulative hierarchy of sets covers higher order logic over anyindividual level \(V_\alpha\) of the hierarchy. In a sense, firstorder logic over the cumulative hierarchy of sets is a very very highorder logic over \(\mn_1\).

There is a marked similarity in the way \(\mn_2\) arises from\(\mn_1\) and in the way \(\mn_3\) arises from \(\mn_2\). In bothcases we simply add a power set construction on top of what the modelalready has. Second-order logic alone is very good with power sets aswe saw in§5.3. A consequence of this is that all the higher order logics (of anyfinite order and up to a point also of infinite order) fromsecond-order on have Turing-equivalent decision problems and the sameHanf- and Löwenheim numbers (see§4). Thus, even though higher than second-order logics are strictlyspeaking stronger than second-order logic no difference can be seen bythe usual criteria of strength of expressive power.

Type theory is a systematic approach to higher order logics.Variables are assigned types, just as in second-order logic we havevariables for individual type, relation type and function type. In ahigher order logic it would make sense to have variables for relationsbetween objects of any lower types as well as functions mappingobjects of lower type to objects of lower type. In set theory objectshave a rank. Elements of a set have a lower rank than the set itself.However, the difference between set-theoretical rank and typing intype theory is that in set theory the rank can be computed when theset is known while in type theory the type of an object can be seenfrom the type of the variable that the object is the value of. In asense type theory imposes from the syntax a type for each objectconsidered while in set theory a set has a rank given by thesemantics. Arguably set theory gained dominance over type theory afterthe 1930s because of its simpler syntax and semantics. On the otherhand type theory is used in computer science, especially in the theoryof programming languages (see SEP entry ontype theory).

14. Second-Order Arithmetic

Owing to the central role that real numbers play in mathematics, thesecond-order theory of natural numbers, known assecond-orderarithmetic (Simpson 1999 [2009]), and denoted \(Z_2\), is animportant foundational theory. It is stronger than (first order) Peanoarithmetic but weaker than set theory. It has variables forindividuals thought of as natural numbers as well as variables forsets of natural numbers thought of as real numbers. In addition thereare \(+\) and \(\times\) for arithmetic operations on the individuals.As axioms \(Z_2\) has some rather obvious axioms about \(+\) and\(\times\), the Induction Axiom (\ref{ind}), and the axioms ofsecond-order logic, including the Comprehension Principles (\ref{CA}).A surprising amount of mathematics can be derived in \(Z_2\). We referto Simpson (1999 [2009]) for details. In a sense, \(Z_2\) is a greatsuccess story for second-order logic.

Reverse mathematics uses \(Z_2\) to isolate the exact axiomson which well-known theorems from mathematics rely. In a textbook suchtheorems are proved perhaps in an informal set theory, but how muchset theory is actually needed in each case? For example, we may askwhat is the weakest set of axioms from which the Bolzano-Weierstrass Theorem^[21] can be proved? How much set theory, comprehension, choice, induction,etc is needed? Since \(Z_2\) is a natural and sufficient environmentfor many mathematical theorems, it is an appropriate framework foranswering questions raised by the reverse mathematics program. Themain (but not the only) distinctions that are made in reversemathematics concern the amount of the Comprehension Principle that isneeded in proving this or that mathematical result. In particular, therole of Arithmetic and \(\Pi^1_1\)-Comprehension Principles isclarified. The basic theory of real numbers can be developed on thebasis of Arithmetic Comprehension only, but proofs relying on thenotion of a countable ordinal require the \(\Pi^1_1\)-ComprehensionPrinciple. Again, we refer to Simpson (1999 [2009]) for details.

16. Finite Model Theory

The rise of mathematical logic in the first half of the twentiethcentury was interwoven with different approaches to understanding theinfinite structures of the natural and the real numbers. With theemergence of computer science in the second half of the twentiethcentury logic went through a process of rebirth. The concepts of acomputation and of a database both emphasized the need to understandnot so much the finite/infinite distinction as the new measures ofdegrees of finiteness. For example, the question whether a problem canbe decided in polynomial time arose to challenge the well-developedtheory of what can be decided in finite time. The analogy betweenfinite relational structures and databases led to the emergence offinite model theory. For a good review we refer to Fagin(1993).

In the context of finite models second-order logic does not sufferfrom the same philosophical problems as in the context of infinitemodels. It is just one language among many others. One of the earlysuccesses was the result of Fagin (1974) to the effect that classes ofmodels definable in existential second-order logic, i.e., in the\(\Sigma^1_1\)-fragment, are exactly those that are NP, i.e., that canbe recognized by a non-deterministic Turing machine running in timewhich is polynomial in the size of the encoding of the model as abinary sequence. The question whether NP is closed under complementsis notoriously open. From the point of view of second-order logic thisis surprising because on all models, finite or infinite,\(\Sigma^1_1\) is of course not closed under complements. For example,the class of infinite models (in the empty vocabulary) is\(\Sigma^1_1\) but not \(\Pi^1_1\). Also, the class of well-orders is\(\Pi^1_1\) but not \(\Sigma^1_1\). Therefore the following earlyresult about second-order logic on finite models was remarkable. Here\(\mon\Sigma^1_1\) refers to \(\Sigma^1_1\) in monadic second-orderlogic, similarly \(\mon\Pi^1_1\).

This has subsequently been extended to graphs with certain otherstructure present, see Fagin, Stockmeyer, and Vardi (1995). The proofsuse the Ehrenfeucht-Fraïssé games (see§3.1) and their elaborations.

Let \(\Sigma^1_{1,m}\) denote the class of \(\Sigma^1_1\)-formulas\(\exists X_1\ldots\exists X_k\phi\), where the bound second-ordervariables \(X_i\) are at mostm-ary and \(\phi\) is firstorder. Similarly \(\Pi^1_{1,m}\) and \(\Delta^1_{1,m}\).

This highly non-trivial theorem is one of the corner stones of thestudy of second-order logic on finite structures. We do not knowwhether \(\Delta^1_1\) is different from \(\Sigma^1_1\) on finitestructures, but the above theorem gives an arity-based hierarchyresult inside \(\Delta^1_1\).