Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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). – Nikos M. May 3 '15 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 – Nikos M. May 3 '15 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) – Nikos M. May 3 '15 at 17:51
up vote 20 down vote accepted

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.

share|cite|improve this answer
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. – Asaf Karagila Jul 21 '13 at 7:02
Yes indeed: @AsafKaragila's observation is exactly right. – Peter Smith Jul 21 '13 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" ;-) – Asaf Karagila Jul 21 '13 at 7:43
Do "people sometimes say that infinities are the troublemakers" with respect to Gödelian incompleteness? Really? Which infinities?? – Peter Smith Mar 25 '15 at 19:48
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. – Peter Smith Sep 2 '15 at 20:42

To answer the question based on the comments already posted:

Are the Godel's incompleteness theorems valid for both classical and intuitionistic logic?

In a sense YES.


  1. Goedel's incompleteness theorem(s) apply first to classical logic

  2. Goedel's incompleteness theorem and its proof is constructive but not intuitionisticaly constructive (Goedel's paper)


Goedel himself stated in his paper that the above procedure is "constructively non-objectionable", however

a) Goedel's reference to contructivism (intuitionism), is rather formal than actual (more detailed below)

b) variations of LEM (law of excluded middle) are used throughout Godel's proof

c) combined with the use of a diagonalisation procedure

(see also Gödel’s Proof and Intuitionism for another analysis)

Does this apply the same to intuitionistic logic?

In a sense YES.


  1. Goedel's negative translation of classical logic into intuitionistic logic is only formal (Goedel's paper)


a) negative translation of classical logic to intuitionistic logic is not intuitionism, rather a formal analogy, because the semantics of what constitutes a construction, a proof, implication and of course the definition/construction of new entities based only on previously constructed entities is totally different, being classical than intuitionistic (and same holds for the original incompleteness proof, where these conditions are neither formalised nor met) (see also Kolmogorov's Interpretation of Intuitionistic Logic as Problems)

b) intuitionism has, in a sense, already embedded the incompletenmess theorems as it accepts statetements which can neither be proved nor refuted (at a certain given time)

c) Brouwer himself foresaw Goedel's results by a decade at least (note: Goedel himself had attended Brouwer's lectures on the foundations of mathematics)

Quoting from Artemov's Understanding Constructive Sematics (Spinoza Lecture)

enter image description here

And also from here

Intuitionistic vs. Classical Perspective

Intuitionists normally base their formal systems on intuition of constructive, e.g., BHK-style informal semantics, rather then on classical foundations...

Classical mathematicians (such as Gödel, Kolmogorov, Kleene, Novikov, and others) seek a rigorous

classical definition of the constructive semantics.

And from A. Heyting, Intuitionism An Introduction

enter image description here

In the light of the above Goedel's incompleteness results do indeed hold for intuitionistic logic in a formal way (with classical semantics) but not for intuitionism (which in any case does not need any incompleteness result as they are already embedded in the practice and semantics)

share|cite|improve this answer
I'm not sure I buy this answer. The incompleteness theorems have nothing to do with semantics, as far as I know. For example, the (classical) first incompleteness theorem tells us that if $T$ is a consistent, computably-enumerable extension of Robinson arithmetic, then there is a sentence in the language of first-order arithmetic that $T$ cannot prove and cannot refute. Notice there's no mention of semantics. So, there's no real scope for subtle philosophical issues to creep in, as far as I can see. – goblin Sep 2 '15 at 22:45
@goblin, edited answer to add reference from Heyting Intuitionism. The semantics enter in multiple ways. For example, the meaning of implication and proof, these are left as classical in Goedel's proofs and in no relation (than a formal analogy) with intuitionism. – Nikos M. Sep 2 '15 at 23:49
@goblin, to give a further analysis, the semantics of implication and proof (classical), is what actually enables the construction of Goedel's proof, thorugh diagonalisation, while this is not possible with intuitionistic semantics (requiring priorities of newly defined entities, implication and so on), which them makes arbitrary diagonalisation problematic (to say th least). Again Goedel's proof is based on classical semantics of proof and implication. Also i dont recal saying i sell something for others to buy, reasoning is explained and references are used – Nikos M. Sep 2 '15 at 23:59
That's just a figure of speech; it means I'm not convinced by your argument. Anyway, I still don't see your point. As far as I know, Heyting arithmetic can prove the incompleteness theorem for Heyting arithmetic. So once again, I don't think messy semantical issues really come into play here. (I didn't downvote, by the way.) – goblin Sep 3 '15 at 1:03
@goblin, correct and is in fact stated as such! The subtle (or not so subtle) difference is what this represents. It represents a classical theory with just different syntactic rules (which correspond to intuitionistic rules but without the actual semantics). So in this sense it does not talk about intuitionism but for a classical theory. Hope it is more clear. Btw thanx for clarifying the downvoting issue, anyway the post is there and speaks for itself – Nikos M. Sep 3 '15 at 2:26

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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