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?