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.
Hi Andrei,
This is a nice example of recursive inseparability! But something is a little unsatisfying here: usually theories are closed under substitution, whereas your
is not. Is there a way to use the same/similar trick to devise a theory that is closed under substitution and essentially incomplete?
Theories are not closed under substitution, they are usually closed under deduction, so one can just take the deductive closure – that is why I usually don’t bother with pointing this explicitly (even in the definition of a theory).
I would say that it depends whether we treat ‘propositional variables’ as actual variables or constant symbols…. but for the avoidance of ambiguity, let us henceforth call a set of propositional formulas closed under deduction and substitution a ‘logic’.
I think the answer to my question above is negative, since classical propositional logic is maximally consistent; if we add any non-tautologous formula as an axiom, then it becomes inconsistent. However, the question does seem to make sense for Intuitionistic Propositional Logic. Can we use the same idea to find an essentially incomplete intermediate logic?