FOM: Pour-El on independent axiomatizations
Sam Buss
sbuss at herbrand.ucsd.edu
Fri Dec 19 20:21:47 EST 1997
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
More information about the FOM
mailing list