I'm trying to see/show that second order logic (with full semantics) is incomplete - i.e. that there are sentences that are true in all models of some theory $T$, and yet still can not be proved from $T$.

First of all, is this even the case? And if it is, is this how it can be shown :

The basic idea is that if second order logic were complete, we should then be able to prove any sentence of arithmetic, which Gödel's theorem says we can not. It seems that Gödel's incompleteness theorem should apply also to second order logic (does it?), and so SOL completeness ($N\vDash \phi$ iff $N\vdash \phi$) would mean that any $\phi$ true in the standard model of number theory (i.e. $N\vDash \phi$ ) is also provable from N, contradicting the incompleteness theorem for SOL.

  • $\begingroup$ What does proved from $T$ mean? $\endgroup$ Jun 12, 2015 at 23:16
  • $\begingroup$ The usual meaning : T ⊢ ϕ. Some proof system in second order logic. That is, there exists some proof system "⊢" in second order logic, such that ϕ can be proved using it. The proof system is allowed to be, let's say, any (decidable) set of logical axioms, that are valid in T. $\endgroup$
    – Cg905
    Jun 13, 2015 at 0:13
  • 3
    $\begingroup$ The problem is that there is really no proof system for second-order logic. $\endgroup$ Jun 13, 2015 at 0:16
  • $\begingroup$ @André Nicolas, could you explain what you mean by saying that there is really no proof system for second order logic? I thought that there were proof systems for second order logic which are sound (though not complete). Am I wrong? $\endgroup$
    – user65526
    Oct 14, 2023 at 8:17

1 Answer 1


The problem is that just saying "any proof system" doesn't give you enough to work with. There is certainly some complete proof systems -- for example the one where every logically valid second-order formula is declared to be an axiom. On the other hand that proof system is not effective, which makes it not very exciting.

However, you're right that you can use Gödel's incompleteness theorem to show that there is no proof system that is all of {sound, complete, effective}. We can even take $T$ to be the empty theory.

The key to this is that the Peano axioms can be expressed as a finite conjunction of formulae in pure second-order logic, so having a sound proof system for second-order logic will allow us to prove formulas $\varphi$ about integer arithmetic by asking whether $$ \forall 0\,\forall S\,\forall {+}\,\forall{\times}\,\Bigl[\text{Peano}(0,S,{+},{\times}) \to \varphi \Bigr] $$ is provable in the empty theory. (This is standardly true in all universes if and only if $\varphi$ is true in the integers).

Either there are easy arithmetic truths that the proof system fails to prove in this way (in which case it is clearly incomplete), or it proves enough that Gödel's theorem applies to it.

  • $\begingroup$ The problem is with meaning of "second order", without reference to semantics it is unclear what second order theory is. If you have a multi-sorder language but with a computable notion of proof, that system is complete w.r.t the Henkin semantics. And us such is a first-order system with many sorts. It contains enough arithmetic to repeat Godel-Rosser proof of incompleteness. If you think about the real second order arithmetic, i.e. w.r.t. the full models, there cannot be effective proof procedure. So talking about incompleteness is, in a way, meaningless. $\endgroup$ Feb 20, 2021 at 16:54

You must log in to answer this question.

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