Monthly Archives: September 2006

Finite Axiomatization of Peano Arithmetic

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.

Continue reading Finite Axiomatization of Peano Arithmetic