Deducing PA's axioms in ZFC
Recently I've stumbled across this claim:
Peano axioms can be deduced in ZFC
I found a lot of info regarding this claim (e.g. what would (one version of) the natural numbers look like within the universe of sets: $0 = \emptyset$, $n + 1 = n \cup \{n\}$), but not what the deductions (ZFC $\vdash$ PA) actually look like. What do they look like?
Solution 1:
Do you mean the original Peano Axioms (with an unrestricted second-order induction axiom), or Peano Arithmetic (known as PA, with a first-order axiom scheme)? Though it's not much different for the purpose of this question.
Before you can start deriving the PA axioms, of course, you run into the problem that they are phrased in the language of integer arithmetic, whereas ZFC only proves things in the language of set theory. So you need to decide on some way to translate logical formulas in the language of arithmetic to set-theoretical formulas.
It's conventional enough to represent $0$ as $\varnothing$ and $S(t)$ as $t\cup\{t\}$, and also to make sure every quantifier and free variable in the arithmetical formula are restricted to range over $\omega$. Representing addition and multiplication leaves some room for choice, though.
If you're working in a not too barebones development of ZFC, it is natural to represent PA addition and multiplication by ordinal addition and ordinal multiplication, which you'll already have investigated as purely ZFC phenomenons. Deriving each of the PA axioms except for instances of the induction scheme is then a straightforward boring matter of definition chasing.
Each instance of the induction axiom scheme now arises as a special case of a general induction theorem in ZFC:
$$ \forall A\subseteq \omega: (\varnothing \in A \land \forall x\in A: x\cup\{x\}\in A)\to A = \omega $$
In order to derive an instance of PA induction from this, simply let $A$ be $\{x\in\omega \mid \phi(x) \}$, where $\phi$ is the set-theoretic representation of the arithmetic formula you're inducting over.
The induction theorem itself follows from the Axiom of Infinity. The details are a bit sensitive to the exact phrasing of the Axiom of Infinity you're working with, but typically the Axiom of Infinity will state that there exists at least one set $X$ such that $$\varnothing\in X ~\land~ \forall y\in X:y\cup\{y\}\in X$$ and $\omega$ is then defined as the intersection of all $X$ satisfying this condition. Notice that the condition is the same as the hypothesis about $A$ in the induction theorem. So if we have an $A\subseteq \omega$ that satisfies the hypothesis, then by definition $\omega$ is the intersection of a class of sets that includes $A$. In particular we must then have $\omega\subseteq A$, and since $A\subseteq \omega$ was assumed, we conclude $A=\omega$ as desired.
Exactly how the above English proof becomes a fully formal proof in ZFC depends a lot of the precise formalizations of ZFC and first-order logic you're working with, but in ways that are not really specific to the application to PA.
Solution 2:
The most direct, model-theoretic method to prove the existence of a model of PA within ZFC is as follows:
First, we formalize the syntax of PA within ZFC. The method is similar to the one used for formalize syntax for the second incompleteness theorem. The main result is a formula $S(n,m)$ which says that $n,m\in \omega$, and $n$ codes a formula $\phi_n(x_1)$ in the language of PA with one free variable and $$(\omega, +,\times,0,1, =) \vDash \phi_n(\ulcorner m\urcorner).$$ Developing this formula $S$ takes some time but the methods are completely standard
Then, using the axiom of separation, one uses ZFC to form the set $$I = \{(n,m) \in \omega^2 : \text{$m$ is minimal such that } S(n,m) \}$$
Now one must verify in a single ZFC proof that $(\omega, +,\times,0,1,=) \vDash PA$. This goes as follows. Using the formalization from part 1, ZFC proves, for some $k$, that there are coded axioms $n_1, \ldots, n_k$ of PA such that for any coded axiom $n$ of PA, either $n=n_i$ for some $i < k$ or $n$ is a coded induction axiom. In the first case, we can do a proof by cases to verify that $(\omega, +,\times,0,1,=)$ satisfies the axiom coded by $n_i$. In the latter case, where $n$ is an induction axiom, we use the single set $I$ from part 2 as a parameter to verify that the axiom coded by $n$ holds in $(\omega, +,\times,0,1,=)$. Namely: if the induction axiom failed for some coded formula $\phi(x)$ then if we let $\phi_r(x)$ be the negation of $\phi(x)$ the set $\{ m \in \omega : (r,m) \in I\}$ would have no least element.