Second-order and Higher-order Logic

3. The Semantics of Second-Order Logic

In order to define the semantics of second-order logic we have to agree what our metalanguage is. This fact has nothing to do with second-order logic but is rather a general feature of semantics (Tarski 1933 [1956]). The most commonly used metalanguage for second-order logic is set theory. We thus give a set-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 of second-order logic. We cannot interpret all properties by sets, e.g. the property of being identical to oneself. But if the domain that the individual variables range over is taken to be a set, then we can meaningfully interpret properties of individuals in that domain as sets. If we want to interpret second-order logic in a domain which is too large to be a set, we can use the set-theoretical concept of a class (see entry on set theory for more on classes).

We use the same concept of an L-structure (or equivalently, an L-model) as in first order logic. That is, an L-structure \(\mm\) has a domain M, which is any non-empty set, an interpretation \(c^\mm \in M\) of any constant symbol c of L, an interpretation \(R^\mm \subseteq M^n\) of any n-ary relation symbol R of L, as well as an interpretation \(H^\mm : M^n \to M\) of any n-ary function symbol H of L. In principle, the domain could be a class but we disregard this possibility here. For a discussion on the set/class distinction in this context, we refer to Shapiro (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 Italic versions of those letters, such as \(M,N\) etc, to name the domain of the structure.

Given an L-structure \(\mm\), an assignment is a function s from variables to the domain M of \(\mm\) such that: if x is an individual variable, then \(s(x) \in M\); if X is relation variable of arity n, then \(s(X) \subseteq M^n\); if F is function variable of arity n, then \(s(F) : M^n \to M\). We use \(s(P/X)\) to denote the assignment which is otherwise as s except that the value at X has been changed to P. 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 individual variables as an assignment maps a \(0\)-ary function symbol simply to an element of \(M\). A \(0\)-ary relation symbol or variable is at the same time an atomic formula and a non-logical symbol. We disregards in the current presentation this potential notational confusion.

The value \(t^\mm\langle s\rangle\) of a term t in a model \(\mm\) under the interpretation s is defined as in first order logic.

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

In clause 1 of the above definition we follow the common practice of giving a set-theoretical interpretation to the predication \(X(t_1,\ldots,t_n)\). Having interpreted X 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) \in s(X)\). In clause 2 we interpret quantification over properties and relations as quantification over subsets of the cartesian product \(M^n\). Respectively, in clause 3 we interpret quantification over functions 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 define what it means for a formula \(\phi\) to be valid and for two formulas \(\phi\) and \(\psi\) to be logically equivalent. As in logic in general, we say that \(\phi\) is (logically) valid if \(\mm\models_s\phi\) holds for all \(\mm\) and all s. Likewise, we define \(\phi\) and \(\psi\) to be logically equivalent, \(\phi\equiv\psi\), if \(\phi\leftrightarrow\psi\) is valid. Two models \(\mm\) and \(\mn\) are said to be second-order equivalent, in symbols \(\mm\equiv_{L^2}\mn\) if for all sentences \(\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 these in the sense of set theory. Thus we interpret “for some \(P \subseteq M^n\)” as “for some set \(P \subseteq M^n\)” and “for some \(f:M^n\to M\)” as “for some set which is a function \(f:M^n\to M\)”.

For infinite M the collection of subsets of \(M^n\) and the set of functions \(M^n\to M\) are famously complex. Currently set theory (ZFC) cannot even decide how many subsets of an infinite set there are. The situation is quite different with first order logic. The respective concept “for some \(a \in M\)” is unproblematic, relatively speaking. Of course, depending on what M is, “for some \(a \in M\)” can be quite problematic 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 of first order logic, the reliance on the metatheory is of a lower degree than when we use set theory as the metatheory for the semantics of second order logic. The central concept, which explains the difference, is that of absoluteness. For details, see §6.

4. Properties of Second-Order Formulas

Many syntactic operations that we are used to in first order logic work equally well in second-order logic. One such is the operation of relativization, in which we want to limit what a formula expresses to a fixed part of the universe. For example, we may consider models where a certain unary predicate U is used for the set of natural numbers. Then we relativize our axioms of arithmetic to the predicate U. Some other part of the model may be used for the power set of the set of natural numbers. Then we relativize 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}\) is obtained by restricting the relations \(R^\mm\) and functions \(F^\mm\) to A. This does not always result in a structure but if it does, it is called the relativization of \(\mm\) to A. Suppose \(\phi=\phi(x_1,\ldots,x_n,X_1,\ldots,X_m,F_1,\ldots,F_k)\) is a second-order formula and U is a unary relation variable. There is a second-order formula \(\phi^{U}\), the relativization of \(\phi\) to U, such that for all \(\mm\) for which \(\mm^{U^\mm}\) is a structure:

Intuitively, \(\phi^{U}\) says about \(U^\mm\) what \(\phi\) says about M. To obtain \(\phi^{U}\) from \(\phi\) one restricts all the first order quantifiers to elements of U and second-order quantifiers to subsets, relations and functions on U.

Hierarchies based on quantifier structure are a useful method to compare the definability of concepts in different systems. In first order logic it was observed very early on that formulas can be brought into a logically equivalent Prenex Normal Form in which all quantifiers occur in the beginning of the formula. This is possible also in second-order logic and the proof is essentially the same. Moreover, using the equivalence (which is reminiscent of a principle of set theory called Axiom of Choice, to which we return in Section 5.4., since in the below formula the relation \(Y\) in a sense chooses one \(X\) for each \(x\) and puts them together into one relation \(Y\) – see entry on Axiom of Choice for more on the topic.)

where the arity of Y is one higher than the arity of X, 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 every second-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 formula are in the front.

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

We have considered above only quantifiers that bind relation variables but the situation is exactly the same if we had bound function variables.

These classes of formulas have some obvious closure properties: They are all closed, up to logical equivalence, under \(\land , \lor\), and first order quantifiers. Moreover, the hierarchy is proper in the sense 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 order quantifiers. By Craig’s Interpolation Theorem, \(\Delta^1_1\)-formulas are logically equivalent to first order formulas ^[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 above hierarchy result (\ref{kurat}) shows that this cannot literally be true. To see this, i.e., to see what the reduction of second-order logic to its \(\Pi^1_1\)-part means, let L be a vocabulary, E a binary and U a unary relation symbol, both not in L. 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\) and for all \(a,b\in M\), \(E^\mm(a,b)\leftrightarrow a\in b\). In such a model monadic second-order formulas \(\phi\) over \(U^\mm\) can be reduced to first order formulas \(\phi^*\) over M. This reduction, due to Hintikka (1955) and further developed by Montague (1963), shows that \(\Pi^1_1\)-formulas alone are enough to express any second-order property with extra predicates. The idea can be extended to third and higher order logic, and also to non-monadic second-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 whether a 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\). This means that the Löwenheim number^[4] and the Hanf number^[5] of the entire second-order logic are the same as those of the fragment \(\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 in expressive power as n increases, but a more careful analysis reveals that already the first level \(\Sigma^1_1\cup \Pi^1_1\) has the power of all the levels \(\Sigma^1_n, \Pi^1_n\) even if the power is somewhat implicit and needs to be brought to light.

In set theory there is the Levy-hierarchy of \(\Sigma_n\)- and \(\Pi_n\)-formulas (Lévy 1965). Formulas where all quantifiers are bounded, i.e., of the form \(\forall x\in y\) or of the form \(\exists x\in y\) for some x and y, are called \(\Sigma_0\) or equivalently \(\Pi_0\). Formulas of the form \(\forall x\,\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 for the 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 reduce the 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 problem gets more and more complicated, and the numbers obtained get bigger and bigger as n increases (see Theorem 4; Väänänen 1979).

The hierarchy \(\Sigma_n^1\cup \Pi_n^1\) inside second-order logic and the hierarchy \(\Sigma_n\cup\Pi_n\) in set theory, are further compared 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 now uncover in detail. Above we characterized the structure of the natural numbers by means of (\ref{ind}). This application of second-order logic is perhaps the most famous and most important. We now reformulate this in a slightly more general form in order to get more power out of it. Suppose U is a unary relation variable (“the set of natural numbers”), G a unary function variable (“the successor function”), and z an individual 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-order logic to say that the U-part of any model of \(\theta_{\textrm{PA}}(U,G,z)\), together with the function G and the individual z are isomorphic to the natural numbers \(\oN\) with their successor function and zero. There are many ways to see that no first order sentence can have this property. For example, by the Compactness Theorem such a sentence would have also a non-standard model where some element is different from each in the sequence z, \(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 may conclude that the Compactness Theorem does not hold for second-order logic 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)\). A first 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 by results of Gödel (1931 [1986: 144–195]) and Tarski (1933 [1956]). This shows that second-order logic is not completely axiomatizable by effective means, or decidable even in the empty vocabulary. That is, there is no decidable second-order theory with an infinite model. This is in sharp contrast to first order logic where the following theories are decidable: first order logic with empty vocabulary, first order logic with monadic predicates, dense linear order, 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 respective second-order theories are decidable. However, if we restrict second-order logic to monadic second-order logic, we obtain many important decidable theories (see §8).

5.2 The collapse of the Completeness Theorem

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

Behind the failure of the Completeness Theorem is the fact that second-order logic is—almost by definition—able to say that a set is the power set of another set. What this means is the following: Let L be a vocabulary. Let E be a binary and U a unary relation symbol, both not in L. 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 necessarily uncountable. This shows that second-order logic, unlike first order logic, has sentences with models but only uncountable ones. Thus the Downward Löwenheim-Skolem Theorem fails for second-order logic, as we already noted above. Combining (\ref{papow}) with the observations in §5.1 yields the following result (by validity we mean the set of Gödel numbers of valid formulas):

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

5.3 “Set theory in sheep’s clothing”

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

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

Let us see where this opinion might come from. First we observe that a very simple, indeed a very basic, second-order formula can say that two sets have the same cardinality: Suppose P and R are unary 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 sets M and \(s(R)\) have the same cardinality. We will use these formulas to launch an attack on the Continuum Hypothesis, the notorious problem of set theory, proved independent of ZFC by Cohen in 1963 (Cohen 1966).

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

Now \(\theta_{\textrm{CH}}\), which is a sentence of the empty vocabulary, has a model if and only if the Continuum Hypothesis CH holds. Similarly, there is a sentence \(\theta_{\neg \textrm{CH}}\), which has a model if and only if the Continuum Hypothesis CH does not hold. This shows that the dependence of the semantics of second-order logic on the metatheoretic set theory is so deep that even questions that ZFC cannot solve can determine the truth or falsity of a sentence in a model.

The curious quality of second-order logic is that the truth of a sentence such as \(\theta_{\textrm{CH}}\) in a big enough model of the empty vocabulary is equivalent to the truth of the Continuum Hypothesis in the set-theoretical universe. By the same technique almost any set-theoretical statement can be turned into a sentence of second-order logic, the truth of which in a big enough model of the empty vocabulary is equivalent to the truth of the statement in the set-theoretical universe. Somehow second-order logic manages to read the background set theory correctly. Does this mean that second-order logic 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 foundations of mathematics. Roughly speaking, this axiom, that originally emerged in set theory, says that if we have a set \(A\) of non-empty disjoint sets, then we can form a new set \(B\) which contains exactly one element from each set in \(A\). What can be seen as a problem is the fact that when \(A\) is infinite, forming the set \(B\) seems to require making an infinite number of choices. See entry on Axiom of Choice for a thorough definition and discussion. On the one hand the Axiom of Choice seems magic, for example when it implies that the wildest sets have a well-ordering. On the other hand it seems innocuous, for example when it implies that the Cartesian product of a family of non-empty sets is non-empty. The Axiom of Choice is typically used to construct odd “paradoxical” sets, such as a non-Lebesgue measurable set of real numbers, a well-ordering of the real numbers, a paradoxical decomposition of the sphere (see entry on set theory), and so on. Such sets are usually in one sense or another undefinable. For example, a non-Lebesgue measurable set of real numbers has to be undefinable in second-order logic over \((\oN,+,\cdot)\), if there are sufficiently large cardinals (see the entry on large cardinals and determinacy).

The puzzling Axiom of Choice arises also in the middle of second-order logic: 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 this is one of many equivalent ways of saying that the Axiom of Choice holds for (continuum size) families of subsets of \(\oR\). The basic tenet of second-order logic is that “all” properties of elements of a fixed domain exist and we can quantify over them. In set-theoretical terms this means that all subsets, definable or not, of a set of any cardinality exist and we can quantify over them. In this spirit the Axiom of Choice seems innocent and is usually accepted in the literature of second-order logic.

By Cohen’s results (1966) there are N and \(N'\) satisfying the axioms of ZF (without the Axiom of Choice) such that “\(\oN\models\theta\)” holds in N but does not hold in \(N'\). This is a further demonstration of the dependence of the semantics 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 was used already in 1939 by Gödel in his analysis of the hierarchy of constructible sets (1939 [1990: 46]) towards proving the consistency of the Continuum Hypothesis. It is briefly mentioned by Gödel three years earlier in connection with the notion of computability (1936 [1986: 397]).

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

Recall that a set a is called transitive if every element of an element of a is an element of a. A transitive model is a model \((M,\in)\) such that M is transitive. By the Mostowski Collapsing Lemma (Mostowski 1949) every well-founded model \((M,E)\) of the Axiom of Extensionality is isomorphic to a unique transitive model. A basic property of transitive models \((M,\in)\) is that if \(a,b\in M\), then \(M\models a\subseteq b\) if and only if \(a\subseteq b\). (If all elements of a that are in M are in b then all elements of a are in b, as by transitivity of M, elements of a are necessarily elements of M.) We could express this by saying that the formula \(x\subseteq y\) is absolute in transitive models. More generally, we say that a formula \(\phi(x_1,\ldots,x_n)\) of the first order language of set theory is absolute relative to ZFC if there is a finite \(T\subseteq \ZFC\) such that for all transitive models \((M,\in)\) of T and all \(a_1,\ldots,a_n\in M\) we have

This definition of absoluteness is equivalent to the following more syntactic 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 if ZFC is replaced by the weaker Kripke-Platek set theory KP (see Barwise 1972a). The usual Tarski Truth Definition of first order logic can be written in \(\Delta_1^{\text{ZFC}}\) form. For second-order logic the propositions “\(\phi\) is a second-order formula”, “\(\mm\) is an L-structure” and “s is an assignment” are all absolute relative to ZFC as well, but “\(\mm\models_s\phi\)” is not, as we shall now see. This is a crucial property of second-order logic. One may consider it a weakness, if one thinks of absoluteness as a desirable property, or a strength, if one takes non-absoluteness as a sign of expressive power. Whether a weakness or not, it is an important feature of second-order logic and a dominating topic in discussions about it. Second-order logic is, however, not the only non-absolute logic. For example, \(L(Q_1)\) (see the entry on generalized quantifiers) and \(L_{\omega_1\omega_1}\) (see then entry on infinitary languages) are non-absolute, while \(L(Q_0)\) and \(L_{\omega_1\omega}\) are absolute. The reason why \(L(Q_0)\) is absolute is essentially that the property of a set being infinite is absolute in transitive models of ZFC. Although the set of sentences of \(L_{\omega_1\omega}\) may vary from one transitive model of ZFC to another, the truth of a sentence of \(L_{\omega_1\omega}\) in a model is absolute in transitive models of ZFC essentially because the truth has a simple inductive definition which only refers to subformulas of the sentence and 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 predicates P and R have the same cardinality. Cardinality is not an absolute property. Two sets (even two ordinals) can be of different cardinality in one transitive model of ZFC and of the same cardinality in a transitive 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 two sets have the same cardinality if there is a bijection between them. In a small transitive set it may happen that the sets are there but the bijection manifesting their equicardinality is not. The bijection may be one obtained by the method of forcing. Or the lack of the bijection may be the result of applying the Downward Lö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 a model 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, say M, satisfies CH and the other, in this case \(M'\), does not (by Cohen 1966). In M the sentence \(\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{”}\). The situation is similar if the Continuum Hypothesis is replaced by the Axiom of Choice (see §5.4). Thus the property of a model satisfying a second-order sentence is not absolute relative to ZFC. Even the property of a second-order sentence having a model is not absolute relative to ZFC, because in M the sentence \(\theta_{\textrm{CH}}\) has a model but in \(M'\) not. For first order logic the property of a sentence of having a model is co-r.e. and therefore arithmetical. Arithmetical properties are always absolute relative to ZFC.

The CH and the AC are central questions of set theory and subjects of continuing debate. While the AC is mostly accepted as an axiom, and is part of the ZFC axiom system, the CH is widely considered an open problem. There are even suggestions (e.g., Feferman 1999) that it cannot be solved by any axiom system with the kind of general acceptance that ZFC has. The formalist position in the foundations of mathematics goes further and maintains that the question, what the truth value of CH is, is meaningless. Both CH and its negation are consistent with ZFC, assuming ZFC itself is consistent. According to the formalist position the status of CH has been solved with this. The semantics of second-order logic depending on these hard questions of set theory puts second-order logic into the same “basket” with set theory. Criticism of set theory becomes criticism of second-order logic and vice versa.

Another indication of the dependence of second-order logic on set theory as the metatheory is the result of Barwise to the effect that the existence of the Hanf number of second-order logic is not provable in 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 of second-order logic being able to quantify over relations. For example, the Craig Interpolation Theorem holds for second-order logic for trivial reasons: If the finite relational vocabulary of \(\phi\) is L, 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 the vocabulary 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 additionally demand that every predicate symbol occurring positively in \(\theta\) occurs positively in \(\phi\) and \(\psi\), and every predicate symbol occurring negatively in \(\theta\) occurs negatively in \(\phi\) and \(\psi\) (the Lyndon Interpolation Theorem [Lyndon 1959]). In the 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 same sense as first order logic does. There is no Compactness Theorem to produce non-standard models. One reason why first order logic has such a rich model theory is that first order logic is relatively weak. Countable first order theories that have infinite models have models of all infinite cardinalities. This is a consequence of a weakness of first order logic: its sentences cannot limit the size of the model unless the size is finite. In model theory this weakness is turned to a strength: the structure of models of first order theories can be analyzed in interesting ways. See the entry on model theory for examples of this.

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

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

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

We start below with a subsection on models that can be characterized in second-order logic by one sentence up to isomorphism. Another approach to the model theory of second-order logic is to focus on models with large 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 models introduced in §9.1. In this case second-order logic becomes very much like first order logic. However, general models are mostly interesting when they are so-called Henkin models, i.e., they satisfy the so-called Comprehension Axioms. In Henkin models second-order logic satisfies the Compactness Theorem and other principles familiar from first order model theory but no general structure- or classification theory exists yet, perhaps because the Comprehension Axioms bring in a lot of complicated 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 many important decidability results. Let us first observe that (not only in the empty vocabulary but also) in a monadic vocabulary, i.e., one consisting of monadic predicates only, monadic second-order logic is certainly decidable as proved already in 1915 by Löwenheim (1915) in one of the earliest papers on the mathematical aspects of formal logic. Löwenheim’s result can be proved easily by quantifier elimination, or alternatively by the more recent method of Ehrenfeucht-Fraïssé-games (see §3). However, monadic third (and higher) order logic in monadic vocabulary, with quantifiers over not only subsets and also over sets of subsets of the domain, is undecidable (Tharp 1973). We now focus on vocabularies which are not merely monadic.

Compared to a monadic vocabulary, the other extreme can be described as follows: Let P be a ternary predicate (a “pairing function”) on a non-empty set S. Suppose that for every \(x,y\in S\) there is \(z\in S\) with \((x, y, z) \in P\) and for every \(z\in S\) there is at most one pair \((x, y)\) with \((x, y, z) \in P\). Then the true (full) second-order theory of S is interpretable in the monadic theory of \((S, P)\) (Gurevich 1985). In other words, in a context where a pairing function is present, as in set theory and number theory, no special advantage arises from limiting second-order logic to its monadic fragment.

The next step from a vocabulary consisting of only monadic predicates is a vocabulary with exactly one unary function. To describe some highly non-trivial results in this case we introduce the following concept, which has independent interest: The spectrum of a first or second-order sentence is the set of cardinalities of its finite models. Spectra were introduced by Scholz, see Durand, Jones, Makowsky, and More (2012) for a history. A spectrum is of course always recursive. In fact, a set of natural numbers is a spectrum of a first order sentence iff it is in NEXPTIME, that is, recognizable by a nondeterministic Turing machine in exponential time (Jones & Selman 1974). In the case of sentences with just one unary function symbol there is a surprising characterization. Let us call a set S of natural numbers eventually periodic if there are natural numbers N and p with \(p > 0\) such that for every n with \(n > N\), we have \(n \in S\) iff \(n +p \in S\).

In graphs monadic second-order logic can still express most interesting properties. For example, the connectivity of the graph (here E is the edge relation) can be expressed by the sentence

and the 3-colorability of the graph by the sentence

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

The proof goes via a reduction to automata. An automaton is a restricted form of a Turing machine. In an automaton the machine never writes on the tape, so the tape just contains the input (Rabin & Scott 1959). However, the computation may be infinite. The input is considered accepted in the case of an infinite computation if an accepting state is reached infinitely many times. (There are also more complicated criteria of acceptance). With monadic second-order logic we can guess an accepting computation of the automaton. It is possible but more difficult to show that an automaton can check the truth of a monadic second-order sentence. The monadic second-order theory of ordinals \((\alpha,<)\) have been studied extensively from the point of view of decidability. For example, the monadic second-order theory of all countable ordinals, the theory of \(\omega_1\), and the theory of all ordinals \(<\omega_2\) are decidable (Büchi 1973), but ZFC cannot decide whether the monadic second-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 upper case Italic versions of those letters, such as \(A,B,M,N\) etc, to name the domain of the structure.

The deductive system of second-order logic, presented first explicitly in Hilbert-Ackermann (Hilbert & Ackermann 1938), is based on the obvious extension of axioms and rules of first order logic together with the Comprehension 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 the second-order variable R is not free in \(\phi\). Then the following formula is an instance of the Comprehension Axiom Schema:

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

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

A priori (\ref{CA}) might appear very strong as it stipulates the existence of a relation. However, such an R seems reasonable to accept because it is definable:

Our Comprehension Axiom Schema is impredicative in the sense that the bound n-ary relation variables which may potentially occur in the formula \(\phi(a_1,\ldots, a_n)\) have R in their range. In this sense second-order logic is utterly impredicative. The Comprehension Axiom Schema has weaker forms that are less impredicative. In the Arithmetic Comprehension Schema we assume \(\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 principles usually suffice, see Simpson (1999 [2009]) and §14.

Hilbert-Ackermann (1938) added to the proof system of second-order logic also two different schemas that they call Axioms of Choice. We are used to thinking of the Axiom of Choice as a set-theoretical principle. But second-order logic has the same situation with choice principles as set theory. It makes perfect sense in second-order logic to ask whether there is a well-order of the domain. The existence of such a well-order does in general not follow from the Comprehension Schema because the well-order may be---and is likely 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 of second-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}\) as arguments. The second Axiom of Choice (AC′) is a kind of second-order choice: We have for all \(a_1,\ldots,a_n\) a function F with the property \(\phi\), so in fact F 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'\) of higher arity such that

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

may be highly undefinable.

Naturally, we may also want to assume the Well-ordering Principle which states that there is a binary relation which is a total order on the individuals and satisfies the condition that every non-empty set of individuals has a least element in the order. It is easy to see that this principle implies (AC′). In ZFC there are hundreds of equivalent formulations of the Axiom of Choice or weaker versions of it. Most of the formulations that are equivalent in ZFC are non-equivalent in second-order logic. This is because set theory allows free movement between sets and their power sets, but second-order logic does not^[11]. To obtain similar equivalence proofs as in set theory, one would have to move between second-order logic and third order logic, see Gaß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 upper case Italic versions of those letters, such as \(A,B,M,N\) etc, to name the domain of the structure.

The axioms of second-order logic are trivially true in a (full) model with just one element. This raises the question how to guarantee that there are more than one element in the domain. Of course, we can add, for every n, an axiom which says that there are more than n elements. There are various ways to say in second-order logic with one axiom that there are infinitely many individuals. These are equivalent in full models but may be non-equivalent in Henkin models. Some are equivalent if the Axiom of Choice is assumed. Let us call a second-order sentence \(\phi\) of the empty vocabulary an Axiom of Infinity if

An axiom of infinity can say in second-order logic that a proper subset of the domain has the same cardinality as the entire domain (i.e., that the domain is not Dedekind-finite), or that there is a partial order without a maximal element, or that there is a set with a unary function and a constant which constitute a structure isomorphic to \((\oN,s,0)\), or that the domain is the union of two disjoint sets which have the same cardinality as the domain, and so on. As is the case in set theory without the Axiom of Choice, the different formulations of infiniteness need not be equivalent. In second-order logic the situation is even more diffuse because of the variety of different 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 of Infinity form in a sense a dense set. For a survey of different concepts of finiteness, see de la Cruz (2002).

10. Categoricity

A theory in second (or first) order logic is said to be categorical if any two of its models are isomorphic. A single sentence (which has a model) is categorical if and only if it characterizes 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 which the 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\). The reason is very simple: \(\Gamma\) has, up to isomorphism, only one model M. Since isomorphism preserves truth in second-order logic, \(\phi\) or \(\neg\phi\) is a (semantic) logical consequence of \(\Gamma\) according to whether \(\phi\) is true in M or false in M.

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-order sentences was so successful in the first quarter of the twentieth century that Carnap even proposed, inspired by Fraenkel (1919 [1928]), see Awodey and Reck 2002 for more on this, that every mathematical structure is determined, up to isomorphism, by its second-order theory. There are trivial cardinality reasons why this could not possibly hold for all models of size \(2^\omega\) and larger. There are simply not enough second-order theories in comparison with the number of non-isomorphic models. However, the proposal of Carnap is trivially true for finite models, and not entirely unreasonable for countable models. In fact Ajtai (1979) showed that it is consistent with ZFC, provided ZFC itself is consistent, that any two countable structures in a finite vocabulary that satisfy the same second-order sentences are isomorphic. Ajtai showed that it is also consistent with ZFC, provided ZFC itself is consistent, that there are two countable structures in a finite vocabulary that satisfy the same second-order sentences without being isomorphic. Thus Carnap’s conjecture (for countable models) is independent of ZFC.

Solovay has made a posting in FOM (2006 [Other Internet Resources]) in which he shows that the related statement that every complete second-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 is categorical,

There is a strong form of categoricity which holds for Henkin structures in important cases and agrees with the usual concept of categoricity in the case of full Henkin models. It builds on the remarkable ability of second-order logic to express its own categoricity. The isomorphism \((M,R)\cong(M',R')\) of two structures \((M,R)\) and \((M',R')\), where the predicates R and \(R'\) are, say, binary, can be expressed in second-order logic as follows, letting \(\ma=(A,M,M',R,R')\), where A 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 a binary predicate symbol P 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 called provable categoricity. The phrase ‘internal categoricity’ was introduced in the context of arithmetic in Walmsley (2002). It was advocated more generally in Väänänen (2012), with more details in Väänänen and Wang (2015). We refer to Button and Walsh (2016) as well as Maddy and Väänänen (2023) for a recent discussion on this concept.

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

Thus internal categoricity means categoricity not only for ordinary models, i.e., full Henkin models, but categoricity inside an arbitrary Henkin model. Note that categoricity is a meta-theoretical concept as it refers to the semantics of second-order logic. In \(\categ(\theta(P))\) the categoricity of \(\theta(P)\) is written in the language of second-order logic. That is, the categoricity, despite being a meta-theoretical concept, is written in the object language. It can be asked, whether this leads us to a different concept? Be that as it may, when the meaning of \(\categ(\theta(P))\) is uncovered by considering its semantics in the meta-theory, the meaning is the same as the meaning we give to the categoricity of \(\theta(P)\). In the concept of internal categoricity we take advantage of this situation by switching from semantical meaning to proof-theoretic meaning: We insist that \(\categ(\theta(P))\) is (not only valid but even) provable. Proof-theory requires less meta-theory than semantics. We can investigate provability of second-order sentences even in number theory by using numbers to code sentences and proofs, as Gödel did in his proof of the Incompleteness Theorem. Of course, the Completeness Theorem brings us back to the semantics.

To verify the categoricity of a second-order sentence one has to go through infinite structures in a way which essentially calls for set theory. The situation with internal categoricity is different. To verify the internal categoricity of a second-order sentence one just has to produce a proof. So there is a dramatic difference. And still internal categoricity is stronger than categoricity. So it would be foolish to establish categoricity if one could establish even internal categoricity. Fortunately, the classical examples of categorical sentences are all internally categorical:

The concept of internal categoricity provides a bridge between full semantics and Henkin semantics. It works in the same way in both cases and shows that the full semantics is a limit case of Henkin semantics but 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 most obvious is third, fourth, and so on order logic. The general principle, already recognized by Tarski (1933 [1956]), is that in higher order logic one can formalize the semantics—define truth—of lower order logic. Therefore one certainly gains expressive power by using higher order logic. Let us take number theory as an example. With first order logic we can express properties such as “n is a prime number” and propositions such as “there are infinitely many prime numbers”, Fermat’s Last Theorem and Goldbach’s Conjecture. First order properties of natural numbers fall into a natural hierarchy called the arithmetical hierarchy the levels of which are denoted \(\Sigma^0_n\) and \(\Pi^0_n\). With second-order logic we can talk about properties of sets of natural numbers, or in other words, properties of real numbers. In particular, we can define the rationals. A continuous function on the real numbers is determined by its values on rationals. Also, an open set is determined by which rational points it contains. Using these observations we can talk about continuous functions and open sets of reals. Basic facts in calculus, such as Bolzano’s Theorem stating that “If a continuous function has values of opposite sign inside an interval, then it has a root in that interval” are expressible in second-order logic over the structure \((\oN,+,\cdot)\) of natural numbers. Second-order properties of natural numbers fall into a natural hierarchy called the analytical hierarchy and its levels are denoted \(\Sigma^1_n\) and \(\Pi^1_n\). With third order logic we can talk about sets of real numbers. We can write the Continuum Hypothesis in third order logic and ask the hard question, whether the model \((\oN,+,\cdot)\) satisfies this sentence. Third order properties of natural numbers have again a natural hierarchy 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 more and more complicated concepts and propositions. However, third order logic over

is nothing more than second order logic over

where \(E\subseteq \oN\times\P(\oN)\) is the relation \(nEr\iff n\in r\), which again is nothing more than first 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\) is nothing more than first order logic over \(\mn_2\). When this line of thought is taken to its limit we can see that first order logic over the cumulative hierarchy of sets covers higher order logic over any individual level \(V_\alpha\) of the hierarchy. In a sense, first order logic over the cumulative hierarchy of sets is a very very high order 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 both cases we simply add a power set construction on top of what the model already has. Second-order logic alone is very good with power sets as we saw in §5.3. A consequence of this is that all the higher order logics (of any finite order and up to a point also of infinite order) from second-order on have Turing-equivalent decision problems and the same Hanf- and Löwenheim numbers (see §4). Thus, even though higher than second-order logics are strictly speaking stronger than second-order logic no difference can be seen by the 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 have variables for individual type, relation type and function type. In a higher order logic it would make sense to have variables for relations between objects of any lower types as well as functions mapping objects of lower type to objects of lower type. In set theory objects have a rank. Elements of a set have a lower rank than the set itself. However, the difference between set-theoretical rank and typing in type theory is that in set theory the rank can be computed when the set is known while in type theory the type of an object can be seen from the type of the variable that the object is the value of. In a sense type theory imposes from the syntax a type for each object considered while in set theory a set has a rank given by the semantics. Arguably set theory gained dominance over type theory after the 1930s because of its simpler syntax and semantics. On the other hand type theory is used in computer science, especially in the theory of programming languages (see SEP entry on type theory).

14. Second-Order Arithmetic

Owing to the central role that real numbers play in mathematics, the second-order theory of natural numbers, known as second-order arithmetic (Simpson 1999 [2009]), and denoted \(Z_2\), is an important foundational theory. It is stronger than (first order) Peano arithmetic but weaker than set theory. It has variables for individuals thought of as natural numbers as well as variables for sets of natural numbers thought of as real numbers. In addition there are \(+\) 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 of second-order logic, including the Comprehension Principles (\ref{CA}). A surprising amount of mathematics can be derived in \(Z_2\). We refer to Simpson (1999 [2009]) for details. In a sense, \(Z_2\) is a great success story for second-order logic.

Reverse mathematics uses \(Z_2\) to isolate the exact axioms on which well-known theorems from mathematics rely. In a textbook such theorems are proved perhaps in an informal set theory, but how much set theory is actually needed in each case? For example, we may ask what 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 environment for many mathematical theorems, it is an appropriate framework for answering questions raised by the reverse mathematics program. The main (but not the only) distinctions that are made in reverse mathematics concern the amount of the Comprehension Principle that is needed in proving this or that mathematical result. In particular, the role of Arithmetic and \(\Pi^1_1\)-Comprehension Principles is clarified. The basic theory of real numbers can be developed on the basis of Arithmetic Comprehension only, but proofs relying on the notion of a countable ordinal require the \(\Pi^1_1\)-Comprehension Principle. Again, we refer to Simpson (1999 [2009]) for details.

16. Finite Model Theory

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

In the context of finite models second-order logic does not suffer from the same philosophical problems as in the context of infinite models. It is just one language among many others. One of the early successes was the result of Fagin (1974) to the effect that classes of models definable in existential second-order logic, i.e., in the \(\Sigma^1_1\)-fragment, are exactly those that are NP, i.e., that can be recognized by a non-deterministic Turing machine running in time which is polynomial in the size of the encoding of the model as a binary sequence. The question whether NP is closed under complements is notoriously open. From the point of view of second-order logic this is 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 early result about second-order logic on finite models was remarkable. Here \(\mon\Sigma^1_1\) refers to \(\Sigma^1_1\) in monadic second-order logic, similarly \(\mon\Pi^1_1\).

This has subsequently been extended to graphs with certain other structure present, see Fagin, Stockmeyer, and Vardi (1995). The proofs use 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-order variables \(X_i\) are at most m-ary and \(\phi\) is first order. Similarly \(\Pi^1_{1,m}\) and \(\Delta^1_{1,m}\).

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