[mo271]

depends-on #17

[TomZahavy]

Very nice result. Object-level PA ⊢ Halts(zf393) ↔ ¬Con(ZF) (and the same for zf_380) closes the "internalizing inside PA is separate" caveat in the Foundational Note. I reviewed the delta over #17. CI is green.

Correctness. The three new challenge theorems depend only on #17's trusted definitions, and this PR adds no new trusted definitions. Going through completeness (build the argument in an arbitrary PAModel via first-order PAM.ind1, then apply paProvable_iff_holdsIn_all_models) is mathematically fine. It also explains why these theorems are classical rather than in constructive.json; it might be worth saying that explicitly in the README.

Comments:

1. Inherits #17's audit/doc mismatch, and it's more visible here. The README "Classical" bullet lists paProvable_iff_holdsIn_all_models as audited via all.json/pa_semantics.json, but it isn't in Challenge.lean or any comparator config. This isn't a soundness gap, since the final PAProvable statements are audited directly. But completeness is now load-bearing, so please either audit it or fix the wording.

2. File layout (suggestion). PA/Zf393BackendInternal.lean, PA/Zf393ProgramInternal.lean, PA/Zf393SoundnessInternal.lean and PA/Zf380Internal.lean don't follow the existing Semantics/Zf393/{Backend,Program}.lean structure. Consider Semantics/PA/Zf393/{Backend,Program,Soundness}.lean and Semantics/PA/Zf380.lean.

3. Duplication (follow-up, non-blocking). Zf393ProgramInternal.lean (4k lines) largely mirrors Semantics/Zf393/Program.lean with ℕ generalised to PAM M. Is the plan to eventually derive the ℕ proofs as the M = ℕ instance? That would roughly halve the maintenance surface.

4. Options (nits):

   • set_option maxRecDepth 200000 is file-global in Zf393ProgramInternal.lean; prefer … in on the declarations that need it.
   • set_option linter.flexible false in (≈ l.3068) has precedent in the repo, but fixing the simp would be nicer.

5. Visibility (nit). Arithmetic.lean has ~231 theorems and only 29 private ones. That's consistent with the rest of Semantics/, but please mark one-off helpers private where possible.

6. Housekeeping:

   • The title has a typo ("equivalences some zf machines").
   • Please add a description: the three theorems, the completeness-based method, and why it's classical.
   • The branch conflicts with main in comparator/README.md.
   • Please retarget/rebase once #17 lands.

Happy to approve once #17 lands and item 1 is addressed. 2–5 are non-blocking.