Theory of arithmetic equiconsistent with ZF

Question

I am wondering if there is an extension of PA by additional axioms, but without extending its language, which is equiconsistent with ZF. In particular I am wondering if there is a relatively short axiom we can add to PA to gain equiconsistency with ZF without leaving the language of PA and using set theory.

Answer 1

The simplest approach would be the following. Given a primitively recursively axiomatized theory $T$ (ZF is such a theory, and indeed by Craig's trick every r.e. axiomatizable theory is equivalent to such), let PA[$T$] be the theory consisting of PA together with, for each $n$, the axiom

$\theta^T_n$: "If there is a proof of $\perp$ in $T$ using fewer than $n$ symbols, then $0=1$."

It's easy to show that (if $T$ proves $Con(PA)$ - which is the case when $T=ZF$) then PA proves that PA$[T]$ is consistent iff $T$ is consistent.

(Note that PA + $Con(ZFC)$ is too strong, so we really do need to be a bit fiddly here.)

---

But that's probably not satisfying, partly because it's "clearly cheating" and also because it's not a single principle. Is there anything better?

Harvey Friedman has developed a many-pronged program around finding "natural combinatorial" principles of high consistency strength (e.g. well beyond ZF) - see e.g. his manuscript on Boolean Relation Theory or his many postings on the Foundations of Mathematics mailing list (which has searchable archives). Friedman is on record as arguing that the principles he has isolated are natural, compelling, and easily comprehensible; I personally largely disagree, but I'd certainly agree that they're much more natural that I would expect and reveal surprising facts about combinatorial complexity and that his results are incredibly striking.

That said, Friedman's goal has always (to the best of my knowledge) been to locate "natural" statements of highest consistency strength possible (well, not quite :P) and to show that the large cardinal hierarchies form the right tool for gauging the consistency strength of such. So he's focused more on principles corresponding to large cardinals beyond ZFC and I don't know of any that have consistency strength exactly that of ZF.