# Are the Gödel's incompleteness theorems valid for both classical and intuitionistic logic?

I am studying an undergraduate text about math logic. The proofs of the two Gödel's incompleteness theorems are not completely formal: they are admittedly simpler that the real proofs. For what I understood, I deduce the two theorems are valid for both classical and intuitionistic logic.

Is my deduction correct?

• as i mentioned in similar question in phil.SE, this is correct only for IL formalised as an alternative classical logic (with modification of syntax rules) and then terated as a formal suntax system. But this is not intuitionism, the difference lies in semamtics (although this is overlooked in formal approaches to logic). May 3, 2015 at 17:19
• In fact Brewer foresaw the incompletenes theorems of Goedels when accepted propositions which can neither be proved nor refuted in intiotionism (up to current knowledge), in tjis sense incompleteness theorems are already embeded in intuitionism from the start. One has to be aware of a classical /syntactic treatment of a logic (e.g intuitionistic) and the actual philosophy like intuitionism which has tio do with semantics May 3, 2015 at 17:19
• a nice post "Gödel’s Proof and Intuitionism" in the same direction and meaning as my previous comments (similar question on phil.SE) May 3, 2015 at 17:51
• The comment by Nikos is utter nonsense. I've just looked at the webpage he linked to and it is pure rubbish. I'm speaking as a logician, but nobody should simply take my word for it; just go ahead and study logic and it will be clear that what I say is true. Sep 12, 2016 at 6:42

The usual proof of Gödel's First Incompleteness Theorem is entirely constructive. We don't have to rely on excluded middle, or have to rely on proving an existential quantification for which we can't produce a witness. For recall: the proof consists in (a) giving a recipe which takes a suitable specification of a sufficiently strong theory $T$ and constructs a certain sentence $G_T$ and then (b) showing $G_T$ is undecidable in that theory. The construction of $G_T$ is clever though simple when you see how, and involves no infinitary ideas. The proof of undecidability involves a pair of reductios, but both of the non-contentious type [like "Suppose $T \vdash G_T$: then contradiction; so $T \nvdash G_T$"]. So overall the proof is intuitionistically acceptable.

The usual proof of the Second Incompleteness Theorem then consists, at heart, in showing that the proof of the First Theorem can be coded up in arithmetic. Again it's all constructive, and so is intuitionistically acceptable.

• Historically this is the strength of the incompleteness theorems. They are foundationally indisputable in this sense. They don't appeal to set theory, nor to LEM. Just the natural numbers. Jul 21, 2013 at 7:02
• Yes indeed: @AsafKaragila's observation is exactly right. Jul 21, 2013 at 7:37
• I know, I made a footnote to your answer which is really a footnote, rather than a full answer with the classical P. Smith preface "This answer is really just a footnote to ...'s answer" ;-) Jul 21, 2013 at 7:43
• By the way, the first incompleteness proof has been formally proved in Coq, an implementation of the calculus of (co)inductive constructions. This dependent type theory has intensional equality and is constructive, so the proof can (by normal standards) be indeed regarded as constructive. Sep 2, 2015 at 20:42
• "existential quantification for which we can't produce a witness." How well expressed! Sep 2, 2015 at 22:03