FOM: Pour-El on independent axiomatizations

[Sam Buss]

   I obtained a copy of Pour-El's article after hearing about it
from John Case on fom.  Since there has been a lot of discussion on
this topic, it's probably appropriate to summarize the contents of
the article for the fom mailing list:

 Pour-El, Independent Axiomatization and its Relation to the Hypersimple Sets,
	Zeitschrift f. math. Logik u. Grandlagen d. Math. 14 (1968) 449-456.

Pour-El also cites an abstract of Kreisel, 
"Independent recursive axiomatization", JSL 22 (1957) 109.

[Disclaimer: I haven't read the details of Pour-El's proofs and probably
won't, now that Harvey has provided us with a nice direct proof.]

The main theorem of theorems of the paper are as follows:

Theories T are first-order, consistent and axiomatizable.

Thm I:  The following are equivalent 

	a. T is not independently axiomatizable

	b. For any r.e. axiomatization A_1, A_2, ... of T, the set

		{ i : A_i is a logical consequence of A_1,..., A_{i-1} }

	   is hypersimple.

	c. The condition of b. holds for some r.e. axiomatization.

As a corollary, she gets:

Thm II:  If T^+ is a finitely axiomatizable, effectively inseparable
theory, then T^+ has an extension T which is no independently axiomatizable.

In the case where T^+ is Robinson's theory Q, then T can be taken to be
an extension of PA.

===

Some background definitions: two r.e. sets A and B are effectively
inseparable (e.i.) provided there is a recursive function g(i,j) so 
that for i,j, if W_i contains A and W_j contains B, W_i and W_j have
empty intersection, then g(i,j) is not in W_i or W_j.   Here W_i is the
i-th r.e. set in some effective enumeration.
   A theory T is e.i. if the set of theorems of T and the set of 
disprovable sentences of T are e.i.

===

Finally, Pour-El cites Kreisel as noting that if one takes Robinson's
theory, adds a new predicate symbol P, and the new axioms

   (forall x)[(exists y)K(x,y) -> P(x)]

for some formula K s.t.  { n : (exists y)K(n,y) } is a hypersimple set,
then one obtains a theory which is axiomatizable but not independently
axiomatizable.

   Regards,

	Sam