Return to Answer

On the one hand, it is easy to see that $\pa$ interprets $T$ using Ackermann’s interpretation ($n\in x$ iff the $n$th bit in the binary expansion of $x$ is $1$), as mentioned in Joel’s answer.

For an interpretation of $\pa$ in $T$, it is easiest to make a short detour through classical results (by now folklore) on finite set theory, due to Mycielski and Sochor (apparently). $\pa$ is bi-interpretable with the theory $\zff$ of finite sets, which can be axiomatized by

Now, I claim that $T$ proves $\zffm$. Axioms 1–3 are straightforward. For 4, first note that $T$ proves that every element $x$ other than the minimal element $0$ has a predecessor (as $\{y:y<x\}$ has a maximal element) and successor $S(x)$ (in particular, as mentioned in paste bee’s answer, there is no largest element, as otherwise $\{x:x\notin x\}$ would exist, leading to Russell’s paradox). Using Sets and Well-founedness, $T$ proves order induction $$\forall x\,\bigl(\forall y<x\,\phi(y)\to\phi(x)\bigr)\to\forall x\,\phi(x),$$ which together with predecessor implies usual induction $$\phi(0)\land\forall x\,\bigl(\phi(x)\to\phi(S(x))\bigr)\to\forall x\,\phi(x).$$ Let $\|x\|<n$ denote $\forall y\in x\,y<n$. Then given a formula $\phi(x)$, $T$ proves the formula $\psi(n)\equiv$ $$\phi(\varnothing)\land\forall x,y\,\bigl(\phi(x)\to\phi(x\cup\{y\})\bigr)\to\forall x\,\bigl(\|x\|<n\to\phi(x)\bigr)$$ by induction on $n$: if $\|x\|<0$, then $x=\varnothing$, which satisfies $\phi$ by the premise. Assuming $\psi(n)$, if $\|x\|<S(n)$, then either $\|x\|<n$ and $\phi(x)$ holds by the induction hypothesis; or $n\in x$ and $x'=x\smallsetminus\{n\}$ satisfies $\|x'\|<n$, thus $\phi(x')$ by the induction hypothesis, thus $\phi(x'\cup\{n\})$ using the premise, i.e., $\phi(x)$. Then $\forall n\,\psi(n)$ implies 4 as every $x$ satisfies $\|x\|<n$ for some $n$ using Finiteness.

On the one hand, it is easy to see that $\pa$ interprets $T$ using Ackermann’s interpretation ($n\in x$ iff the $n$th bit in the binary expansion of $x$ is $1$), as mentioned in Joel’s answer.

For an interpretation of $\pa$ in $T$, it is easiest to make a short detour through classical results (by now folklore) on finite set theory, due to Mycielski, Vopěnka, and Sochor (apparently). $\pa$ is bi-interpretable with the theory $\zff$ of finite sets, which can be axiomatized by

Now, I claim that $T$ proves $\zffm$. Axioms 1–3 are straightforward. For 4, first note that $T$ proves that every element $x$ other than the minimal element $0$ has a predecessor (as $\{y:y<x\}$ has a maximal element) and successor $S(x)$ (in particular, as mentioned in paste bee’s answer, there is no largest element, as otherwise $\{x:x\notin x\}$ would exist, leading to Russell’s paradox). Using Sets and Well-founedness, $T$ proves order induction $$\forall x\,\bigl(\forall y<x\,\phi(y)\to\phi(x)\bigr)\to\forall x\,\phi(x),$$ which together with predecessor implies usual induction $$\phi(0)\land\forall x\,\bigl(\phi(x)\to\phi(S(x))\bigr)\to\forall x\,\phi(x).$$ Let $\|x\|<n$ denote $\forall y\in x\,y<n$. Then given a formula $\phi(x)$, $T$ proves the formula $\psi(n)\equiv$ $$\phi(\varnothing)\land\forall x,y\,\bigl(\phi(x)\to\phi(x\cup\{y\})\bigr)\to\forall x\,\bigl(\|x\|<n\to\phi(x)\bigr)$$ by induction on $n$: if $\|x\|<0$, then $x=\varnothing$, which satisfies $\phi$ by the premise. Assuming $\psi(n)$, if $\|x\|<S(n)$, then either $\|x\|<n$ and $\phi(x)$ holds by the induction hypothesis; or $n\in x$ and $x'=x\smallsetminus\{n\}$ satisfies $\|x'\|<n$, thus $\phi(x')$ by the induction hypothesis, thus $\phi(x'\cup\{n\})$ using the premise, i.e., $\phi(x)$. Then $\forall n\,\psi(n)$ implies 4 as every $x$ satisfies $\|x\|<n$ for some $n$ using Finiteness.

For an interpretation of $\pa$ in $T$, it is easiest to make a short detour through classical results on finite set theory by Mostowski (and if something I mention is not due to Mostowski, it is in the works of Sochor). $\pa$ is bi-interpretable with the theory $\zff$ of finite sets, which can be axiomatized by

Moreover, the theory $\zffm$ axiomatized by 1–4 interprets $\zff$ (hence $\pa$), namely it proves axioms of $\zff$ relativized to the class WF of hereditarily well-founded sets: $x$ is in WF iff there is a transitive set $y\supseteq x$ such that every nonempty subset of $y$ has an $\in$-minimal element. (It is a longish but straightforward exercise to show that $\zffm$ proves all the usual axioms of $\def\zfc{\mathsf{ZFC}}\zfc$ except infinity and foundation; some of these may be useful for verification of this interpretation.) (NB: In recent literature stemming from a rediscovery of some of Mostowski’s results, the notation $\zff$ is used for a weaker theory that only has $\zfc$-style foundation axiom in place of $\in$-induction, and our $\zff$ is denoted $\zff+\mathsf{TC}$ or the like. I will keep the notation $\zff$ for the stronger theory as I have no use for the weaker one in my answer.)

Now, I claim that $T$ proves $\zffm$. Axioms 1–3 are straightforward. For 4, first note that $T$ proves that every nonminimal element has a predecessor (as the set of strictly smaller elements has a maximal element), and (using Sets and Well-founedness) order induction $\forall x\,\bigl(\forall y<x\,\phi(y)\to\phi(x)\bigr)\to\forall x\,\phi(x)$, which together imply usual induction $$\phi(0)\land\forall x,y\,\bigl(\phi(x)\land S(x,y)\to\phi(y)\bigr)\to\forall x\,\phi(x),$$ where $0$ is the smallest element, and $S(x,y)$ iff $y$ is the successor of $x$. Then assuming $$\phi(\varnothing)\land\forall x,y\,\bigl(\phi(x)\to\phi(x\cup\{y\})\bigr),$$ we can prove $$\forall x\,(\forall y\in x\,y\le n\to\phi(x))$$ by induction on $n$, which implies $\forall x\,\phi(x)$ using Finiteness.

For an interpretation of $\pa$ in $T$, it is easiest to make a short detour through classical results (by now folklore) on finite set theory, due to Mycielski and Sochor (apparently). $\pa$ is bi-interpretable with the theory $\zff$ of finite sets, which can be axiomatized by

Moreover, the theory $\zffm$ axiomatized by 1–4 interprets $\zff$ (hence $\pa$), namely it proves axioms of $\zff$ relativized to the class WF of hereditarily well-founded sets: $x$ is in WF iff there is a transitive set $y\supseteq x$ such that every nonempty subset of $y$ has an $\in$-minimal element. (It is a longish but straightforward exercise to show that $\zffm$ proves all the usual axioms of $\def\zfc{\mathsf{ZFC}}\zfc$ except infinity and foundation; some of these may be useful for verification of this interpretation.) (NB: In recent literature stemming from a rediscovery of some of these results, the notation $\zff$ is used for a weaker theory that only has $\zfc$-style foundation axiom in place of $\in$-induction, and our $\zff$ is denoted $\zff+\mathsf{TC}$ or the like. I will keep the notation $\zff$ for the stronger theory as I have no use for the weaker one in my answer.)

Now, I claim that $T$ proves $\zffm$. Axioms 1–3 are straightforward. For 4, first note that $T$ proves that every element $x$ other than the minimal element $0$ has a predecessor (as $\{y:y<x\}$ has a maximal element) and successor $S(x)$ (in particular, as mentioned in paste bee’s answer, there is no largest element, as otherwise $\{x:x\notin x\}$ would exist, leading to Russell’s paradox). Using Sets and Well-founedness, $T$ proves order induction $$\forall x\,\bigl(\forall y<x\,\phi(y)\to\phi(x)\bigr)\to\forall x\,\phi(x),$$ which together with predecessor implies usual induction $$\phi(0)\land\forall x\,\bigl(\phi(x)\to\phi(S(x))\bigr)\to\forall x\,\phi(x).$$ Let $\|x\|<n$ denote $\forall y\in x\,y<n$. Then given a formula $\phi(x)$, $T$ proves the formula $\psi(n)\equiv$ $$\phi(\varnothing)\land\forall x,y\,\bigl(\phi(x)\to\phi(x\cup\{y\})\bigr)\to\forall x\,\bigl(\|x\|<n\to\phi(x)\bigr)$$ by induction on $n$: if $\|x\|<0$, then $x=\varnothing$, which satisfies $\phi$ by the premise. Assuming $\psi(n)$, if $\|x\|<S(n)$, then either $\|x\|<n$ and $\phi(x)$ holds by the induction hypothesis; or $n\in x$ and $x'=x\smallsetminus\{n\}$ satisfies $\|x'\|<n$, thus $\phi(x')$ by the induction hypothesis, thus $\phi(x'\cup\{n\})$ using the premise, i.e., $\phi(x)$. Then $\forall n\,\psi(n)$ implies 4 as every $x$ satisfies $\|x\|<n$ for some $n$ using Finiteness.

Note that (1) alone is not enough to make the theory bi-interpretable with $\pa$, as $\N_\sigma\models(1)$ whenever $\sigma$ satisfies $\sigma(x)<2^x$ for all $x\in\N$, thus the argument above still applies.