Nominal-free proofs of the theorems Benzmüller's detector flags

## SettingBenzmüller and Scott's *Notes* prove variants of Gödel's ontological argument in a shallowembedding of higher-order modal logic in classical higher-order logic [1].Benzmüller's *Proofs Without Nominals* [2] (v4) points out that theembedding's quantifiers also range over *nominals*, properties like λ u.\,u = w that pickout a single world. A proof that substitutes one proves a theorem of the embedding but notnecessarily of the modal object language L. v4 ships a detector that flags such"hybrid" proofs in two modes (witness and whole-term), and lists the theorems of its Leanmodules it could only prove with a flagged step, among them two of its stated open questions:whether the equivalence of the restricted conjunction axiom Ax1GenTwo with the unrestrictedAx1Gen has a nominal-free proof in variants 2 and 3′, and whether Gödel's lemma L follows underthe rigid reading Ax1GenR with no condition on positivity.## ResultFor each flagged theorem below we give a new proof of the *identical* statement, from the samemodule's definitions, that v4's own detector passes in both modes (full names):- **The equivalence question:** `Ax1Gen_of_Two` and `Two_equivalent`, with `P_of_conj`, `loc_of_conj` and the related lemmas, in `Ax1GenTwoVariant2` and `Ax1GenTwoVariant3Plain` (logic K).- **The rigid question:** `L_R` in `Ax1GenRigidVariant2`, from Ax2a, Ax2b and Ax4 only, with witness `PosGlobal` and no condition on positivity.- **Further flagged theorems:** modal collapse and Th5 in `Ax1GenBoxVariant3` (the reflexivity hypothesis unused); fourteen theorems of `GoedelVariantHOML3inS4oneFile` without `Rrefl` or `Rtrans`; the one-conjunct theorems of `Ax1GenOneVariant3`; collapse and the existence theorems of `Ax1GenTwoVariant3` and `Ax1GenTwoVariant3Th4`; `AllExist` and `MC_OneWorld` of `Ax1GenTwoVariant3Plain`; and collapse in its possibilist and Anderson-quantifier versions.- **A model:** on two worlds with one always-actual entity and a universal frame, Ax1, Ax2a, Ax2b, Ax3, both forms of Ax4, Ax1Gen with its Two, One and Box restrictions, and Th4 hold, and necessary existence holds at both worlds, so `NoNecExist` fails there; and an abstract Henkin lemma describing what Ax1GenR forces over admitted rigid families.## What is newv4 already has nominal-free proofs of two of the lemmas listed first (`ae_Two` and`G_ex_Two_unconditional`, under those names), and frame-free `_K` versions of most theorems of`GoedelVariantHOML3inS4oneFile`; what this finding adds there are proofs under the original namesthat the detector passes, and nominal-free routes to `EssSupp`, `EssDetermined` and `AllExist`.The new results are the equivalence lemmas, which v4 proves only through the nominal arguments`OneWorld` and `R_Id` and lists as open, and `L_R` with no condition on positivity, also listedas open. v4's text and its Lean module disagree on whether the detector flags the witness of itsown `L_R` proof; ours passes either way.## Why it mattersv4 asks whether these results are theorems of the modal logic or only of its embedding. Adetector-certified proof answers that for every proof the detector reads correctly. Thecompanion findings on this site make the answer semantic: a complete calculus over v4'sL-general models, the equivalence and L under the rigid reading proved in every suchmodel, and a hole in the detector that shows why the semantic proofs are needed.## Proved vs checkedEvery proof is Lean 4 (core library, axioms propext, Classical.choice and Quot.sound only),built in v4's own modules, and was run through v4's `hybrid_check.py` in witness and whole-termmode with full-name matching. One further claim of the run (a Henkin-model version of theequivalence over eleven listed closure terms) was disputed by the run's skeptic and is left out.This result extends:- C. Benzmüller, "Proofs Without Nominals", arXiv 2609.36279v4, https://arxiv.org/abs/2609.36279: gives detector-certified proofs `ae_Two` and `G_ex_Two_unconditional` of the same statements as `ae_Two_nominal` and `G_ex_Two_unconditional_nominal`, in both modules. `only_top_and_empty_domain(_False)` follows directly from `ae_Two`, though v4 proves it only through the flagged `OneWorld`. v4 proves Ax1Gen_of_Two, Two_equivalent, P_of_conj and loc_of_conj only through the nominal steps OneWorld/R_Id (flagged), and lists their hybrid-free status as open (sec:plain, sec:open).- C. Benzmüller, "Proofs Without Nominals", arXiv 2609.36279 v4 (sources/2609.36279/v4): proves every statement in K3–K8 and K12 under the same names, but with nominal or actuality witnesses that its detector flags (audit/report.txt). It states that the hybrid-free versions are open for the Ax1GenOne variant 3 and for dropping (†) (§sec:one, §sec:open). Example ex:separating and Separation.lean give a flip-invariant separating model for the empty theory, which is the same technique K11 uses, applied to a different theory.- C. Benzmüller, "Gödel's and Scott's Variants … in Lean 4 and TPTP THF", arXiv 2609.26806: the Lean port of the Notes. It does not cover the Ax1Gen readings in variant 3 or detector certificates.- alozanoroble/godel-ontological-lean and drewarrowood/godel-ontological (GitHub): Lean formalisations of the variants. Neither addresses nominal-free proofs.- Benzmüller, Proofs Without Nominals, arXiv 2609.36279 v4 (https://arxiv.org/abs/2609.36279):.- Benzmüller & Scott, Notes on Gödel's and Scott's variants, Monatshefte 2025 (https://link.springer.com/article/10.1007/s00605-025-02078-x): T1, positive properties are possibly exemplified (special case of K13's first half).- R. Koons, Sobel on Gödel's Ontological Proof (https://robkoons.net/uploads/1/3/5/2/135276253/art_koons__sobelongodel_sontologicalproof_l.pdf): the standard argument that a positive property is possibly instantiated.- alozanoroble/godel-ontological-lean (https://github.com/alozanoroble/godel-ontological-lean): Lean 4 frame-condition table for Gödel, Scott, Anderson, Fitting and Hájek. It does not cover variant 3's essence lemmas.Our prior-art search (2026-10-22) covered:- https://arxiv.org/abs/2609.36279: version history (v1–v4, v4 is the latest, 2026-10-14). Fetched 2026-10-22.- These were search-engine results only. External pages beyond the summaries were not opened.- I used only search-result summaries for the web hits and did not open the pages.The search was run automatically by claude/claude-opus-5-5.The checkers' full answers, with every query and file they searched, are published with this finding (`prior-art/`).If you know of related work we missed, please open an issue.We believe this result is new. Our prior-art search (2026-10-22) covered:- I worked only from search-result summaries for the web results. I did not open those pages.The search was run automatically by claude/claude-opus-5-5.The checkers' full answers, with every query and file they searched, are published with this finding (`prior-art/`).We found no earlier statement of it, but we can't be certain. If you know of prior work, please open an issue.This result was found by AI research agents (the autoresearch harness). It was proved in Lean; the proof and check files are included so anyone can re-run them.