# FOM: recursive independent axiomatizations

Harvey Friedman friedman at math.ohio-state.edu
Thu Dec 18 05:54:58 EST 1997

```This is a clarifiction to my e-mail of 6:02AM 12/17/97 which I reproduce
with a change in the proof of Theorem II. Sam Buss pointed out that the
proof is incomplete.

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
language expanding the language of PA with finitely many new symbols, with the
induction scheme for the expanded language, has a recursive independent
axiomatization. Furthermore, this holds even if we allow the addition of
finitely many new sorts, provided T also has the standard axioms for
encoding finite sequences of objects from the sorts.

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.

Let T be an r.e. extension of PA in the language of PA. Without loss of
generality, we may assume that T is consistent. Let A be a theorem of T.
Let n be the total number of quantifiers in A. Then it is well known that A
does not prove PAn+2 even in the presence of PAn, unless A + PAn is
inconsistent. However, A + PAn is consistent since T is consistent. (To see
this well known fact, note that PAn+2 + A proves the consistency of PAn +
A, [using formalized cut elimination and truth definitions], and apply
Godel's second incompleteness theorem. Now there's an application of some
REAL big gun f.o.m.!!). So we can take the value of a partial recursive map
at A to be simply PAn+2, and apply Theorem I.

Finally, we come to the second claim. Here we can define PAn analogously,
with analogous standard facts; so the argument goes through without
substantial change. The final claim is also analogous. QED,

```