Is "PA has no non-standard models" consistent with ZF?

Question

I have seen several proofs that there exist nonstandard models of arithmetic, but they all seem to rely on the compactness theorem, which is not implied by ZF. So are there any proofs in ZF that there's exists a nonstandard model of PA? Tennenbaum's theorem, which states that every nonstandard model is uncomputable seems to hint at the possibility that there are models of ZF that contain no nonstandard models of PA.

Answer 1

No, ZF, without choice, suffices to prove that PA has nonstandard models. The reason is that PA is formalized in a countable first-order language. For such languages (indeed, for all first-order theories in well-orderable languages), the completeness theorem and therefore the compactness theorem are provable without choice.

To prove the completeness theorem for theories in a countable language, you can follow the usual Henkin completeness proof. The part of the proof that adds Henkin constants and the Henkin axioms that govern them needs no choice. The next step in the usual proof, namely extending the resulting theory to a complete theory, is usually done with Zorn's Lemma, but, in view of countability, we can use an ordinary induction instead. List all sentences in the language (including Henkin constants) in a sequence (indexed by the natural numbers). Go through this sequence, one sentence at a time, adding each sentence to your theory iff it is consistent with everything that's already in your theory. After a countable sequence of steps, you'll have a complete theory, and you can then use it to define a model just as in the usual proof.