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{\leftrigh...