FOM: finitely axiomitized conservative extension of PA

[Martin Davis]

In connection with Joe Shipman's recent request, the following may be of 
some interest:

In the summer of 1959, Hilary Putnam and I produced a report from Rensselaer
Polytechnic (AFOSR TR59-124) that contained three papers one of which 
concerned a system along the lines Shipman requested.

[If anyone cares, the other two papers were, respectively, on a proof
algorithm for predicate calculus(later published in the JACM becoming
somewhat notorious). and an early version of the Davis-Putnam-Robinson
theorem on exponential Diophantine equations (before Julia Robinson had
eliminated our needed hypothesis that there are arbitrarily long arithmetic
progressions consisting entirely of primes). ]

Here are the axioms:

GROUP A.
1, x=y <=> (Az)[ x \in z <=> y \in z]
2. x \in y => x \in N & y \not\in N

GROUP B.
1. 1 \in N
2. x \in N => x+1 \in N
3. x+1 = y+1 => x=y
4. \neg (1 = x+1)
5. [ (1 \in z) & (Ax)( x \in z => x+1 \in z)] => (Ax)(x \in z => x+1 \in z)

GROUP C.
1. J(x,y) = J(x',y') => (x=x') & (y=y')
2. J(x,y) \in N <=> (x \in N) & (y \in N)
3. x+(y+1) = (x+y)+1
4. x*1 =x
5. x*(y+1)=x*y+x

GROUP D.
1. x \in {y} <=> x=y & x \in N & y \in N
2. x \in (y \cap z) <=> x \in y & x \in z
3. x \in -y <=> x \in N & x \not\in y
4. J(x,J(y,z)) \in \sigma <=> y \in N & z \in N & x = y+z
5. J(x,J(y,z)) \in \pi <=> y \in N & z \in N & x = y*z
6. J(x,y) \in I <=> x \in N & y \in N & x = y
7. x \in P(y) <=> (Ez)(J(z,x) \in y)
8. J(x,y) \in G(z) <=> J(y,x) \in z
9. J(x,J(y,z)) \in D(u) <=> J(y,J(z,x)) \in u
10.J(x,J(y,z)) \in L(u) <=> J(x,J(z,y)) \in u
11.J(u,v) \in (x X y) <=> (u \in x) & (v \in y )

Martin


                           Martin Davis
                    Visiting Scholar UC Berkeley
                      Professor Emeritus, NYU
                          martin at eipye.com
                          (Add 1 and get 0)
                        http://www.eipye.com