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?


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!

  • 3
    $\begingroup$ You got three isomorphic answers in the span of a minute (and four seconds, to be exact). :-) $\endgroup$
    – Asaf Karagila
    Sep 22, 2015 at 19:41
  • 2
    $\begingroup$ The key difference in second-order logic is that you have to distinguish more carefully between syntactically consistent theories and semantically consistent theories. $\endgroup$ Sep 22, 2015 at 20:34
  • 1
    $\begingroup$ This question has the interesting property of also being the answer to my deleted question from six months ago. I had proven independently that Gödel must fall when I constructed a theorem (which I was told was second order logic) that showed the halting problem is not universal and in fact has a hidden assumption in its popular statement. $\endgroup$
    – Joshua
    Sep 23, 2015 at 1:24

4 Answers 4


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.

  • $\begingroup$ What if $c$ is a nonstandard number? $\endgroup$ Jul 26, 2016 at 12:41
  • 1
    $\begingroup$ @PyRulez: The second-order Peano axioms have no model with nonstandard numbers, because the set of standard numbers would fail the second-order induction axiom unless it is the entire universe. $\endgroup$ Jul 26, 2016 at 13:02
  • $\begingroup$ oh, okay. Does that mean you need set theory to do second order logic? $\endgroup$ Jul 26, 2016 at 13:04
  • $\begingroup$ @PyRulez: You need set theory in order to speak about models (first or second order) at all. Without it, you cannot even state the completeness theorem. $\endgroup$ Jul 26, 2016 at 13:06
  • 1
    $\begingroup$ This answer makes an unspoken assumption that only full models are being considered. Henkin's proof of the completeness theorem applies perfectly well to second-order logic and produces a "Henkin model" for the theory in this answer. This model is not "full" - its sets do not range over all the subsets of the individuals. But it is still a model of all the axioms including second-order induction. To conclude "there is no model" requires limiting the set of "models" to full models. We could equally well make first-order logic incomplete by restricting to finite or to computable models. $\endgroup$ Mar 25, 2018 at 22:22

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.

  • 1
    $\begingroup$ Well, the OP's "proof" works just fine in the first-order case if you state the completeness theorem as "every logically valid sentence relative to $T$ has a proof from $T$" and first prove as a lemma "every consistent theory has a model" (which is a priori weaker, since it's the contrapositive of the special case that the sentence is $\bot$). :0) $\endgroup$ Sep 22, 2015 at 20:10
  • $\begingroup$ The usual practice is to define a proof in second-order logic to be basically the same thing as a proof in first-order logic. Sometimes, some set existence and/or choice schemes are added. The resulting proof system is indeed incomplete, but it is a reasonable notion of proof, unless we want to conflate "reasonable" with "complete". $\endgroup$ Sep 22, 2015 at 20:36
  • $\begingroup$ Maybe "complete" is implicit in Noah Schweber's phrase "reasonable notion of proof". (The existence of sound proof systems is trivial.) But, it seems that a complete notion of proof for second-order logic would have to be much more unreasonable that just plain "infinite": since second-order validity is not $\Sigma_1$ in set theory, not even "set-sized" proofs would do. $\endgroup$
    – mmw
    Sep 22, 2015 at 23:34

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.

  • 1
    $\begingroup$ As a side comment, we could also use the single Goedel sentence for the second-order PA axioms, which is syntactically consistent with PA2 but not semantically consistent with PA2. So there is not any strict need to use an infinite axiom scheme. The scheme is usually easier to understand, since it does not involve incompleteness, just order. $\endgroup$ Sep 22, 2015 at 20:38

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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .