FOM: recursive independent axiomatizations

[Harvey Friedman]

This concerns Tait, 9:08AM 12/13/97.

We prove that every r.e. extension of PA has an r.e. independent
axiomatization.

Clarification: Any r.e. theory has a recursive axiomatization. Any theory
with an r.e. independent axiomatization has a recursive independent
axiomatiation.

THEOREM I. Let T be an r.e. theory in predicate calculus with equality, in
a recursively presented language. Then T has an infinite recursive
independent axiomatizaion if and only if there is a partial recursive
function which maps every consequence A of T to another consequence B of T
such that A does not logically imply B.

Proof: Let T be as given, and assume that T has an infinite recursive
independent axiomatization. Given any sentence A in the language of T, we
search for a proof using finitely many terms in the infinite recursive
independent axiomatization. If we find it then we output the next term
after the highest term among the finitely many terms found.

On the other hand, suppose f is a partial recursive function as described.
Let A1,... be any recursive enumeration of T. Define B1,B2,... as follows.
Take B1 = f(A1) & A1. Take Bi+1 = f(Bi) & Bi & Ai+1. Then B1,B2,... is a
recursive axiomatization of T where B1 is not logically valid, and for all
i, Bi+1 logically implies Bi and Bi does not logically imply Bi+1.

Now consider B1, B1 arrows B2, B2 arrows B3, etcetera. Clearly this is also
a recursive axiomatization of T. Now suppose B1 logically follows from
finitely many other terms. Note that every term other than B1 logically
follows from notB1. Hence B1 logically follows from notB1, and so B1 is
logically valid, which is a contradiction.

Now suppose Bi arrows Bi+1 follows logically from finitely many other
terms. The earlier terms all logically follow from Bi, and the later terms
all logically follow from notBi+1. So we have {Bi,notBi+1} logically
implies (Bi arrows Bi+1). Hence {Bi,notBi+1} logically implies Bi+1.
Therefore Bi logically implies Bi+1, which is a contradiction. QED.

THEOREM II. Every r.e. extension of PA has a recursive independent
axiomatization. Moreover, every r.e. extension of PA formulated in a
recursively presented language extending the language of PA, with the
induction scheme for the expanded language, has a recursive independent
axiomatization.

Proof: PA is in the language of 0,S,+,x,= with basic axioms (successor
axioms and defining equations) and the induction scheme. For each n >= 1,
let PAn be the basic axioms together with the induction scheme with respect
to all formulas with at most n quantifiers and any number of bounded
quantifiers and any free variables. It is well known that PAn is finitely
axiomatizable, and the finite axiomatization is effectively given in n.
Suppose A is a given sentence. Search for a proof in PA. If one is found,
say in PAn, then output PAn+1. QED.