How does (ZFC-Infinity+"There is no infinite set") compare with PA?
Solution 1:
This started as a rather long comment on Asaf's answer, and grew into an answer of its own:
Informally, $T$ interprets $S$ means that there is a procedure for associating structures $\mathcal N$ in the language of $S$ to structures $\mathcal M$ in the language of $T$ in such a way that if $\mathcal M$ is a model of $T$, then $\mathcal N$ is a model of $S$.
Let's be a bit more precise, and do this more syntactically to reduce the requirements of the metatheory: One can take "the theory $T$ interprets the theory $S$" to mean that there is
A map $i$ that assigns formulas in the language of $T$ to the symbols of the language $\mathcal L$ of $S$, and
A formula ${\rm Dom}(x)$ in the language of $T$,
with the following properties: We can extend $i$ to all $\mathcal L$-formulas recursively: $i(\phi\land\psi)=i(\phi)\land i(\psi)$, etc, and $i(\forall x\phi)=\forall x({\rm Dom}(x)\to i(\phi))$. It then holds that $T$ proves
- $\exists x\,{\rm Dom}(x)$, and
- $i(\phi)$ for each axiom $\phi$ of $S$ (including the axioms of first-order logic).
Here, $T,S$ are taken to be recursive, and so is $i$.
If the above happens, then we can see $i$ as a strong witness to the fact that the consistency of $T$ implies the consistency of $S$.
Two theories are mutually interpretable iff each one interprets the other. By the above, this is a strong version of the statement that they are equiconsistent.
Two theories are bi-interpretable iff they are mutually interpretable, and in fact, the interpretations $i$ from $T$ is $S$ and $j$ from $S$ in $T$ can be taken to be "inverses" of each other, in the sense that $T$ proves that $\phi$ and $j(i(\phi))$ are equivalent for each $\phi$ in the language of $T$, and similarly for $S$, $\psi$ and $i(j(\psi))$. In a sense, two theories that are bi-interpretable are very much "the same", only differing in their presentation.
We can then show that $\mathsf{PA}$ and $\mathsf{ZFfin}$ are bi-interpretable, where $\mathsf{ZFfin}$ is the variant of $\mathsf{ZF}$ resulting from replacing the axiom of infinity with its negation, and where foundation is stated as the axiom scheme of $\epsilon$-induction.
If we do not take the precaution of stating foundation this way, then the resulting theory $\mathsf{ZFfin}'$ is mutually interpretable with $\mathsf{PA}$, but it is not clear whether they are bi-interpretable, see below for this. (Similar issues, curiously, occur with NFU and appropriate fragments of set theory.) The problem is related to the existence of transitive closures, see this answer for more details.
The standard interpretation of $\mathsf{ZFfin}$ inside $\mathsf{PA}$ goes by defining $n\mathrel E m$ iff, writing $m$ in base $2$, the $n$th number from the right is $1$. That is, $m=(2k+1)2^n+s$ for some $k$ and some $s<2^n$. This is definable inside $\mathsf{PA}$, see this answer. This interpretation goes back to Ackermann:
Wilhelm Ackermann. Die Widerspruchsfreiheit der allgemeinen Mengenlehre, Math. Ann. 114 (1937), 305–315.
In the other direction, the interpretation goes by realizing that in $\mathsf{ZFfin}$ we can still define $\omega$ and ordinal arithmetic, and the result is a model of $\mathsf{PA}$. But this is not the inverse. To obtain the inverse, we work in $\mathsf{ZFfin}$, and compose this with a definable bijection $p:V\to\mathsf{ORD}$, namely $$ p(x)=\sum \{2^{p(y)}\mid y\in x\}. $$ (Of course, $V$ stands here for "$V_\omega$", the universe, and $\mathsf{ORD}$ stands for "$\omega$".) The paper listed here explains all this and provides additional references. This inverse interpretation is due to Mycielski, who published it in Russian:
Jan Mycielski. The definition of arithmetic operations in the Ackermann model. Algebra i Logika Sem. 3 (5-6), 1964, 64–65. MR0177876 (31 #2134).
(Thanks to Ali Enayat for the reference.) Mycielski's result remained "hidden" until attention was drawn to it in the survey
Richard Kaye and Tin Lok Wong. On interpretations of arithmetic and set theory. Notre Dame Journal of Formal Logic 48 (4), (2007), 497–510. MR2357524 (2008i:03075).
On the difference between mutual interpretability and bi-interpretability, see this nice post by Ali Enayat to the FOM list. Ali shows there that $\mathsf{ZF}$ and $\mathsf{ZFC}$, which are obviously mutually interpretable, are not bi-interpretable. The proof goes by noticing that if $T$ and $S$ are bi-interpretable, then the class of groups arising as ${\rm Aut}(\mathcal M)$ for $\mathcal M\models T$ coincides with the class of groups of the form ${\rm Aut}(\mathcal N)$ for $\mathcal N\models S$.
However, $\mathsf{ZF}$ admits a model with an automorphism of order $2$, and this is not possible for $\mathsf{ZFC}$. (Additional details are given at the link.)
This naturally leads to the question of whether $\mathsf{ZFfin}'$ and $\mathsf{PA}$ (or, equivalently, $\mathsf{ZFfin}$) are bi-interpretable, that is, whether a more clever interpretation than Ackermann's may get rid of the issues that forced us to adopt $\epsilon$-induction.
That this is not the case, meaning, the theories are mutually interpretable, but not bi-interpretable, was shown recently in
Ali Enayat, James H. Schmerl, and Albert Visser. $\omega$-models of finite set theory. In Set theory, arithmetic, and foundations of mathematics: theorems, philosophies, Juliette Kennedy, and Roman Kossak, eds. Lect. Notes Log., vol. 36, Assoc. Symbol. Logic, La Jolla, CA, 2011, pp. 43–65. MR2882651 (2012m:03132).
In fact, in Theorem 5.1, they show that $\mathsf{ZFfin}'$ and $\mathsf{PA}$ are not even sententially equivalent. This is a weaker notion than bi-interpretability:
Recall that if we have an interpretation $i$ from $T$ in $S$, then to each model $\mathcal M$ of $S$ we associate a model $i(\mathcal M)$ of $T$. That $T$ and $S$ are bi-interpretable gives us interpretations $i$ from $T$ in $S$, and $j$ from $S$ in $T$ such that for any model $\mathcal M$ of $S$, the model $j(i(\mathcal M))$ is isomorphic to $\mathcal M$, and for any model $\mathcal N$ of $T$, the model $i(j(\mathcal N))$ is isomorphic to $\mathcal N$.
We say that $T$ and $S$ are sententially equivalent when the interpretations $i$ and $j$ can be chosen to satisfy the weaker demand than $i(j(\mathcal N))$ and $\mathcal N$ are elementarily equivalent, and similarly for $j(i(\mathcal M))$ and $\mathcal M$.
Their proof that this property fails for $\mathsf{PA}$ and $\mathsf{ZFfin}'$ ultimately traces back to the fact that no arithmetically definable model of $\mathsf{PA}$ that is non-standard can be elementarily equivalent to the standard model. This is a result of Dana Scott. On the other hand, there are many arithmetically definable $\omega$-models of $\mathsf{ZFfin}'$. (This answer illustrates a very general method for producing such examples; further details can be seen in the Enayat-Schmerl-Visser paper.)
Solution 2:
You are correct. Replacing the infinity axiom with its negation gives you the same strength as PA. The theories are bi-interpretable.
See Richard Dore's wonderful answer: Does finite math need the axiom of infinity? (Mathoverflow).