# Is there a result for second-order theories analogous to Gödel's second incompleteness theorem?

One formulation of Gödel's second theorem says that, if $T$ is a consistent, axiomatisable extension of $PA$, and then $T$ cannot prove $\neg Prv(\ulcorner 0=1 \urcorner)$, where $Prv(-)$ is a predicate in the language of $T$ satisfying the Hilbert-Bernays derivability conditions. By my understanding, what this means is that if a first-order theory is capable of encoding its own syntax, and if it has a predicate satisfying the Hilbert-Bernays derivability conditions, then it can encode a statement that it is provably consistent, but that statement is undecidable.

I have two questions.

1) Is my understanding of the theorem correct? In particular, I want to know whether I am making a mistake by dropping reference to extensions of $PA$.

2) Is there an analogous result for second-order theories? Something like, "for $T$ in such-and-such class of consistent second-order theories, $T$ cannot prove $\neg Prv(\ulcorner \neg Con(T) \urcorner)$."

In Gödel's original paper (1931), see : Jean van Heijenoort (editor), From Frege to Gödel : A Source Book in Mathematical Logic (1967), page 592-on, the results was proved for the following system :

If to the Peano axioms we add the logic of Principia Mathematica (with the natural numbers as the individuals) together with the axiom of choice (for all types), we obtain a formal system $S$, for which the following theorems hold [...].

And see page 600 for the induction axiom (and not axiom schema).

Thus, Gödel's reuslts apply to second-order theories.

But you have to take into account that second-order logic itself is "incomplete" in the sense of Gödel's Completeness Theorem.

• Yep, provability in 2nd order logic (with 'full semantics)' is a somewhat unsatisfying notion. Unlike 1st order logic, there's no completeness theorem. (But, 2nd order logic is complete with respect to the less stringent 'Henkin semantics'.) Commented Dec 18, 2015 at 12:24
• Great, thanks. I was aware of the differences between first- and second-order logic, but was not sure how that affected Godel's result. Commented Dec 18, 2015 at 12:25
• @BrianO - yes, sure; but this is a topic that I'm not able "to manage" ... As Quine said : "2nd order logic (the "full" one) is set theory in disguise" ; in the same way, we can say that 2nd order logic with 'Henkin semantics' is " is nothing but FOL (many-sorted) together with the comprehension axioms", i.e. a sort of FOL "in disguise". So, what is "really" 2nd order logic ? Commented Dec 18, 2015 at 12:30
• I agree, I wasn't going to stray into that topic, but yes 2OL with Henkin semantics is a 2-sorted FOL (in many ways? in all ways that matter?). Just what 2OL is, is clear with finite structures (complexity theory for example), but gets murky at the simplest infinity. We can't even say how big the 2OL "standard model" of arithmetic is, as that depends on CH. Commented Dec 18, 2015 at 12:37