I was revisiting the discussion under a previous question of mine, and realized that I don't know how to rigorously formulate the notion of a theory being stronger than another.

If the two theories are formulated in the same language, then you can say that a theory is syntactically stronger than another if it implies it.

But what about in a case like $\sf ZFC$ and $\sf PA$? Do you need to construct a homomorphism from the language of $\sf PA$ to the language of $\sf ZFC$ or something?

  • $\begingroup$ There are some possible formulations. If your theories allow recursive axiomatization, you may compare their consistency strengths. You may also use interpretations to compare theories with different languages. $\endgroup$
    – Hanul Jeon
    Commented Sep 8, 2020 at 4:56

2 Answers 2


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}$.

  • 3
    $\begingroup$ Beat me to it, +1! Let me mention a couple additional sources which may be of interest, namely this survey by Enayat and this (sadly non-LaTeX) manuscript of Friedman. The former is a good summary of what interpretations are, and touches on ZF/PA a bit; the latter is more technical, but may still be worth looking at. $\endgroup$ Commented Sep 8, 2020 at 5:45
  • $\begingroup$ Thank you. Is there a definition that generalizes outside of first-order logic? Also, shouldn't "ZFC" and "ZF" be interchanged? $\endgroup$ Commented Sep 8, 2020 at 7:12
  • $\begingroup$ @AbhimanyuPallaviSudhir For the second question, yes, we can construct a structure of natural numbers without any help of axiom of choice. For the first question, I bet the answer is yes, but I am not sure. I have not seen any references that refer to interpretations outside of first-order logic. $\endgroup$
    – Hanul Jeon
    Commented Sep 8, 2020 at 7:16
  • $\begingroup$ @HanulJeon I meant in the line "an interpretation from ZFC to ZF". Shouldn't that be an interpretation from ZF to ZFC, since ZFC is stronger? Re:interpretation -- I was asking in reference to stuff like "first-order set theory is stronger than second-order arithmetic". $\endgroup$ Commented Sep 8, 2020 at 7:23
  • $\begingroup$ @Abhimanyu Aha, I was confused. The identity interpretation (which sends a formula to itself) is an interpretation from ZF to ZFC (so ZF and ZFC are mutually interpretable.) $\endgroup$
    – Hanul Jeon
    Commented Sep 8, 2020 at 7:38

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

  • $\begingroup$ Note that the sole disadvantage of this definition of interpretation is that one is restricted to countable languages, because we cannot talk about a computable translation over an uncountable language. $\endgroup$
    – user21820
    Commented Sep 8, 2020 at 17:42
  • $\begingroup$ Do you mean countable or r.e.? $\endgroup$
    – tomasz
    Commented Sep 8, 2020 at 17:49
  • 1
    $\begingroup$ @tomasz: Countable. $Th(ℕ)$ can be viewed as an uncomputable formal system that interprets PA. The point of my comment was just that "computable translation" only makes sense for countable domain. $\endgroup$
    – user21820
    Commented Sep 8, 2020 at 18:33

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .