How does Gödel Completeness fail in second-order logic?

Question

So a while ago I saw a proof of the Completeness Theorem, and the hard part of it (all logically valid formulae have a proof) went thusly:

Take a theory $K$ as your base theory. Suppose $\varphi$ is logically valid but not a theorem. Then you can add $\neg\varphi$ to $K$'s axioms, forming a new theory $K'$ which is consistent, and therefore $K'$ has a model $M$. Since $\neg\varphi$ is an axiom of $K'$, $M\models\neg\varphi$, but since $\varphi$ is logically valid in $K$ and $M$ is also a model of $K$, $M\models\varphi$, contradiction. Therefore, $\varphi$ must be a theorem of $K$.

Which makes sense to me, but I don't see how the above fails in second-order logic? This theorem looks perfectly generalisable to second-order logic, I don't see any steps that couldn't be done there.

Is the theorem correct? If not, why? If so, which part fails in second-order logic?

--EDIT:

As was commented, I got three isomorphic answers, and I can't set all of them as the true answer so I set the one that was phrased in the clearest way to me. In any case, thank you all!

Answer 1

The property that "every consistent theory has a model" does not hold for second-order logic.

Consider, for example the second-order Peano axioms, which are well known to have only $\mathbb N$ as their model (in standard semantics). Extend the language of the theory with a new constant $c$, and add new axioms $$ c\ne 0 \\ c\ne S0 \\ c\ne SS0 \\ \cdots $$

The extended theory is still consistent -- that is, it cannot prove a contradiction -- because a proof must be finite and can only mention finitely many of the new axioms, and there is a model as long as we only take finitely many of these axioms.

But the extended theory does not have a model, because the model will have to be exactly $\mathbb N$ in order to satisfy the original Peano axioms, but must have a $c$ that is not a numeral in order to satisfy all the new axioms.

Answer 2

Take the language of arithmetic, augmented by a single constant symbol $c$. Now add to the Peano [second-order] axioms the following schema, $0<c$, $s(0)<c$ and so on.

If this theory is consistent, then it should have a model. But second-order Peano has only one model. So it has to be that model. But how will you interpret $c$ there? You can't.

So the theory is inconsistent. So a contradiction should be provable from finitely many axioms. But given any finitely many axioms, you can find some large enough natural number such that interpreting $c$ with that value is okay. So any finitely many axioms from this theory do not prove a contradiction.

So you have a theory without a model, but without inconsistencies. So completeness (and compactness) fail.

Answer 3

First of all, even in the first-order case that "proof" doesn't work: how do you get $M$? You need the assumption that, if $K'$ is consistent, then it has a model; but this is exactly what you are trying to prove.

Second of all, in order to even ask if the completeness theorem holds for second-order logic, we need to define what a "proof" is in second-order logic.

As a matter of fact we can show that there is no reasonable notion of proof for second-order logic, at all! This is because second-order logic is not compact: there is a set of sentences $K$, and a sentence $\varphi$, such that (i) $\varphi$ is a logical consequence of $K$, but (ii) $\varphi$ is not a logical consequence of any finite subset of $K$. (Exercise. HINT: find a $\varphi$ which characterizes $(\mathbb{N}; +, \times)$ up to isomorphism.) This means that any kind of proof system for second-order logic, in order to be complete, would have to allow infinitely long proofs in a certain sense.

Answer 4

The compactness theorem required for the proof of "every consistent theory has a model" is not valid in second order logic. That where the problem is.