First-order formal logic is a standard topic in computer science. Not so for second-order logic: which, though used the default in fields of mathematics such as topology and analysis, is usually not treated in standard courses in mathematical logic. For today’s Theory Lunch I discussed some classical theorems that hold for first-order logic, but not for second-order logic: my talk was based on Boolos’ classical textbook.

We consider languages made of symbols that represents either objects, or functions, or relations: in particular, unary relations, or equivalently, sets. A *sentence* on such a language is a finite sequence of symbols from the language and from the standard logical connectives and quantifiers ( for conjunction, for disjunction, for negation, etc.) according to the usual rules, such that every variable is bounded by some quantifier. A *first-order* sentence only has quantifiers on objects, while a *second-order* sentence can have quantifiers on functions and relations (in particular, sets) as well.

For example, the set is made of the following first-order sentences on the language :

Of course, second-order logic is much more expressive than first order logic. The natural question is: *how much*?

The answer is: possibly, *too much* more than we would like.

To discuss how it is so, we recall the notion of *model*. Informally, a model of a set of sentences is a “world” where all the sentences in the set are true. For instance, the set of natural numbers with the usual zero, successor, addition, multiplication, and ordering is a model of . A model for a set of sentences is also a model for every *theorem* of that set, *i.e.*, every sentence that can be derived in finitely many steps from those of the given set by applying the standard rules of logic.

For sets of first-order sentences, the following four results are standard:

**Compactness theorem.** (Tarski and Mal’tsev) Given a set of first-order sentences, if every finite subset of has a model, then has a model.

**Upwards Löwenheim-Skolem theorem.** If a set of first-order sentences has a model of infinite cardinality , then it also has models of every cardinality .

**Downwards Löwenheim-Skolem theorem.** If a set of first-order sentences on a finite or countable language has a model, then it also has a finite or countable model.

**Completeness theorem.** (Gödel) Given a set of first-order sentences, if a first-order sentence is true in every model of , then is a theorem of .

All of these facts fail for second-order theories. Let us see how:

We start by considering the following second-order sentence:

**Lemma 1.** The sentence is true in a model if and only if the universe of is at most countable.

The informal reason is that intuitively means:

the universe is a monoid on a single generator

Let us now consider the following second-order sentence:

**Lemma 2.** The sentence is true in a model if and only if the universe of is infinite.

The informal reason is that intuitively means:

the universe contains a copy of the natural numbers

**Theorem 1.** Both Löwenheim-Skolem theorems fail for sets of second-order sentences.

*Proof.* only has countably infinite models. only has uncountably infinite models.

Let us now consider the set of all the sentences of together with the following second-order sentence:

Clearly, is the induction principle: which is an axiom in second-order Peano arithmetics, but only an *axiom scheme* in first-order PA.

**Lemma 3.** Every model of is isomorphic to the set of natural numbers with zero, successor, addition, multiplication, and ordering.

The informal reason is that , though finite, is powerful enough to tell numbers from each other: therefore, in every model of , each numeral (th iteration of the successor, starting from ) can be denoted by at most one item in the universe of the model. On the other hand, is powerful enough to reconstruct every numeral.

**Theorem 2.** The compactness theorem fails for sets of second-order sentences.

*Proof.* Let be a constant outside the language of . Consider the set made of all the sentences from and all the sentences of the form . Then every finite subset of has a model, which can be obtained from the set of natural numbers by interpreting as some number strictly greater than all of the values such that . However, a model of is also a model of , and must be isomorphic to the set of natural numbers: but no interpretation of the constant is possible within such model.

We can now prove

**Theorem 3.** The completeness theorem does not hold for second-order sentences.

In other words, *second-order logic is semantically inadequate*: it is not true anymore that all “inequivocably true” sentences are theorems. The proof will be based on the following two facts:

**Fact 1.** (Gödel) The set of the first-order formulas which are true in *every* model of is recursively enumerable.

**Fact 2.** (Tarski) The set of first-order formulas which are true in *is not* recursively enumerable.

Fact 1 is actually a consequence of the completeness theorem: the set of first-order formulas which are true in every model of is the same as the set of first-order sentences that are provable from , and that set is recursively enumerable by producing every possible proof! To prove Theorem 3 it will thus be sufficient to prove that Fact 1 does not hold for second-order sentences.

*Proof of Theorem 3.* We identify with the conjunction of all its formulas, which are finitely many.

Let be a first-order sentence in the language of . Because of what we saw while discussing the compactness theorem, is true in if and only if it is true in every model of : this, in turn, is the same as saying that is true in every model of . Indeed, let be a model of : if is isomorphic to , then is true in if and only if is true in ; if is not isomorphic to , then is false in , which makes true in . This holds whatever is.

Fix a Gödel numbering for sentences. There exists a recursive function that, for every sentence , transforms the Gödel number of the first-order sentence into the Gödel number of the second-order sentence .

Suppose now, for the sake of contradiction, that the set of second-order sentences that are true in every model of is recursively enumerable. Then we could get a recursive enumeration of the set of first-order sentences which are true in the standard model of by taking the Gödel number of such a sentence , turning it into that of via the aforementioned recursive function, and feeding the latter number to the semialgorithm for second-order sentences that are true in every model of . But because of Tarski’s result, no such recursive enumeration exists.

Bibliography:

- George S. Boolos et al. Computability and Logic. Fifth Edition. Cambridge University Press, 2007

I’m always missing something when I read this argument. Completeness is lost. But so what?

If you care about doing maths in the logic, or at least about arithmetics, it seems completeness of first-order logic doesn’t really give any guarantees anyway. Logicians know this better than me, and most still prefer first-order logic — with few arguing at the side for second-order logic. Why?

In particular, it seems in fact that all proofs in first-order logic are also valid in second-order logic, and more facts become true (for instance for arithmetics) and might be provable.

First-order logic is better because first-order arithmetic does not describe naturals correctly? In either logic, there are properties of naturals one can’t prove — depending on the logic, either because the logic is incomplete (second-order), or because the property of interest only holds for true naturals and fails for other non-standard models (first-order). IIRC, according to Peter Smith’s book, that’s the case for Gödel’s sentence.

It’d be bad if first-order proofs became invalid second-order proofs, but that seems impossible

(and this abstract suggests it is impossible: http://consequently.org/writing/ptm-second-order/). Warning: I refer to proofs *in* the logic, not to proofs about the logic, so the post is not a counterexample.

Finally, second-order logic is boring for model theorists, because Löwenheim-Skolem theorems fail. But that could be provocatively phrased as follows: second-order logic doesn’t have certain bugs that you can build an entire branch of mathematics on. (Almost: there might be model theory not depending on Löwenheim-Skolem’s theorems, not sure).

Let me try to subscribe to this post with a dummy comment… there seem to be issues.