recursive inseparability of the two Gödelnumber-sets: theorems and 'anti-theorems' of EA

Question

Here again one of my more or less basic proof-theoretic questions, working through Girards monograph from '87.

This is about exercise 1.5.10. - "recursive inseparability", on page 80.

It is this:

Let A and B be disjoint recursively enumerable subsets of $\mathbb{N}$; A and B are called $\textit{recursively inseparable}$ if and only if there is no recursive subset C of $\mathbb{N}$ such that $A \subset C, B \subset \complement{C}$.

Show that the sets $A= \{x \mid Thm_{EA}[x]\}$ and $B= \{x \mid Thm_{EA}[\langle 13, x \rangle]\}$ are recursively inseparable.

[Remark: So A is the set of the Gödelnumbers of the theorems of EA, and B is the set of the Gödelnumbers of formulae such that the negations of these formulae are theorems of EA. (13 is the Gödelnumber of the negation sign).]

So there shall be no subset C of the natural numbers such that C and its complement 'divide' A and B from each other, in the sense that the theorem-numbers are part of C and the formula-numbers, when the negated formula is a theorem, are part of C's complement.

It might have something to do with Church's theorem:
Any extension T of EA in the language of EA is either undecidable or inconsistent.
Here 'decidable' means that the set of the Gödelnumbers of the theorems of T is recursive, that is there is a recursive function that 'says yes' (say, = 0) on the theorem-numbers and 'says no' ( = 1) on any non-theorem-number.

We may assume that EA is consistent, I think, cause otherwise any formula is a theorem, and A and B are just the same, so they are not even disjoint.

I guess if there was such a C we could construct a recursive function for A, the set of theorem-numbers, contradicting Church's theorem. Because then we'd already have a recursive function 'sort of dividing' A from B, we'd only have to figure out a way in which this function can be alternated to 'deal properly' with the numbers that are not in A neither in B.

Regards and Thanks,

Ettore

Answer 1

Already has an answer, even here on SE: Show that a recursively inseparable pair of recursively enumerable sets exists

The idea lies in the diagonal lemma: The assumed separating set C can be represented by a formula $\varphi$ in EA, which in turn is connected biconditionally in EA to a formula $\tau$. This formula $\tau$ has a Gödel number. If one asks oneself where this number might lay, in C or its complement, one gets a contradition either way.

Answer 2

To do the neat argument using `I am not in C' we need a bit more detail.

Suppose C a recursive set that separates the theorems and anti-theorems of our given theory, say U. (We must assume it is consistent and interprets some suitable base theory like the Tarski-Mostowski-Robinson theory R.) Then there are \Sigma^0_1-formulas S(x) and S'(x) that represent C and its complement. The problem is still that U does not need to be able verify that S' and S are disjoint. To fix that we replace S(x) by S^\ast(x) that says there is a witness that x is in S strictly before there is a witness that x is in S' ' and we replace S'(x) by S^\dag(x) that says there is a witness that x is in S' before or at the same time as there is a witness that x is in S'. The theory can now verify that S^\ast and S^\dag are disjoint. We apply the fixed point theorem to find \phi iff \neg, S^\ast(\phi) (confusing formulas with the numerals of their gödelnumbers).

Suppose U \vdash \phi. Then, S^\ast(\phi) is true. It follows that U \vdash S^\ast(\phi) and so U \vdash \neg \phi. A contradiction with the consistency of U. Suppose U \vdash \neg \phi. Then, S^\dag(\phi) is true and, hence, U \vdash S^\dag(phi). It follows that U \vdash \neg S^\ast(\phi). (For this step we need the pair S^\ast, S^\dag, rather than S, S'.) So, U \vdash \phi. Again this contradicts the consistency of U.

An alternative proof uses the representability of recursive functions in U. (the Kleene-style argument)

We note that Ehrenfeucht provides an example of a theory that is essentially undecidable but not recursively inseparable. So an argument using extendability to a complete theory cannot work.