Second-order theories should not be taken lightly

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 ( $\wedge$ for conjunction, $\vee$ for disjunction, $\sim$ 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 $\mathbf{Q}$ is made of the following first-order sentences on the language $\{ \mathbf{0}, {}', +, \cdot, < \}$ :

$\forall x . \sim (x' = \mathbf{0})$
$\forall x y . x' = y' \to x = y$
$\forall x . x + \mathbf{0} = x$
$\forall x y . x + y' = (x + y) '$
$\forall x . x \cdot \mathbf{0} = 0$
$\forall x y . x \cdot y' = x \cdot y + x$
$\forall x . \sim (x < \mathbf{0})$
$\forall x y. x < y' \iff (x < y \vee x = y)$
$\forall x . \mathbf{0} < x \iff \sim (x = \mathbf{0})$
$\forall x y . x' < y \iff (x < y \wedge y \neq x')$

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 $\mathbb{N}$ of natural numbers with the usual zero, successor, addition, multiplication, and ordering is a model of $\mathbf{Q}$ . 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 $\Gamma$ of first-order sentences, if every finite subset of $\Gamma$ has a model, then $\Gamma$ has a model.

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

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 $\Gamma$ of first-order sentences, if a first-order sentence $A$ is true in every model of $\Gamma$ , then $A$ is a theorem of $\Gamma$ .

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

We start by considering the following second-order sentence:

$\mathbf{Denum} \equiv \exists x \exists f \forall S . ( S(x) \wedge \forall y . (S(y) \to S(f(y))) ) \to \forall y . S(y)$

Lemma 1. The sentence $\mathbf{Denum}$ is true in a model $\mathcal{M}$ if and only if the universe of $\mathcal{M}$ is at most countable.

The informal reason is that $\mathbf{Denum}$ intuitively means:

the universe is a monoid on a single generator

Let us now consider the following second-order sentence:

$\mathbf{Infin} \equiv \exists x \exists f . (\forall y . x \neq f(y)) \wedge (\forall y z . f(y) = f(z) \to y = z)$

Lemma 2. The sentence $\mathbf{Infin}$ is true in a model $\mathcal{M}$ if and only if the universe of $\mathcal{M}$ is infinite.

The informal reason is that $\mathbf{Infin}$ 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. $\mathbf{Infin} \wedge \mathbf{Denum}$ only has countably infinite models. $\mathbf{Infin} \wedge \sim \mathbf{Denum}$ only has uncountably infinite models. $\Box$

Let us now consider the set $\mathbf{PA2}$ of all the sentences of $\mathbf{Q}$ together with the following second-order sentence:

$\mathbf{Ind} \equiv \forall S . (S(\mathbf{0}) \wedge \forall x. (S(x) \to S(x'))) \to \forall x . S(x)$

Clearly, $\mathbf{Ind}$ 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 $\mathbf{PA2}$ is isomorphic to the set of natural numbers with zero, successor, addition, multiplication, and ordering.

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

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

Proof. Let $c$ be a constant outside the language of $\mathbf{PA2}$ . Consider the set $\Gamma$ made of all the sentences from $\mathbf{PA2}$ and all the sentences of the form $X_n \equiv c \neq \mathbf{n}$ . Then every finite subset $\Gamma_0$ of $\Gamma$ has a model, which can be obtained from the set of natural numbers by interpreting $c$ as some number $M$ strictly greater than all of the values $n$ such that $X_n \in \Gamma_0$ . However, a model of $\Gamma$ is also a model of $\mathbf{PA2}$ , and must be isomorphic to the set of natural numbers: but no interpretation of the constant $c$ is possible within such model. $\Box$

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 $\mathbf{Q}$ is recursively enumerable.

Fact 2. (Tarski) The set of first-order formulas which are true in $\mathbb{N}$ 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 $\mathbf{Q}$ is the same as the set of first-order sentences that are provable from $\mathbf{Q}$ , 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 $\mathbf{PA2}$ with the conjunction of all its formulas, which are finitely many.

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

Fix a Gödel numbering for sentences. There exists a recursive function that, for every sentence $A$ , transforms the Gödel number of the first-order sentence $A$ into the Gödel number of the second-order sentence $\mathbf{PA2} \to A$ .

Suppose now, for the sake of contradiction, that the set of second-order sentences that are true in every model of $\mathbf{Q}$ 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 $\mathbf{Q}$ by taking the Gödel number of such a sentence $A$ , turning it into that of $\mathbf{PA2} \to A$ via the aforementioned recursive function, and feeding the latter number to the semialgorithm for second-order sentences that are true in every model of $\mathbf{Q}$ . But because of Tarski’s result, no such recursive enumeration exists. $\Box$

Bibliography:

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

2 thoughts on “Second-order theories should not be taken lightly”

blaisorblade on February 18, 2016 at 10:31 am said:

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).

Reply ↓
- blaisorblade on February 18, 2016 at 10:32 am said:
  
  Let me try to subscribe to this post with a dummy comment… there seem to be issues.
  
  Reply ↓

Theory Lunch

Institute of Cybernetics, Tallinn

Second-order theories should not be taken lightly

2 thoughts on “Second-order theories should not be taken lightly”

Leave a Reply Cancel reply

Share this:

Like this:

Related

2 thoughts on “Second-order theories should not be taken lightly”

Leave a Reply Cancel reply