The transitive-model consistency-strength gap

Transitive ZF models have standard arithmetic and proof codes: A transitive set model M of ZF has the real omega and natural arithmetic, and all finite natural-number syntax and proof codes. Every fixed arithmetic predicate on these codes agrees with ambient arithmetic. If M models ZFC, it satisfies the standard Con(ZFC).

Models and consistency for countable theories: In external ZF, an explicitly countable sentence theory is consistent iff it has a nonempty set model, and iff it has a model with carrier injecting into $\omega$. For an effective presentation, external consistency agrees with the truth of its certified Con formula in standard arithmetic. No transitivity or external well-foundedness of a model follows.

ZF has an effective standard arithmetic interpretation: ZF and ZFC have effective axiom presentations and an interpretation of PA on the actual internally defined $\omega$, using von Neumann zero/successor and recursively defined addition/multiplication. For their standard presentations the arithmetic proof constructors and translations needed for D1–D3 are verifiable in that interpretation. AC is unnecessary for the PA interpretation; ZFC adds one encoded Choice sentence.

Second incompleteness for standard provability: If T is consistent and has the arithmetic/interpretation and D1–D3 hypotheses above for the displayed standard predicate, T does not prove its displayed $\mathrm{Con}(T)$. Numeralwise correctness of an arbitrary predicate is insufficient.

Deduction theorem for sentence assumptions: In ZF, for a sentence theory $T$, a sentence $\sigma$ and any formula $\theta$,

$T\cup \{\sigma \}⊢\theta ⟺T⊢\sigma \to \theta \mathrm{.}$

The forward transformation also works for an open discharged assumption $\sigma$ provided every variable generalized or existentially eliminated in the given derivation is absent from $\mathrm{FV}(\sigma )$; the other assumptions remain sentences.