Metatheory of Second-order Logic

Every element of a second order arithmetic model is named by a numeral

If $\Sat{M}{\Th{PA^2}}$source then $\Domain{M} = \Setabs{\Value{\num{n}}{M}}{n \in \Nat}$source.

Proof

Let $N = \Setabs{\Value{\num{n}}{M}}{n \in \Nat}$source, and suppose $\Sat{M}{\Th{PA^2}}$source. Of course, for any $n \in \Nat$source, $\Value{\num{n}}{M} \in \Domain{M}$source, so $N \subseteq \Domain{M}$source.

Now for inclusion in the other direction. Consider a variable assignment $s$source with $s(X) = N$source. By assumption,

Consider the antecedent of this conditional. $\Value{\Obj{0}}{M} \in N$source, and so $\Sat{M}{X(\Obj{0})}[s]$source. The second conjunct, $\lforall[x][(X(x) \lif X(x'))]$source is also satisfied. For suppose $x \in N$source. By definition of $N$source, $x = \Value{\num{n}}{M}$source for some $n$source. That gives $\Assign{\prime}{M}(x) = \Value{\num{n+1}}{M} \in N$source. So, $\Assign{\prime}{M}(x) \in N$source.

We have that $\Sat{M}{X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]}[s]$source. Consequently, $\Sat{M}{\lforall[x][X(x)]}[s]$source. But that means that for every $x \in \Domain{M}$source we have $x \in s(X) = N$source. So, $\Domain{M} \subseteq N$source.

Categoricity of second order Peano arithmetic

Any two models of $\Th{PA^2}$source are isomorphic.

Proof

By the theorem that second order arithmetic models contain only numeral values, the domain of any model of $\Th{PA^2}$source is exhausted by $\Value{\num{n}}{M}$source. Any such model is also a model of $\Th{Q}$source. By the proposition about standard models of Q, any such model is standard, i.e., isomorphic to $\Struct{N}$source.

Definability of arithmetic from successor and second order induction

Let $\Th{PA^{2\dagger}}$source be the second-order theory containing the first two arithmetical axioms (the successor axioms) and the second-order induction axiom. Then $\le$source, $+$source, and $\times$source are definable in $\Th{PA^{2\dagger}}$source.

Proof

To show that $\le$source is definable, we have to find a formula $!A_\le(x, y)$source such that $\Sat{N}{!A_\le(\num n, \num m)}$source iff $n \le m$source. Consider the formula

Clearly, $!B(\num n, Y)$source is satisfied by a set $Y \subseteq \Nat$source iff $\Setabs{m}{n \le m} \subseteq Y$source, so we can take $!A_\le(x, y) \ident \lforall[Y][(!B(x, Y) \lif Y(y))]$source.

To see that addition is definable observe that $k+l=m$source iff there is a function $u$source such that $u(0)=k$source, $u(n')=u(n)'$source for all $n$source, and $m = u(l)$source. We can use this equivalence to define addition in $\Th{PA^{2\dagger}}$source by the following formula:

It should be clear that $\Sat{N}{!A_+(\num k, \num l, \num m)}$source iff $k+l=m$source.

Exercise completing the definability proof

Complete the proof of the proposition defining arithmetic from successor and second order induction.

Undecidability of second order logic

Second-order logic is undecidable.

Proof

A first-order sentence is valid in first-order logic iff it is valid in second-order logic, and first-order logic is undecidable.

No sound and complete effective second order proof system

There is no sound and complete derivation system for second-order logic.

Proof

Let $!A$source be a sentence in the language of arithmetic. $\Sat{N}{!A}$source iff $\Th{PA^2} \Entails !A$source. Let $!P$source be the conjunction of the nine axioms of $\Th{PA^2}$source. $\Th{PA^2} \Entails !A$source iff $\Entails !P \lif !A$source, i.e., $\Sat{M}{!P \lif !A}$source. Now consider the sentence $\lforall[z][\lforall[u][\lforall[u'][\lforall[u''][\lforall[L][(!P' \lif !A')]]]]]$source resulting by replacing $\Obj{0}$source by $z$source, $\prime$source by the one-place function variable $u$source, $+$source and $\times$source by the two-place function-variables $u'$source and $u''$source, respectively, and $<$source by the two-place relation variable $L$source and universally quantifying. It is a valid sentence of pure second-order logic iff the original sentence was valid iff $\Th{PA^2} \Entails !A$source iff $\Sat{N}{!A}$source. Thus if there were a sound and complete proof system for second-order logic, we could use it to define a computable enumeration $f\colon \Nat \to \Sent[L_A]$source of the sentences true in $\Struct{N}$source. This function would be representable in $\Th{Q}$source by some first-order formula $!B_f(x, y)$source. Then the formula $\lexists[x][!B_f(x, y)]$source would define the set of true first-order sentences of $\Struct{N}$source, contradicting Tarski's Theorem.

Explain

Call a set of sentences $\Gamma$source finitely satisfiable if every one of its finite subsets is satisfiable. First-order logic has the property that if a set of sentences $\Gamma$source is finitely satisfiable, it is satisfiable. This property is called compactness. It has an equivalent version involving entailment: if $\Gamma \Entails !A$source, then already $\Gamma_0 \Entails !A$source for some finite subset $\Gamma_0 \subseteq \Gamma$source. In this version it is an immediate corollary of the completeness theorem: for if $\Gamma \Entails !A$source, by completeness $\Gamma \Proves !A$source. But a derivation can only make use of finitely many sentences of $\Gamma$source.

Compactness is not true for second-order logic. There are sets of second-order sentences that are finitely satisfiable but not satisfiable, and that entail some $!A$source without a finite subset entailing $!A$source.

Failure of compactness for second order logic

Second-order logic is not compact.

Proof

Recall that

is satisfied in a structure iff its domain is infinite. Let $!A^{\ge n}$source be a sentence that asserts that the domain has at least $n$source elements, e.g.,

Consider the set of sentences

It is finitely satisfiable, since for any finite subset $\Gamma_0 \subseteq \Gamma$source there is some $k$source so that $!A^{\ge k} \in \Gamma$source but no $!A^{\ge n} \in \Gamma$source for $n>k$source. If $\Domain{M}$source has $k$source elements, $\Sat{M}{\Gamma_0}$source. But, $\Gamma$source is not satisfiable: if $\Sat{M}{\lnot \fn{Inf}}$source, $\Domain{M}$source must be finite, say, of size $k$source. Then $\Sat/{M}{!A^{\ge k+1}}$source.

Exercise on noncompact entailment

Give an example of a set $\Gamma$source and a sentence $!A$source so that $\Gamma \Entails !A$source but for every finite subset $\Gamma_0 \subseteq \Gamma$source, $\Gamma_0 \Entails/ !A$source.

Explain

The (Downward) Löwenheim--Skolem Theorem states that every set of sentences with an infinite model has an enumerable model. It, too, is a consequence of the completeness theorem: the proof of completeness generates a model for any consistent set of sentences, and that model is enumerable. There is also an Upward Löwenheim--Skolem Theorem, which guarantees that if a set of sentences has a denumerable model it also has a non-enumerable model. Both theorems fail in second-order logic.

Failure of downward Loewenheim Skolem in second order logic

The Löwenheim--Skolem Theorem fails for second-order logic: There are sentences with infinite models but no enumerable models.

Proof

Recall that

is true in a structure $\Struct{M}$source iff $\Domain{M}$source is enumerable, so $\lnot\fn{Count}$source is true in $\Struct{M}$source iff $\Domain{M}$source is non-enumerable. There are such structures---take any non-enumerable set as the domain, e.g., $\Pow{\Nat}$source or $\Real$source. So $\lnot \fn{Count}$source has infinite models but no enumerable models.

Failure of upward Loewenheim Skolem in second order logic

There are sentences with denumerable but no non-enumerable models.

Proof

$\fn{Count} \land \fn{Inf}$source is true in $\Nat$source but not in any structure $\Struct{M}$source with $\Domain{M}$source non-enumerable.