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. Gödel's theorem says that axiomatic systems containing PA are never complete - they are incomplete.

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?

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?

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. Godels theorem says that axiomatic systems containing PA are never complete - they are incomplete.

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/proveability 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?

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. Gödel's theorem says that axiomatic systems containing PA are never complete - they are incomplete.

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?