Language: Mono-sorted first order logic with equality.

Extralogical Primitives: $<, \in$

Define: $x \leq y \iff x < y \lor x=y$

  • $\textbf{Well ordering: }\\\textit{Transitive:} \ x < y \land y < z \to x < z \\ \textit{Connective:} \ x \neq y \leftrightarrow (x < y \lor y < x) \\ \textit{Well founded:} \ \exists n \in x \to \exists n \in x \forall m \in x (n \leq m)$

  • $\textbf{Finiteness: }\exists n \in x \to \exists n \in x \forall m \in x (m \leq n)$

  • $\textbf{Sets: } \forall n \exists! x \forall m (m \in x \leftrightarrow m \leq n \land \phi)$, if $x$ is not free in formula $\phi$.

Is this theory synonymous with $\sf PA$?

  • $\begingroup$ Using the other axioms, you can simplify Finiteness to $\exists n\,\forall m\in x\,m<n$. $\endgroup$ Jan 5 at 6:39
  • $\begingroup$ @EmilJeřábek, but how to get rid of $\omega$? I thought this should be $\exists n \in x \forall m \in x \ m \leq n$. $\endgroup$ Jan 5 at 8:17
  • $\begingroup$ What $\omega$? There is no $\omega$ anywhere in the axioms. $\endgroup$ Jan 5 at 8:45
  • 1
    $\begingroup$ @EmilJeřábek Take $V_{\omega\cdot 2}$, and well-order it, first by rank and for sets of the same rank by an arbitrary well-ordering. This satisfies the well-ordering axioms, the simplified finiteness axiom ($x$ is larger than all of its elements), and the sets axiom (the resulting set has a rank at most one more than the rank of $n$, so it is in $V_{\omega\cdot 2}$), but not the original finiteness axiom (the set $\omega$ has no maximum element). $\endgroup$
    – paste bee
    Jan 5 at 8:46
  • $\begingroup$ Ah, I see. The argument I had in mind needs that every non-minimal element has a predecessor, and I didn’t realize this no longer follows from the simplified axiom. I guess that if it’s explicitly added, it’s not a simplifaction any more. $\endgroup$ Jan 5 at 8:53

4 Answers 4


$\def\pa{\mathsf{PA}}\def\zff{\mathsf{ZF_{fin}}}\def\zffm{\mathsf{ZF_{fin}^-}}$Your theory (let me denote it $T$ for the moment) is mutually interpretable with $\pa$, but it is not bi-interpretable with $\pa$, and a fortiori not synonymous.

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

  1. Extensionality

  2. Existence of $\varnothing$

  3. Existence of $x\cup\{y\}$ for all $x$ and $y$

  4. Induction: $\phi(\varnothing)\land\forall x,y\,\bigl(\phi(x)\to\phi(x\cup\{y\})\bigr)\to\forall x\,\phi(x)$

  5. $\in$-induction: $\forall x\,\bigl(\forall y\in x\,\phi(y)\to\phi(x)\bigr)\to\forall x\,\phi(x)$

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.

$\def\N{\mathbb N}$Finally, to show that $\pa$ is not bi-interpretable with $T$, the key observation is that $T$ has lots of nonisomorphic (and not elementarily equivalent) standard models. Here, I call a model $(M,<,\in)\models T$ standard if $(M,<)$ is well founded (necessarily of order-type $\omega$). For every permutation $\sigma\colon\N\to\N$, we have $\N_\sigma=(\N,<,\in_\sigma)\models T$, where $$n\in_\sigma x\iff\text{the $n$th bit of $\sigma(x)$ is $1$.}$$

Now, assume for contradiction that $F$ is an interpretation of $\pa$ in $T$ and $G$ is an interpretation of $T$ in $\pa$ such that $F\circ G$ is definably isomorphic to the identity self-interpretation of $T$. Fix permutations $\sigma\ne\tau$. Then $F$ induces models $\N_\sigma^F$ and $\N_\tau^F$ of $\pa$, and $G$ induces a copy of $\N_\sigma$ definable in $\N_\sigma^F$ and a copy of $\N_\tau$ definable in $\N^F_\tau$, using the same definitions. Since $\N_\sigma^F$ has full induction schema, it can define an embedding $f$ of the universe into the internal copy of $\N_\sigma$ such that $f(0)$ is the least element of $\N_\sigma$, and $f(n+1)$ is the successor (as computed in $\N_\sigma$) of $f(n)$. Since $f$ is an order embedding into a well-ordered set, its domain must be well ordered as well: that is, $\N_\sigma^F$ must be isomorphic to the standard model $\N$ of $\pa$.

The same argument applies to $\N_\tau^F$, thus in particular, $\N_\sigma^F\simeq\N_\tau^F$. But then their internal models of $T$, viz. $\N_\sigma$ and $\N_\tau$, must be isomorphic as well, as they are defined by the same formulas. This is a contradiction, as $\N_\sigma$ and $\N_\tau$ are not even elementarily equivalent (they disagree on some sentences of the form $\overline n\in\overline m$, where $\overline n$ denotes the $n$th least element according to $<$).

Note that we have used only one half of the definition of bi-interpretability, thus the argument above actually shows that $T$ is not an interpretation retract of $\pa$.

Let me add that in order to get a theory synonymous with $\pa$ (or equivalently, $\zff$), it is enough to extend $T$ with the two axioms $$\let\eq\leftrightarrow\begin{align} \tag1n\in x&\to n<x,\\ \tag2x<y&\eq\exists n\,\bigl(n\in y\land n\notin x\land\forall m>n\,(m\in x\eq m\in y)\bigr). \end{align}$$ (In fact, it is sufficient to keep only one implication (either one) of the outer bi-implication in (2); the other one then follows using axioms of $T$. On the other hand, it’s quite possible some of the axioms of $T$ can be simplified in the presence of (1) and (2).)

Since $T$ proves order induction, (1) ensures that the theory includes $\in$-induction, and therefore all of $\zff$. Then (2) ensures that $x<y$ is equivalent to an inductive definition in terms of $\in$ alone (coinciding with the usual order on $\omega$ lifted by Ackermann’s bijection between $\omega$ and $V_\omega$). Thus, the resulting theory is equivalent to an extension of $\zff$ by a definition.

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.

  • 1
    $\begingroup$ No, I mean the one that’s the outermost connective in the formula. The top of the parse tree. $\endgroup$ Jan 5 at 19:07
  • 1
    $\begingroup$ I am not aware of any work of Mostowski in relation to finite set theory, could it be that you meant Mycielski? He is the one who first proved (despite a conjecture of Beth to the contrary) that the arithmetical operations are definable in the Ackermann model, as indicated in the abstract, see: zbmath.org/0171.26403 $\endgroup$
    – Ali Enayat
    Jan 5 at 20:29
  • 1
    $\begingroup$ @AliEnayat Oh dear, yes, I meant Mycielski rather than Mostowski. Though now I see that his paper is rather short, and certainly does not include the concise axiomatization of $\mathsf{ZF_{fin}}$ by induction schemata. I’m not really sure who exactly discovered it; as an upper bound, it was common knowledge in the 1970s in Vopěnka’a group working on the Alternative Set Theory. I’ll tentatively attribute it to Sochor, who was behind the axiomatic foundations of AST. $\endgroup$ Jan 6 at 9:15
  • 1
    $\begingroup$ @ZuhairAl-Johar I’m not sure which part of the proof you didn’t understand, but I added a little more details. $\endgroup$ Jan 6 at 9:40
  • 1
    $\begingroup$ The earliest reference on an axiomatic development of finite set theory I know of is the following, some of the results of which are summarized in the preliminary section of the paper "$\omega$-models of set theory" referenced in my answer to this MO question: P. Vopěnka, Axiome der Theorie endlicher Mengen, Časopis Pro Pěstování Matematiky, vol.89 (1964), pp. 312–317. $\endgroup$
    – Ali Enayat
    Jan 6 at 10:28

Emil Jeřábek has already provided a detailed proof to show that the proposed theory $T$ in not bi-interpretable with $\mathsf{PA}$ (even though it is mutually interpretable with $\mathsf{PA}$).

The point of this answer is to completement Jeřábek's nice answer by indicating that the argument of Theorem 5.1 of the paper $\omega$-models of finite set theory (co-authored with Schmerl and Visser, available here) can be slightly fine-tuned to show the failure of bi-interpretability. At the bottom, the argument is close in spirit to Emil's.

More specifically, the fine-tuning needed in the proof of Theorem 5.1 of the aforementioned paper to conclude the failure of bi-interpretability, is to observe that, using Remark 4.10 of the same paper, there are (many) recursive models other than $V_{\omega}$ of $\mathsf{ZF_{fin}}$ that have a definable linear ordering of order-type $\omega$, and thus they satisfy the proposed theory $T$.


Here's the other half of the answer: an interpretation of PA in this theory.

If $a < b$ and $b < a$, then $a < a$, which by Connective implies $a \neq a$, which is a contradiction. So $<$ is asymmetric.

Consider an arbitrary number $n$. By the axiom of sets, the set of numbers that are less than or equal to $n$ exists (using a formula like $m = m$ as $\phi$), and by well-foundedness this has a minimum element $0$. For any number $k$, if $k < 0$, then $k < n$, so $k$ is in the set of numbers $\leq n$, and therefore $0 \leq k$ (by minimality of $0$ in the set), which is a contradiction. So $0 \leq k$ for all $k$.

Suppose that $n$ is the largest number. Then because $m \leq n$ for all $m$, we can, by Sets, construct the set of all numbers that are not elements of themselves. This is an element of itself iff it is not, which is a contradiction. So there is no largest number.

Since for any $n$ there is some $m > n$ (because $n$ cannot be the largest number), we can take the set of all numbers that are $\leq m$ and $> n$. This set is not empty, because $m$ is in it, so it has a minimum element $S(n)$. There is no number between $n$ and $S(n)$, because if there was it would be $< m$ and therefore in the set so $S(n)$ wouldn't be minimal. So every number has a successor.

For any two numbers $n,m$, the set $\{n,m\}$ exists. Suppose (wlog) that $n \leq m$. Then the set of numbers $\leq m$ that are either equal to n or equal to m contains both $n$ and $m$, since those are both less than $m$, and clearly doesn't contain anything else.

For two numbers $n,m$, define the pair $(n,m)$ to be $\{\{n\},\{n,m\}\}$, which exists by repeated applications of the above argument (constructing $\{n\}$ as $\{n,n\}$). If $(a,b) = (c,d)$, then either they both have only one element, in which case $a = b$, $c = d$, and $\{\{a\}\} = \{\{c\}\}$, which implies $a = c$ and therefore $b = d$; or they both have two elements (which implies $a \neq b$ and $c \neq d$), in which case $\{a\} = \{c\}$ (which implies $a = c$) and $\{a,b\}=\{c,d\}$ (which implies $b = d$); so either way, $a = c$ and $b = d$, so this is a pairing function.

Any number $n \neq 0$ is the successor of some other number. Take the set of numbers $\leq n$ that are less than n. This set is not empty because it contains $0$, so by finiteness, this set has a maximum element $m$. If $n < S(m)$, then $n$ is between $m$ and $S(m)$ which is impossible. If $S(m) < n$, then $S(m) < m$ by maximality of $m$ in the set of numbers less than $n$, which is impossible. So $n = S(m)$.

For any formula $\phi(n)$, if $\phi(0)$, and $\phi(n)$ implies $\phi(S(n))$ for all $n$, then $\phi(n)$ for all n. Suppose there is some number $k$ such that $\neg\phi(k)$. The set of numbers $\leq k$ for which $\phi$ is false is not empty (it contains $k$), so it has a minimum $x$. $x$ is not 0, because $\phi(0)$ and $\neg\phi(x)$, so it is the successor of some number $y$. If $\phi(y)$, then $\phi(S(y))$, but we know that isn't true. If $\neg\phi(y)$, then $x$ wasn't the minimum, because $y < x$. This is a contradiction.

Given number $n$ and $m$, the union of $n$ and $m$ exists: it is the set of numbers less than or equal to the maximum of the maximum element of $n$ and the maximum element of $m$, that are elements of either $n$ or $m$.

For a function $f$ (encoded as a formula $\phi(x,y)$ that represents $f(x) = y$), and numbers $n$ and $x$, there is a set $F_n$ with the properties that:

  1. $(0,x) \in F_n$
  2. For $k < n$, if $(k,y) \in F_n$, then $(S(k),f(y)) \in F_n$.
  3. For all $k \leq n$, there is a unique number $F_n(k)$ such that $(k,F_n(k)) \in F_n$.
  4. For all $k > n$ and all $y$, $(k,y) \notin F_n$.

For $n = 0$, $F_0 = \{(0,x)\}$. For $n = S(m)$, $F_n = F_m \cup \{(n,f(F_m(m)))\}$.

For any two sets $F_n$ and $F_m'$ satisfying these properties, $F_n(k) = F_m'(k)$ for all $k$, by induction: for $k = 0$, $F_n(0) = F_n'(0) = x$, and for $k = S(m)$, $F_n(k) = f(F_n(m)) = f(F_m'(m)) = F_m'(k)$.

Define $f^n(x)$ to be $F_n(x)$ for any $F_n$ (we know they all give the same answer). By property 1, $f^0(x) = x$, and by property 2, $f^{n+1}(x) = f(f^n(x))$.

Now we can define $n + m$ as $S^m(n)$, and $n \cdot m$ as $f^m(0)$ where $f(x) = x + n$. The axioms for the recursive definitions of $+$ and $\cdot$ follow immediately from the paragraph above.

Suppose that $S(n) = S(m)$, but $n \neq m$; wlog assume $n < m$. Then $S(n) \leq m$, but since $m < S(m)$, $S(n) < S(m)$, which is a contradiction. So $S$ is injective.

If $S(n) = 0$, then $n < 0$, which is a contradiction. So $0$ is not a successor.

I already proved that $0$ and successor exist, and induction, so that's all the axioms of PA.

  • 4
    $\begingroup$ This does not show the two theories are synonymous, as the question asks. (In fact, they are not.) Also, an interpretation of PA in the theory can be shown more easily by going through $\mathrm{ZF_{fin}}$. $\endgroup$ Jan 5 at 8:54
  • $\begingroup$ @paste bee, Thanks! This seemingly achieves mutual-interpretability with PA. I think bi-interpretability would need transitive closures or something like that, and from it we get to synonymy. $\endgroup$ Jan 5 at 9:08
  • $\begingroup$ @ZuhairAl-Johar Transitive closure won’t help much. What you really need is that $<$ agrees with the bitwise definition of $<$ in terms of $\in$ under the Ackermann interpretation. $\endgroup$ Jan 5 at 10:08
  • $\begingroup$ @EmilJeřábek, if we add an axiom that $x \in y \to x < y$. Would that work? $\endgroup$ Jan 5 at 11:52
  • 1
    $\begingroup$ @ZuhairAl-Johar Yes, but that does not say much more than that $T$ interprets PA. Whenever a theory $U$ faithfully interprets a theory $V$, there is an extension $U'$ of $U$ by definitions such that $V$ is synonymous with a fragment of $U'$. Namely, let $U'$ extend $U$ by definitions of all the primitive symbols of $V$ according to the given interpretation. (There are also broad conditions under which interpretability of $V$ in $U$ implies faithful interpretability; such theories $U$ are called trustworthy. E.g., your $T$ is trustworthy.) $\endgroup$ Jan 5 at 13:57

Let me give half an answer.

Specifically, we can interpret your theory in PA via the Ackermann encoding. Namely, in any model of PA, define $m\in x$ if and only if the $m$th bit of $x$ is $1$. This fulfills all your axioms.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.