Classically, one sets up an axiomatic system with a formal deduction system & an interpretation in a model. Generally it is sound, that is: a formally deduced theorem is also true when interpreted in the model. The reverse is called completeness, if a sentence in the model is true then it is also formally deducible. This is the statement of Godels completeness Theorem.

Confusingly Gödel Incompleteness Theorem refers to the notion of decidability (this is distinct to the notion of decidability in computation theory aka Turing machines and the like) - a statement being decidable when we are able to determine (decide) that it has either a proof or a disproof. If all statements in the language are decidable we call it complete. The theorem says that axiomatic systems containing PA is incomplete - that is there are always statements which we cannot find a proof or a disproof.

Now, what happens if the formal deduction system is not classical but intuitionistic? Intuitionistic logic is many-valued but rather than modelling truth one models constructability/provability, which instead of using set theory semantics uses Kripke semantics. Now:

  1. Is it still sound? That is: a formally deduced theorem is also constructible?

  2. Is it incomplete? There is a constructible sentence that is not formally deducible?

  3. Does it have undecidable statements?

  • 1
    Far from well read on the topic, but the SEP page on intuitionism has a few mentions of the incompleteness theorem and might be helpful.
    – commando
    Jun 7, 2013 at 18:51
  • as mentioned in answers Goedle;s incompleteness theorems apply to Intuitionistic Logic only when formalised as a kind of classical logic without LEM, but this does not capture Intuitionism as Brewer proposed. In essence IL is not just classical logic without LEM, since semantics are different not just a few changes i(i.modify a couple of rules) in syntax.
    – Nikos M.
    May 3, 2015 at 17:09
  • Moreover constructive manthematics is not just classical mathematics without Axiom of Choice (which implies LEM), but in citations this analogy is made. It embodies a different view related to semantics most importantly. In this sense having propositions which can be undecidable, effectively embeds Goede;s theorems as integral part of Intiotionism from the start
    – Nikos M.
    May 3, 2015 at 17:10
  • 1
    a nice post "Gödel’s Proof and Intuitionism" in the same direction and meaning as my previous comments (similar question on math.SE)
    – Nikos M.
    May 3, 2015 at 17:51

3 Answers 3


The common axiom systems for intuitionistic logic are both sound and complete. It is interpretable as an S4 modal logic or as a weakening of classical logic (essentially you just drop the law of excluded middle and double negation elimination and then tweak the quantifier rules).

Since it is both sound and complete it is not incomplete. The fact that they treat "truth" as something like "provability" does not bear on the situation.

Now, is intuitionistic logic incomplete? No, but neither is classical first order logic and incompleteness tends to come with stronger logical systems than FOL, not weaker ones.

The question I imagine you have in mind (though I apologize for presuming to be able to read your thoughts) is whether intuitionistic/constructive mathematics is susceptible to incompleteness. The answer here is yes. Gödel gave the proofs in a constructively/intuitionistically acceptable manner (i.e., using only inferences they endorse) and so the result would hold for intuitionistic number theory.

It is worth noting that you don't need an arithmetic as strong as PA to fall prey to incompleteness. All that is required is a number theory which is recursively axiomatizable.

Robinson arithmetic (Q) is a theory much weaker than PA (I believe it is PA without induction) but incompleteness still arises. It might be (can't remember exactly) the weakest system still prey to the incompleteness theorems. It was actually designed to be such a weak system--- a system which can represent all and only recursive number-theoretic functions.

Here is an interesting article I found on the topic--- looks like a good read. These lecture notes (again from Kevin Klement) do quite a good job of walking through Gödel's theorems if you want that. Otherwise the SEP entry @commando linked to should be helpful as well.

  • thanks for the references, they look useful. No need to apologise - You read my intentions correctly! I think I was confusing completeness which refers to syntax & semantics, and incompleteness which refers to solely 'formal proof' syntax only through the inference/deductive/proof system if I've read you right. Which is the standard name to use - inference/deductive/proof - they seem to all be used?! Jun 7, 2013 at 19:54
  • 1
    @MoziburUllah I'm afraid that I'm not quite getting what difference you're pointing to. As far as I know, there is just one form of (in)completeness: (not) being able to formally prove every truth of your theory.
    – Dennis
    Jun 7, 2013 at 19:59
  • 2
    You said "it is both sound and complete it is not incomplete" and then "whether it is suceptible to incompleteness. The answer here is yes". I think its those two notions of completeness I had mixed up - simply because they have similar names. Jun 7, 2013 at 20:11
  • 1
    @mcb This isn't actually all that surprising. (Classical) First-order logic is the language most mathematics is formalized in. First-order logic is complete, but very few mathematical theories couched in it will be. So yes, you're right, there are additional axioms you add to a base of intuitionistic logic that cause the incompleteness of constructive maths. In particular, whatever axioms you add that allow you to define an arithmetic at least as strong as Robinson Arithmetic are the axioms that will cause the incompleteness theorem to apply.
    – Dennis
    Jun 8, 2015 at 19:40
  • 1
    @Dennis First-order logic is the language most mathematics is formalized in. I think most mathematics is actually formalized in what can be called "second-order" logic, as you seriously need to quantify over function symbols rather often. May 31, 2016 at 21:49

The two notions (completeness and incompleteness) are not opposites but very much connected (not only by Godel's name in the name of the two theorems).

Do take into account that Godel's Completeness Th of First-Order Logic is :
if a sentence is true in all the models of the axioms (i.e. it is a logical consequence of the axioms) then it is also formally deducible (in FOL) by the axioms.

Godel's Incompleteness Th is relative to formal systems containing "a certain amount" of arithmetic (for example : Robinson Arithmetic, that is weaker than Peano's) and says that we can find in an effective way a statement expressible in those formal systems that is "true" in the intended model (i.e. the model with domain the standard numbers and operation the standard addition and multiplication) but not deducible from the axioms.

This does not contradict the Completeness Th : the aforesaid statement is true in the standard model but is NOT true in some other "strange" model (there are many): this is the reason it is not deducible from the said axioms.

The arithmetical statement constructed by Godel in his proof is quite "strange", but starting from a result of Paris & Harrington (1977) has been possible, in mathematical logic, to find statements that are true (in the standard model) but not provable in Peano arithmetic and are more "natural". This was the first "natural" example of a true statement about the integers that could be stated in the language of arithmetic, but not proved in Peano Arithmetic.

  • I hope you don't mind my edit to clarify your first sentence. Along the way I also fixed some grammar and spelling. =)
    – user21820
    Sep 12, 2016 at 6:29

(adapted from a post of mine on MathSE)

NOTE1 Intuitionistic logic is NOT many-valued! (and in fact Goedel's name is again related to investigations in this direction)

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.

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)

You must log in to answer this question.

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