Peano arithmetic (PA) is the logical system which includes the nonnegative integers, plus, and times; i.e. number theory. In my foundations of mathematics class I saw the axioms of PA written for the first time. There are infinitely many of them (an axiom schema). While it is of little practical importance, it irritates me that such a fundamental system (provably) has no finite axiomatization.

So the question becomes: can I create a conservative extension of PA that is finitely axiomatizable, much like NBG Set Theory is to ZFC. And I think the answer is yes.

I don’t get to name much after myself (and I’m pretty sure somebody else has already done this), so for kicks, I’ll name it Peano-Palmer axioms. Hmm, I’m using Gödel’s method, so I’ll stick him in there: Peano-Gödel-Palmer axioms. You can abbreviate that to PGP, which emphasizes the importance of number theory to public-key cryptography `:-)`.

The way I’ll do this is to add a continuum of objects into the number-theoretic universe: the subsets of ω (ω is the set of all nonnegative integers, the domain of discourse of PA). Basically I’m taking PA and adding in a teeny bit of set theory, so that we don’t need to use a schema to get induction. The theory, then, will be two-sorted: lowercase letters will represent numbers as usual, uppercase letters will represent sets of numbers. If you don’t like sorted theories, you can pretend that there is a predicate Set(), and replace “∀x” with “∀x ¬Set(x) ⇒”, “∀X” with “∀X Set(X) ⇒”, and similarly for the existence quantifiers.

Here are the basic axioms of PA. The symbols of the theory are: (0, S) together with the new symbol (ε). 0 is the number 0, S is the successor function (plus 1), ε means “element of”, and is only defined when the left side is a number and the right side is a set (we could say it is false otherwise).

- ¬∃x. S(x) = 0 — no number plus 1 is 0
- ∀x,y. S(x) = S(y) ⇒ x = y — successor is one-to-one (distinct natural numbers have distinct successors).
- (schema) for every property with one free variable φ(x), (φ(0) ∧ ∀x.(φ(x) ⇒ φ(S(x)))) ⇒ ∀x. φ(x). This is the induction schema: if a property holds for 0, and from the property holding at x it follows that it holds at x+1, then it holds for all natural numbers.

The last axiom is actually infinitely many of them: one for every logical formula φ. We would like to get rid of it, and replace it with finitely many other axioms. So here we go:

- Extensionality: ∀X,Y. X = Y ⇔ ∀u. (u ε X ⇔ u ε Y). Two sets are equal when they have the same elements.

At this point, I would have liked to write that “every concievable set exists”, i.e. every combination of natural numbers is equal to some set. However, I could not think of a way to do that (read: I do not think there is a way to do that)^{1}. So this is where Gödel’s method comes in: I will recreate first-order logic as set theory.

- Union axiom (standing in for logical or): ∀X,Y ∃Z ∀u. u ε Z ⇔ (u ε X ∨ u ε Y).
- Intersection axiom (standing in for logical and): ∀X,Y ∃Z ∀u. u ε Z ⇔ (u ε X ∧ u ε Y).
- Complement axiom (standing in for logical not): ∀X ∃Y ∀u. u ε Y ⇔ ¬(u ε X).
- Zero axiom (standing in for the PA constant symbol): ∃X ∀u. u ε X ⇔ u = 0.

Okay, now we need a way to express relations. To do that, we need an ordered pair. This we can easily do with <m,n> = 2^{m}3^{n}, once we define plus, times, and exponentiation. The subtle problem is that in order to use this as a unique ordered pair, we need some theorems about numbers which we can only get using induction, but we are not through defining induction yet. A very difficult exercise for the reader should be to see if the axioms mutually support each other and still give us an extension of PA, or if they can also go some other way and make some weird non-arithmetical system. Whatever the answer, it is not important to our finite axiomatization, since we could introduce a third sort of object, an ordered pair, and make some (surely finite) axioms about them.

Nontheless, let’s proceed with our axioms:

- Diagonal axiom (standing in for logical equality): ∃X ∀u,v. <u,v> ε X ⇔ u = v.
- Successor axiom (standing in for the PA function symbol): ∃X ∀u,v. <u,v> ε X ⇔ S(u) = v.
- Product axiom (allowing us to introduce a dummy argument): ∃X ∀u,v. <u,v> ε X ⇔ v ε X.
- Domain axiom (allowing us to extract variables): ∀X ∃Y ∀u. u ε Y ⇔ ∃v <u,v> ε X.
- Commutativity axiom (allowing us to reorder arguments): ∀X ∃Y ∀u,v. <u,v> ε Y ⇔ <v,u> ε X.
- Association axiom (more reordering): ∀X ∃Y ∀u,v,w. <u,<v,w>> ε Y ⇔ <<u,v>,w> ε X.
- Induction axiom (the fruit of all our efforts): ∀X. (0 ε X ∧ (∀u. u ε X ⇒ S(u) ε X)) ⇒ X = ω (where ω may be defined as any set union its complement).

To show that we can do something with these axioms, let’s do something seemingly simple. Construct the set of <x,y> such that S(x) = S(y). (We could show that this is a subset of the diagonal set to verify axiom 2)

Let’s rewrite the statement so we have a handle on how it could be handled by sets: ∃u,v. u=S(x) ∧ v=S(y) ∧ u=v. Adopting some less formal notation, we can get our {<x,u>} and {<y,v>} with the proper relations by the successor axiom. Then use product, intersection, and commutivity to get {<<x,u>,m>} ∩ {<n,<y,v>>} = {<<x,u>,<y,v>>}. Use commutivity and associativity to get {<<u,v>,<x,y>>}, then domain to get {<u,v>}. Use intersection and diagonal to get a new set of all u,vs that equal each other. Use product to get {<<u,v>,n>} and intersect that with the {<<u,v>,<x,y>>} from above. Now reorder and use domain to get all the appropriate {<x,y>} where u and v match. We have constructed our desired set. Whew.

(If you could follow that, kudos; it was more for me than for readers.)

Presumably you can construct any set of objects that you could specify a formula about with this method. You wouldn’t want to, but you could. Construct the set, do some math and show that that set is equal to ω by the induction axiom. That’s how you do induction in our new system. And it is finitely axiomatized! Ahh, my aesthetic sense is so much more comfortable now (Yes, even after the abomination of the previous paragraph).

What is left is to show that this is a *conservative* extension of PA (thus if PA is consistent then so is PGP). Such a task is beyond my ability at this point, but I hope to at least have an idea of how this is done by the end of the semester.

^{1} **UPDATE:** I believe the reason that I was unable to come up with a way to write “every concievable set of integers exists” is a result of the

Yes!

Great.

http://www.jstor.org/pss/2964289 Here is a paper that might interest you. It very much interests me.

My bad, I posted the follow up to Kleene’s paper. I ment to post Kleene’s paper on the same topic. I can’t find a link on the interenet to it, but here is info for what journal its in http://books.google.com/books?id=qi8PAAAAIAAJ

I’m late to the party, but what you have re-invented is the subsystem [ACA0](http://en.wikipedia.org/wiki/Second-order_arithmetic#Arithmetical_comprehension) of second-order arithmetic. It is indeed conservative. The proof involves assigning codes to subsets of the natural numbers to translate statements of ACA0 into statements of PA.

In conclusion: yes, you re-invented a well-known system of axioms, and yes, it is a conservative extension of arithmetic. But rejoice! The fact that it exists and is well studied means your idea was clever indeed!