# Demetri Martin in Boulder

A few months ago I sent an email to my favorite living comedian, Demetri Martin, asking him to come to Boulder on his tour. I checked his tour today, and he’s going to on November 16! I’ll just pretend that the reason is because I asked him :-).

# You Learn the Blues

I had Cake’s “You Turn the Screws” going through my head all day, so today’s improvisation is a development of that theme.

# 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.