How is Gödel's incompleteness theorem interpreted in intuitionistic logic?

Question

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?

Answer 1

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 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.

Answer 2

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.

Answer 3

(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.

BUT

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)

Why?

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.

BUT

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

Why?

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)

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)