FOM: Re:no recursive independent axiomatization

[Harvey Friedman]

This posting is a sequel to my 8:05PM 12/18/97 posting.

1. Replace the sentence "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."    by

"To see iii), suppose W[e] is empty. Note that by the truth of PA1 + A,
"PA1 + A + W[e] is empty" is consistent."

2. There is a strengthening of Lemma 2 which suffices to prove the
following sharpened form of the Theorem:

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 true pi-0-1 sentences.

Here is the sharper form of Lemma 2:

LEMMA 2'. There is a recursive function f of two variables, from sentences
in the language of PA and elements of N, into pi-0-1 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.

This Lemma can surely be proved using the theory of creative r.e. sets or
effectively inseparable r.e. sets. But we have a proof of this without
making a detour through recursion theory. In fact, the only proof I know of
the following related classical results from logic even for PA makes a real
detour through recursion theory:

a. The pi-0-1 theorems of PA are not recursive.
b. The pi-0-1 theorems of PA are complete r.e.

In the course of proving Lemma 2' without a real detour through recursion
theory, we also immediately have a proof of these (b implies a, of course)
without a detour through recursion theory. A little background: if we
replace pi-0-1 by sigma-0-1 in a,b, then this is immediate without a real
detour through recursion theory. And the proof of Lemma 2 from my 8:05PM
12/18/97 gives a direct proof using Godel's second theorem for implications
between pi-0-1 sentences. What we have noticed is that we can give a direct
proof using Rosser's construction for the pi-0-1 case.

Proof of Lemma 2': Define f(A,e) to be PA1 + A + "every proof of this
sentence from PA1 + A has a shorter proof of its negation from PA1 + A +
"W[e] is empty." "  Let this sentence in outer quotes be B. Now i) is
obvious.

Suppose first that W[e] is nonempty. Let n be the least proof of notB from
PA1 + A + "W[e] is empty." If there is a proof of B from PA1 + A <= n, then
B is refutable in PA1, which is a contradiction. On the other hand, if not,
then B is provable in PA1. So B is provable in PA1. We also obviously get
that B is true.

Now suppose that W[e] is empty. Suppose B is provable in PA1 + A. Then B is
true. Hence there is no proof of notB from PA1 + A + "W[e] is empty."
Therefore B is false. So B is not provable in PA1 + A. We also obviously
get that B is true. QED.

In fact, we give a version of this proof in isolation, to derive the
classical result b.

THEOREM A (classical). Let T be any consistent recursively axiomatized
extension of a weak fragment of arithmetic. Then the set of pi-0-1 theorems
of T is complete r.e.

Proof: Let A be a pi-0-1 sentence. By self-reference, let B be a sentence
which asserts "every proof of B from T has a shorter witness of the falsity
of A." We claim that A is true if and only if B is not provable in T.

case 1. A is true. Suppose B is provable in T, and let n be the least
proof. Since there is no witness of the falsity of A, B is refutable in T.
This contradicts the consistency of T. Hence B is not provable in T.

case 2. A is false. Let n be the least witness to notA. If there is no
proof of B from T that is <= n, then B is provable in T. If there is a
proof of B from T that is <= n, then B is refutable from T. This
contradicts the consistency of T. Hence B is provable in T. QED.

Is this proof of Theorem A new? You can teach it right after you do
Rosser's theorem.

PS: Of course, the proof of Theorem A uses a simpler more direct
construction, we can also we used for Lemma 2'. Also, it is easy to see how
we can get a recursive set of purely universal sentences in predicate
calculus with no recursive independent axiomatization, by appropriate
Skolemizing.