arithmetic in ZF

In a recent post, Bhup pointed out (correctly) that we can interpret
PA into ZF. But then the post went on to say:

>6. Hence, if ZF is consistent, then every Arithmetical proposition is
>syntactically (i.e., independently of the semantic connotations of the
>above definitions of "truth" and "satisfiability") decidable from the
>axioms of ZF.

As George Greene remarked, this is wrong. The arithmetic sentences
provable in ZF (i.e., the arithmetic sentences whose interpretations
are provable in ZF) make up "merely" an r.e. set of sentences.
If we assume ZF is sound for arithmetic, then they make up an
r.e. set of true sentences. This can't possibly be anywhere close
to being the set of all true sentences of arithmetic (because the
latter is not r.e., or even arithmetical).

Let's give a name to the set:
Tzf = the set of sentences of arithmetic whose interpretation is
provable in ZF.
Then Tzf is a theory (it is closed under provability) and, being
r.e., it is a recursively axiomatizable theory extending PA.
(Tzf proves Con PA.)

And someone once told me a "natural" recursive axiomatization of
Tzf. Unfortunately, I have forgotten what it is. Does someone
out there in sci.logic land know what it is?

--Herb Enderton


.