In what sense is $\sf ZFC$ "stronger" than Peano arithmetic?

There are various ways to say $\mathsf{ZFC}$ is stronger than $\mathsf{PA}$.

One way to compare them is to measure their arithmetical consequences. Both $\mathsf{ZFC}$ and $\mathsf{PA}$ can express statements on arithmetic, and we can see that $\mathsf{ZFC}$ proves more arithmetic statements than $\mathsf{PA}$. ($\mathsf{Con(PA)}$ is an example.) Some subsets of arithmetical consequences (for example, $\Pi^0_2$-consequences of a theory) are adopted to measure the proof-theoretic strength of a given theory.

However, the above method is only applicable when the given theories are able to express arithmetic. There is a more direct (perhaps more akin to looking one theory implies another) way to see it: interpretation. Let me introduce its formal definition, as finding its definition online seems not easy.

Definition. Let $T_0$ and $T_1$ be theories over a language without function symbols (but not necessarily over the same language.) Then an interpretation $\mathfrak{t}:T_0\to T_1$ is a map which sends a formula to a formula as follows:

• $\mathfrak{t}$ preserves $\land$, $\lor$, $\to$ and $\lnot$, e.g., $(\phi\land\psi)^\mathfrak{t}$ is $\phi^\mathfrak{t}\land\psi^\mathfrak{t}$,
• There is a formula $\delta(x)$ over $T_1$ (which means domain of an interpretation) such that $(\forall x\phi(x))^\mathfrak{t}$ is $\forall x \delta(x)\to\phi^\mathfrak{t}(x)$, and $(\exists x\phi(x))^\mathfrak{t}$ is $\exists x \delta(x)\land\phi^\mathfrak{t}(x)$,
• For each relation symbol $R$ over $T_0$, there is a formula $\phi_R$ (with the same arity of $R$) such that $\mathfrak{t}$ assigns $R$ to $\phi_R$.
• Furthermore, if $T_0\vdash\phi$ then $T_1\vdash \phi^\mathfrak{t}$.

For example, there is an interpretation from the theory of $(\mathbb{Z},+)$ to the theory of $\mathbb{N}$: we can code integers and the addition operation by the standard method. Another example is an interpretation from $\mathsf{ZFC}$ to $\mathsf{ZF}$: taking a constructible universe yields this interpretation. We may call $T_1$ is stronger then $T_0$ if there is an interpretation from $T_0$ and $T_1$, since $T_1$ can simulate $T_0$ inside itself.

We can see that $\mathsf{ZFC}$ can interpret $\mathsf{PA}$: we know that $\mathsf{ZFC}$ can define the set of natural numbers $\mathbb{N}$ and operations over $\mathbb{N}$. This gives a natural interpretation of arithmetic into $\mathsf{ZFC}$.

Hanul Jeon gave a typical definition for "interpretation", but that is a rather restricted definition. In particular, it only applies for FOL theories. So for example we are unable to express statements like:

1. Intuitionistic logic interprets classical logic (via the double-negation translation).

2. Every computable formal system that interprets PA$^-$ (now what does this mean?) is either arithmetically inconsistent or arithmetically incomplete.

Here is a much more general notion of interpretation that covers all these cases as well as all other formal systems that can ever be conceived of in the future.

A formal system $S$ is a triple $⟨L,T,C⟩$ where $L$ is a set of strings (of symbols over some alphabet) and $T⊆L$ and $C∈L$. We will call $L$ the language of $S$, and call $T$ the theorems of $S$ and call $C$ a contradiction over $S$. We say that $S$ is consistent iff $C∉T$. We say that $S$ is computable iff $L,T$ are computably enumerable sets.

For example, an FOL system can be defined as a triple $⟨L,T,C⟩$ where $L$ is some set of sentences over an FOL language and $T$ is a deductively closed subset of $L$ under FOL deduction and $C$ is the string "$⊥$".

Given formal systems $S=⟨L,T,C⟩$ and $S'=⟨L',T',C'⟩$, we say that $S'$ interprets $S$ iff there is a computable translation function $ι : L→L'$ such that for every string $Q∈T$ we have $ι(Q)∈T'$. Furthermore, we say that $S'$ consistently interprets $S$ iff $S'$ interprets $S$ and $ι(C)=C'$.

For example, ZFC consistently interprets PA, and HA (Heyting arithmetic) consistently interprets PA too. By definition, any formal system that is consistently interpreted by some consistent formal system is itself consistent. Hence this definition of interpretation allows us to reason about relative consistency of all kinds of formal systems in general, not just about FOL theories.

For another example, every computable formal system that interprets PA$^-$ via translation $ι$ is either arithmetically inconsistent or arithmetically incomplete (i.e. for some arithmetical sentence $Q$ with negation $¬Q$ it either proves both $ι(Q)$ and $ι(¬Q)$ or proves neither $ι(Q)$ nor $ι(¬Q)$).

Note that every reasonable foundational system $F$ for mathematics must consistently interpret PA$^-$, as this is nearly the minimum to permit us to say that $F$ can reason about basic arithmetic, and hence the Godel-Rosser incompleteness theorem applies. But if we want to apply the general incompleteness theorem to $F$, it suffices to show that $F$ can reason about programs (as defined in the linked post), which roughly amounts to showing that $F$ interprets TC. In fact, PA$^-$ interprets TC, and this fact can be proven using Godel encoding. However, Godel encoding is not necessary for proving most stronger systems arithmetically incomplete (see here).

We can define a partial order on formal systems where $S ≤ S'$ iff PA proves that $S'$ consistently interprets $S$. This partial order represents in some sense the order of the strength of formal systems. Naturally, we also define $S < S'$ iff $S ≤ S'$ but $S' \not≤ S$, and define $S ≡ S'$ iff $S ≤ S' ≤ S$. Then it turns out that we have a very tall hierarchy (if ZFC is consistent):

• TC $≤$ PA$^-$ $<$ HA $≡$ PA $≡$ ACA0 $<$ ACA $<$ ATR0 $<$ $Π^1_1$-CA0 $<$ Z2 $<$ Z $<$ ZF $≡$ ZFC

Here ACA0, ACA, ATR0 and $Π^1_1$-CA0 are well-known subsystems of Z2 (full second-order arithmetic) that are studied in reverse mathematics. I mention them to give you an idea of how many systems have strength in-between PA and ZFC.

In general, we can climb the strength hierarchy via consistency statements. Define that a formal system $S' = ⟨L',T',C'⟩$ standardly interprets $S$ via $ι$ iff $S'$ consistently interprets $S$ via $ι$ and $T'$ is closed under MP under $ι$, which is the rule ( $ι(Q),ι(Q⇒R) ⊢ ι(R)$ ). For such $S'$, define $S'+ι(Q) = ⟨L',T'',C'⟩$ where $T''$ is the minimal superset of $T'∪\{ι(Q)\}$ closed under MP under $ι$, and note that $S'+ι(Q)$ also standardly interprets $S$.

Take any computable formal systems $S ≤ S'$ such that $S'$ standardly interprets PA via $ι$ and $S'$ proves $ι$( $S$ is consistent ). Then $S < S'$, otherwise $S'$ proves $ι$( $S$ consistently interprets $S'$ ) and hence proves $ι$( $S'$ is consistent ), which is impossible if $S'$ is really consistent. This last fact is essentially Godel's second incompleteness theorem. For completeness, here is an outline of the proof: Let "$⬜Q$" denote "$S'$ proves $ι(Q)$". Let $G$ be an arithmetical sentence such that PA proves ( $G⇔¬⬜G$ ). Then $⬜(G⇔¬⬜G)$. Thus $⬜G$ implies both $⬜⬜G$ and $⬜¬⬜G$, which yield $⬜\bot$. Thus $⬜(¬⬜\bot⇒¬⬜G)$. If $⬜¬⬜\bot$, then $⬜¬⬜G$ and hence $⬜G$, which yields $⬜\bot$.