FOM: no recursive independent axiomatization

[Harvey Friedman]

NOTE: After I did this, Buss told be that the Pour El paper has this result
in some ways more generally, using hyperhypersimple sets. This proof may
well be more friendly for the nineties. Also, the positive theorem of my
earlier postings isn't there. And it may not address the logical complexity
of the axiomatizations as I do. I have't looked yet.
**************************

This posting is a sequel to my 6:02AM 12/17/97 posting, and my 11:54AM
12/18/97 posting.

We prove that there is a true r.e. extension of PA1 in the language of PA
with no recursive independent axiomatization. Let W[e] be the e-th r.e. set.

LEMMA 1. There is a recursive sequence e1,e2,... of natural numbers such
that infinitely many W[ei] are empty, and the following fails for all
recursive functions f: For all i there exists i < j <= f(i) such that W[ej]
is empty.

Proof: Call a pair (n,m) critical if and only if m is the least natural
number such that for all 1 <= i <= n, if W[i] is nonempty then W[i] is
first seen to be nonempty in <= m stages of computation. Note that for all
n there exists a unique m such that (n,m) is critical, and also as n
increases, m increases (<=). Also, the m's are unbounded.

For n,m, let P(n,m) be the statement "(n,m) is critical." Note that P is
co-r.e. Let h(n,m) be the recursive function that outputs the natural index
of an r.e. set which is empty if and only if P(n,m).

We now define ei. If i is of the form (2^n)(3^m) then take ei = h(n,m).
Otherwise, take ei to be a fixed r.e. index of {0}. We claim that e1,e2,...
is as required. Suppose not, and let f be a recursive function as in the
statement of the Lemma. Then when we iterate f  p times starting at e1, we
get past the p-th critical pair. But this yields a recursive upper bound as
to how long it takes to see that an arbitrary r.e. set is nonempty. This is
a contradiction. QED.

LEMMA 2. There is a recursive function f of two variables, from sentences
in the language of PA and elements of N, into sentences in the language of
PA, such that the following holds. Suppose PA1 + A is true. i) f(A,e)
logically implies A & PA1. ii) if W[e] is nonempty then f(A,e) is provably
equivalent to A over PA1. iii) if W[e] is empty then A does not imply
f(A,e) over PA1. iv) f(A,e) is true.

Proof: Define f(A,e) to be PA1 + A + "if W[e] is empty then Con(PA1 + A +
W[e] is empty)." Let PA1 + A be true. Then i) and iv) are obvious. To see
ii), note that if W[e] is nonempty then the statement in quotes is
trivially provable in PA1. To see iii), suppose W[e] is nonempty. Note that
by the 1-consistency of PA1 + A, PA1 + A + W[e] is empty is consistent. is
consistent. Now if PA1 + A proves f(A,e), then PA1 + A + W[e] is empty
proves its own consistency, contrary to Godel's second incompleteness
theorem (now there's some REAL big gun f.o.m.!).

THEOREM. There is a true r.e. extension of PA1 in the language of PA with
no recursive independent axiomatization. Furthermore, it has a recursive
axiomatization consisting entirely of implications between pi-0-1 sentences.

Proof: Let e1,e2,... be as given by Lemma 1. Let A0 = PA1. For n >= 0 let
An+1 = f(An,en). Let T be axiomatized by {A0,A1,...}. Suppose that T has a
recursive independent axiomatization. Then by Theorem 1 of 6:02AM 12/17/97,
let f be a recursive function such that for all i >= 0, f(Ai) is a theorem
of T that does not logically follow from Ai. So let g be a recursive
function such that for all i >= 0, A_g(i) does not logically follow from
Ai. By Lemma 2, there exists i < j <= g(i) such that W[ej] is empty. But
this contradicts Lemma 1. QED.