Does PA prove that Con(PA) implies Con(ZF-I) and Con(NFU)?

Question

I read from many sources that PA and ZF-I (a suitable axiomatization of ZF minus Infinity plus its negation) are bi-interpretable, but is PA enough to prove that they are equiconsistent? Specifically is the following true? $\newcommand\t[1]{\textrm{#1}}$ $\def\imp{\rightarrow}$ $\def\eq{\leftrightarrow}$

$\t{PA} \vdash \t{Con}(\t{PA}) \eq \t{Con}(\t{ZF-I})$.   (Explicitly proven.)

I think so, but I'm not sure. Exercise IV.30 in this book asks to prove that the equiconsistency can be proven finitistically, but I don't know what exactly their "finitistic" means so I would just like confirmation.

Similarly, I read that consistency of PA implies NFU (New Foundations with Urelements), but I have never once saw any explicit mention of the meta-system needed for this result. Certainly it cannot itself be strong enough to prove Con(PA) otherwise the antecedent is redundant. So is PA enough? Specifically is the following true?

$\t{PA} \vdash \t{Con}(\t{PA}) \imp \t{Con}(\t{NFU})$.   (And if so, is there an explicit proof?)

To clarify, when I ask for explicit proofs I mean that there must be a clear deterministic procedure for obtaining such a proof, meaning that it must be completely constructive (finitistic and also not relying on the law of excluded middle; equivalent you should be able to show me how to construct a program that outputs such a proof).

I'm asking both questions together because I suspect the answer is the same, and also because the motivation for them were the same; I wanted to know how much we can prove using just PA.

Answer 1

There are syntactic interpretations of PA into ZF-I and of ZF-I into PA. For the purposes of equiconsistency, it does not matter whether these are inverses of each other, an issue that is discussed by Kaye and Wong in this paper. They are worried about something stronger than mere equiconsistency. I will assume we are talking about interpretations in their sense, however.

In a very standard way, the existence of the two interpretations allows us to show that

$\text{PRA} \vdash \text{Con(PA)} \leftrightarrow \text{Con(ZF-I)}$

Here PRA is primitive recursive arithmetic, a very weak theory of arithmetic. The key point is that the interpretation of a theory $S$ into a theory $T$ allows us to transfer an inconsistency in $S$ into an inconsistency in $T$, by merely manipulating the proof of the inconsistency in a primitive recursive manner.

That kind of syntactic manipulation can be carried out in PRA as long as the interpretation of $S$ into $T$ is sufficiently effective, that is, if all of the syntactic functions in the interpretation are primitive recursive. If we work with interpretations as defined in the paper of Kaye and Wong, this means that the function that interprets formulas of $S$ into formulas of $T$, and the function that produces $T$-proofs of the interpretations of axioms of $S$, must both be primitive recursive.

If $T$ and $S$ are effective theories, $T$ is syntactically interpretable in $S$, and $S$ is syntactically interpretable in $T$, and both of these interpretations are primitive recursive, then $\text{PRA} \vdash \text{Con(T)} \leftrightarrow \text{Con(S)}$.

It may help to also remember that every effective theory has a primitive recursive axiomatization, which we use to define the consistency sentence of that theory.