FOM: Finite Axiomatizations

[JoeShipman@aol.com]

Thanks to Allen Hazen for confirming that "finite GB" gives a finitely axiomatizable conservative extension of finite set theory.  It's still inelegant, though, so I'm forced to regard the original version of PA with the induction schema as the best formulation of finitary reasoning, despite my strong preference for first-order axioms over schemes.

By the way, I noticed that the eight GB class formation axioms given by Cohen seem redundant: 

1) There is a class representing the membership relation on sets
2) The intersection of two classes is a class
3) The complement of a class is a class
4) Given a class X, there is another class containing exactly the second components of the elements of X which are ordered pairs
5) Given a class X, there is another class containing all ordered pairs whose second component is in X.
6) Given a class X, there is another class containing exactly those ordered pairs <b,c> where the ordered pair <c,b> is in X.
7) Given a class X, there is another class containing exactly those ordered triples <b,c,a> where the ordered triple <a,b,c> is in X.
8) Given a class X, there is another class containing exactly those ordered triples <a,c,b> where the ordered pair <a,b,c> is in X.

Shouldn't you be able to eliminate 6)?  If you construct an ordered triple as an ordered pair whose second element is an ordered pair, you can reverse a class X of ordered pairs by applying axiom 5) to get V x X, then axiom 8) to get V x (X reversed), then axiom 4) to get X reversed, thus eliminating 6).   (I think you might also be able to keep 6) and eliminate 8).) 

One more question:  The famous graph minor theorem of Robertson and Seymour transcends both Peano Arithmetic and Predicative Arithmetic.  What is the best-known  theorem of "ordinary mathematics" which is independent of PA but predicatively provable?


-- Joe Shipman
-- Joe Shipman