Gödel's lemma L under the rigid reading, with no condition on positivity

## SettingGödel's lemma L says that a God-like being's property G is positive, $P\,G$. InBenzmüller's *Proofs Without Nominals* [1] (v4, sec:rigid), theconjunction axiom Ax1Gen is read *rigidly*: it applies only to sets of properties given byconditions formed in the object language L, so Ax1GenR is a schema overL-conditions. v4 asks whether L follows under this reading with no condition onpositivity. The finding *Nominal-free proofs* on this site gives a detector-certified proof inv4's module `Ax1GenRigidVariant2`; this one proves the statement over v4's semantics.## Result- **L under the rigid reading.** In every v4 L-general model with nonempty individuals where the variant-2 axioms Ax2a, Ax2b, Ax4 and the instance of Ax1GenR for the set of globally positive properties \ψ Pψ=\ hold at every world, $P\,G$ holds at every world. The proof is a derivation in the certified deep calculus of the companion finding, so it holds by that calculus's soundness theorem, with the deep axioms matched clause by clause to the Lean module.- **The schema reading is faithful.** In the full structure on any frame, actuality and positivity, if the rigid Ax1GenR holds for every set of properties then every deep instance Ax1GenR\,c, for c a rigid L-condition (equations under connectives and carrier quantifiers), holds at every world.- **The instance is needed.** Ax2a, Ax2b and Ax4 alone do not give $P\,G$: in a full S5 model with three worlds and one entity, where Pφ holds iff φ holds of the entity at two or more worlds, they hold while $P\,G$ and the Ax1GenR instance fail at every world.## Prior workv4 derives L under the rigid reading in two ways: through a hybrid witness that its detectorflags, and from the rigidly positive properties under a proviso that it shows does not followfrom the axioms (`L_R_rigidpos`). The result here needs neither. The faithfulness lemma followsthe deep–shallow method of Benzmüller and Kirchner for other logics.## Why it mattersThis answers v4's rigid-reading question semantically and with no condition on positivity: theone instance of the schema at the globally positive properties is enough, and without it theother axioms do not suffice.## Proved vs checkedThe first two claims are Lean 4 theorems (core library, axioms propext, Classical.choice andQuot.sound only), kernel-checked in the library build. The third is an explicit finite model,checked by a script (`checks/K2-lr_instance_needed.py`, re-run at publication) and re-derived bythe run's skeptic, but not in Lean; its status is *derived*.This result extends:- Benzmüller, "Proofs Without Nominals", arXiv 2609.36279 v4, §sec:rigid: Ax1GenR. It has L_R in K from Ax2a and Ax2b via the hybrid witness @_w P. L_R_rigidpos derives L from {ψ ∣ A(Pψ)} only under rigid positivity. It leaves open the case without that condition, which is the case K1 addresses. prop:lgeneral gives shallow soundness over 𝓛-general models.- Benzmüller & Scott, Notes (Monatshefte 2025), and Benzmüller, arXiv 2609.26806: L (P G) from the world-dependent Ax1Gen, by the instance Φ = P.- Kanckos & Woltzenlogel Paleo, "Variants of Gödel's Ontological Proof in a Natural Deduction Calculus", Studia Logica 105 (2017): explicit derivations in a rigid higher-order modal logic, but with P G (A3) as an axiom, not derived from a conjunction schema.- Benzmüller & Woltzenlogel Paleo, arXiv 1308.4526: says A3 is derivable from Axiom 1 and D1 given infinitary conjunction. This is an informal remark, with no rigid schema and no general-model semantics.- Benzmüller, "Proofs Without Nominals", arXiv 2609.36279 (sources/2609.36279/v4/main.tex): defines rigid L-conditions (def:hybridfree) and Ax1GenR (sec:rigid). Instantiates Ax1GenR with the L-condition {ψ ∣ A(Pos ψ)} in the shallow embedding (`L_R_rigidpos`). Gives soundness over L-general and standard models (prop:lgeneral). Deep embedding only for the propositional part (Separation). No general deep-instance lemma.- Benzmüller & Kirchner, "Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness", arXiv 2609.07345 / AFP MSOinHOL: deep↔shallow faithfulness for MSO under standard (full) and Henkin readings, with comprehension. Same mechanism as K3, different logic.- Benzmüller & Kirchner, "First-Order Modal Logic in HOL…", arXiv 2607.10880: deep↔shallow faithfulness for first-order modal logic only (no quantification over properties or sets of properties).- Benzmüller, "Faithful Logic Embeddings in HOL — Deep and Shallow", arXiv 2502.19311 (CADE-30): the same for propositional modal logic.- Benzmüller, "A Comment on Modal Collapse and Ultrafilters", arXiv 2608.07578: names a deep embedding of higher-order modal logic as the natural setting for definability questions, i.e. future work.- drewarrowood/godel-ontological PR #1 (GitHub): tests a rigid-Φ repair of Ax1Gen in Lean through countermodels. Nothing on deep instances.Our prior-art search (2026-10-23) covered:- https://arxiv.org/abs/2609.36279 (versions v1–v4; v4 dated 2026-10-14 is latest), 2026-10-23The 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.This result was found by AI research agents (the autoresearch harness). It was partly proved in Lean (claims K1, K3) and partly checked by script (claims K2); the proof and check files are included so anyone can re-run them.