Consider the following formulation of Gödel’s first incompleteness theorem.
Theorem. Any complete, consistent theory that extends PA is not recursive. In other words, PA is essentially incomplete.
Five years ago, I wondered whether such a recursively enumerable and essentially incomplete theory could be easily found in classical propositional logic, where formulas are built up from a countable set of variables using negation and implication. It turns out that this is an almost immediate consequence of the following classical result, which asserts the existence of recursively inseparable sets.
Theorem. There exist disjoint sets , which are recursively enumerable such that there is no recursive with and .
Proof. Let be a partial binary computable function which is universal, in the sense that for every partial unary computable function there is an such that . Let to be the set of all such that and the set of all such that . Suppose that there is a as in the statement, and let be such that . Assume that . Then , so , which contradicts . Thus , i.e. , so , which contradicts .
Now take and as above and to be the set . We show that this consistent theory is essentially incomplete. Assume that there is a complete recursive extension of . Then the set of all such that is also recursive and separates and , a contradiction.