FOM: Independent axiomatizations

[Sam Buss]

  Here are some more comments on independent sets of axioms for
systems such as PA.  (My apologies for the technical details; which
I've surrounded with  ======'s if you wish to skip them)

1. Torkel Franzen asked about

> the question whether PA is axiomatizable using a recursively
> enumerable subset of the induction axioms, none of which is a logical
> truth

  The answer here is that it *is* possible to give an axiomatization
for PA that involves only the usual base axioms Q, plus induction
axioms, so that no axiom is a logical truth.  The idea of the
construction is as follows:

==================(begin technical material)
   a. First isolate a finite fragment of PA (of I-Sigma-1 in fact),
so that every Pi_1 - formula A(x) is equivalent to a particularization
of a  universal Pi_1 formula U(n,x),  i.e., for all such A, there
is an integer n so that

	A(x) <-> U(n,x)      is provable.

   (I'm not sure who noted this originally, but it is certainly
possible from the formalization of the MDPR theorem in I-Sigma-1,
see Gaifman-DImitracopoulos.  It can also be proved without the MDPR
theorem.)

    b.  Letting  U_k(n,x,y_1,..,y_k) be a universal Pi_k formula
formed from U as Qy_1...Qy_kU(n,<x,y_1,...,j_k>) we have that
an induction axiom for U_k implies induction for all Pi_k (or all
Sigma_k) formulas.

    c.  Thus PA can be axiomatized by the base theory from a., plus
induction on each formula U_k.
===================(end technical material)

2. Bill Tait asked if there is "an r.e  axiom set equivalent to 
no r.e. independent set".    
   
   I conjecture the answer is "yes", but at the moment, can only
prove that there is an r.e. axiomatized
theory with no subset of its axioms an r.e. independent axiomatization
of the theory.

====================(begin technical material)
   Let B be a finite base theory for PA (e.g., the axioms for I-Sigma-1.)
Let M(x) be a Turing machine who's domain is an r.e., non-recursive
set.   Let P(x) be a new unary predicate symbol.  Consider the theory T
with axioms:
	
	i.   B
	ii.  (forall x)( M(x) halts  ->  P(x))
        iii. P( \underline n )     for all integers n.

Note iii. is an infinite set of axioms, \underline n means the term
SSSS...S0 (n S's) with value n.

   Any subset of the axioms of T which is independent and equivalent to
all of T must contain exactly axioms i. and ii. and exactly those
axioms iii. for n on which M does not halt.  
   But by choice of M, this set of axioms is not r.e.
QED
===================(End technical material)

   At the moment, I am unable to answer Tait's question, but maybe
someone else can provide an easy proof...

  Regards,

	Sam Buss