Completeness theorem and compactness theorem do not hold in full second and higher-order logic. What makes them incompatible with the theorems? Is it somehow related to Russell's paradox or diagonalization issues?


  • 2
    $\begingroup$ My intuition on the matter (which may be wrong) is that we put an extra condition on semantics: that we insist that the class "all first-order predicates" must be interpreted as the set-theoretic power set of the domain, and that is the source of most/all of our problems. $\endgroup$
    – user14972
    May 7, 2012 at 1:10

2 Answers 2


For the Compactness Theorem:

Take second-order Peano arithmetic, that is, the original Peano arithmetic, with full second-order version of induction. The language of Peano arithmetic in particular has a constant symbol $0$, and a unary function symbol $S$ for the successor function. It is not hard to show that second-order Peano arithmetic is categorical: any two models are isomorphic.

Add to the language a new constant symbol $B$. Add to second-order Peano arithmetic the infinitely many special axioms $\lnot(B=0)$, $\lnot(B=S(0))$, $\lnot(B=S(S(0)))$, $\lnot(B=S(S(S(0))))$, and so on forever.

Any finite subset $T_{\text{fin}}$ of this theory has a model. Just interpret $B$ as a natural number larger than any of the natural numbers "mentioned" in the finitely many special axioms that occur in $T_{\text{fin}}$. But the full theory does not have a model, since such a model cannot be isomorphic to the natural numbers. Thus the Compactness Theorem is violated.


The reason is that (the set of valid formulas) of these systems are not c.e. and therefore do not have effective proof systems, i.e. there is no c.e. set of axioms that would formalize them.

Here I am using the word proof system in the usual sense, i.e. a decidable set of axioms and rules and a proof is finite structure built from them. In addition given a string and a formula we can decide if the string is a proof of the formula. If we modify the requirements we can have a proof system and a completeness theorem. For example, we can add the $\omega$-rule and then anything in second order arithmetic is derivable. We can combine these ideas with computability and consider only those proof objects which have finite representations, e.g. a Turing machine gives their bits. There is considerable amount of literature in proof theory on these topics.

  • $\begingroup$ What does c.e. mean? Is the point that the second order quantifier range over an un-enumarable domain? $\endgroup$
    – Nikolaj-K
    Jun 23, 2013 at 22:57
  • $\begingroup$ @Nick, c.e. stands for computably enumerable is the modern terminology replacing r.e. and the part after i.e. in the first paragraph explains what I meant. $\endgroup$
    – Kaveh
    Jun 23, 2013 at 23:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.