The subtle difference between incompleteness (of a theory), completeness (of a proof system) and indecidability (of a logical system) are a common source of confusion. How come Gödel proved both completeness and incompleteness? How can a proof system be complete (there exists a proof for every true sentence) when the underlying logical system is undecidable (it is impossible to find a proof for every true sentence)?

The first question can be answered by something that should be familiar to everyone working in IT: bad naming. The “completeness” in the two theorems actually refers to two different things: completeness in the completeness theorem relates a formal proof system to model theory and says that a statement is true only if it can be proved (in a proof system for which completeness holds), that is \( \Pi \models X \Rightarrow \Pi \vdash X \) – read \( X \) follows from \( \Pi \) implies \( X \) is provable from \( \Pi \); the completeness in the incompleteness theorem refers to whether a theory \( \Pi \) contains every sentence or its negation, i.e. \( \forall X (\Pi \models X \lor \Pi \models \neg X) \) – read for each \( X \), either \( X \) or \( \neg X \) follow from \( \Pi \). It is not hard to see that those two statements have no direct relationship to each other – one of them talks about a theory (the \( \Pi \)), the other one about a proof system.

The second question is more subtle and can be explained by the slightly metaphysical definition of truth and existence in classical logic. We can rewrite the statement of the completeness theorem as “for each true statement, there exists a proof“. To do so, let’s define \( P(x, \Pi, \phi) \) to be the predicate that is true iff \( x \) is a valid proof for \( \Pi \vdash \phi \). Then a formalisation would be \(\Pi \models \phi \Rightarrow \exists p\;P(p, \Pi, \phi) \). Decidability, which could be expressed as “there exists a procedure with which, for every true statement, we can find a proof“, on the other hand, could be expressed as (for the reader following at home – this definition works because f can just return an invalid proof for \( \Pi \not\models \phi \)) \(\exists f, P\;( f \text{ computable} \land \Pi \models \phi \Leftrightarrow P(f(\Pi, X), \Pi, \phi)) \).

For a sound proof system (one that only proves true sentences, i.e. \( \Pi \models X \Leftarrow \Pi \vdash X \)), completeness of a proof system would imply decidabilty if you left out the part about computabilty. The difference is that explicitly quantifying over the function and requiring it be computable means there has to be a procedure, while a simple exists quantifier introduces an implicit function. The notion of procedure is a lot stronger than function; a function as defined in mathematics is simply a mapping from one set to the other (whereof there are uncountably infinite for infinite sets), while procedure requires a formal (finite) representation that could be executed by a computer (whereof there are countably infinite).

This mirrors the distinction between classical and intuitionistic logic. In classical logic, there is a platonic idea of truth (and thus existence): it is legitimate to refer to an object that one has no procedure on how to produce, if one can infer it has to exist (whatever it is). Intuitionistic logic, however, is a lot stricter and requires there to be a procedure on how to produce the objects.