Is this theory synonymous with PA?

Question

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

Answer 1

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

Answer 2

Emil Jeřábek has already provided a detailed proof to show that the proposed theory $T$ is 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$.

Answer 3

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.

Answer 4

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.