A complete calculus for the ℒ-general models of the ontological argument

## SettingBenzmüller's *Proofs Without Nominals* [1] (v4) judges proofs in theshallow embedding of higher-order modal logic against $\mathcal L$-*general models*: Henkin-stylemodels whose carriers are closed under the terms of the modal object language $\mathcal L$. ItsProposition prop:lgeneral gives soundness over these models for proofs meeting a *whole-term*condition; its Example ex:separating gives a sentence of $\mathcal L$,$\mathsf A\exists p.(\mathsf{Atom}\,p\wedge p)$, that the embedding proves but the conditionexcludes, formalised in its propositional part only. v4 leaves open whether its weaker *witnesscriterion* alone implies the condition, and whether a separating model exists for any of itsaxiom sets. This finding makes that semantics machine-checked.## Result- **A sound and complete calculus.** A deep natural-deduction calculus for the embedding's higher-order logic, with ∀E/∃I instances restricted to $\mathcal L$-terms and Leibniz substitution at every type of $\mathcal L$, is sound over v4's $\mathcal L$-general models with nonempty individuals, and complete: for every $\mathcal L$-theory $T$ and sentence $\varphi$, $\varphi$ holds in all such models of $T$ exactly when the calculus derives it from $T\cup\{\exists x.\top\}$. Löwenheim–Skolem and compactness follow: for theories containing $\exists x.\top$, a failure has a countermodel with countably many worlds and countable carriers, and every consequence follows from a finite sub-theory.- **prop:lgeneral in deep form.** Leibniz with whole-term motives and $\mathcal L$-term sides derives the same sentences, and unrestricted Leibniz derives the separating sentence from any theory, so the motive clause is what keeps the calculus sound.- **ex:separating at all types.** v4's flip model (total frame on $2^{\mathbb N}$, one individual, empty positivity) is $\mathcal L$-general at every type of $\mathcal L$ and refutes the separating sentence at every world. A model of variant 2 (Ax1Gen, Ax2a, Ax2b, Ax3, Ax4), with modal collapse and a God-like being, also refutes it at every world: a separating model for one of v4's axiom sets. With finitely many worlds the sentence always holds, so such a model needs infinitely many.- **The equivalence, semantically.** In every $\mathcal L$-general model of variant 2 or 3′ (Ax2a, Ax2b, $P\,E$, Ax4, $\exists x.\top$), Ax1GenTwo holds everywhere exactly when unrestricted Ax1Gen does, and then modal collapse and a God-like being follow (in variant 2 with Ax3).- **The witness criterion does not suffice in practice.** A Lean proof of the separating sentence in v4's own `Ax1GenTwoVariant2` module, which uses the nominal $\lambda u.\,u=w$ only as an argument of `congrFun`, passes v4's `hybrid_check.py` with no flags in both witness and whole-term mode. The sentence fails in the variant-2 model above, so the detector certifies a proof of a sentence that is not a consequence over $\mathcal L$-general models.## Prior workSoundness over $\mathcal L$-general models for whole-term proofs is v4's Propositionprop:lgeneral, proved there in prose; here it is a Lean theorem about an explicit calculus. Theseparating sentence is in substance the world-proposition axiom of Fine and Kaplan[2]: some true proposition entails every truth. Its failure in atomlessalgebras is known for S5 with propositional quantifiers [3], finite-support(Fraenkel–Mostowski) constructions of Henkin models are standard [4], andcompactness and Löwenheim–Skolem for intensional general models follow Muskens's pattern[5]. Existing completeness theorems for the embedding are relative toHenkin models [6], whose domains contain every singleton, so they arenot $\mathcal L$-general. We found no statement of completeness over $\mathcal L$-generalmodels, of a separating model for one of v4's axiom sets, or of the detector result.## Why it mattersThe first four items settle, inside Lean, the semantic question v4 states as open, and theygive the detector-certified proofs on this site a meaning: a whole-term proof is true in every$\mathcal L$-general model. The last item shows that the detector's implementation can miss anominal hidden in a motive, which is the case v4's open question asks about. It does not refuteProposition prop:lgeneral, which holds; it shows that certifying proofs with the detector isnot yet a substitute for the semantic proof.## Proved vs checkedEvery claim except the detector result is a Lean 4 theorem (core library, axioms propext,Classical.choice and Quot.sound only), kernel-checked in the library build. The detector resultis a Lean proof plus a run of v4's `hybrid_check.py` on it; the run's skeptic found it and wereproduced it outside the run. Its status is *derived* because the detector run is a check, nota Lean theorem.This result extends:- Benzmüller, "Proofs Without Nominals", arXiv 2609.36279 v4, Prop. prop:lgeneral with Def. def:lgeneral: soundness of HOL proofs over 𝓛-general models, under a stronger whole-term hypothesis (every term used as an element of an 𝓛-domain is an 𝓛-term). It uses the same relativisation and covers the same Leibniz case. The proof is informal and not mechanised, and there is no deep ND. The paper leaves the instance-only (witness) version open.- Benzmüller, "Gödel's and Scott's variants … in Lean 4 and TPTP THF", arXiv 2609.26806 v3, Section sec:axioms: states without proof that results whose instantiations are object-language terms hold in all models closed under the object-language operations.- Hetzl, "Higher-Order Logic" lecture notes, https://dmg.tuwien.ac.at/hetzl/teaching/hol.20190125.pdf: Henkin structures as prestructures closed under definability, and Henkin soundness of the calculus (generic HOL, not the modal embedding).- Stanford Encyclopedia of Philosophy, "Second-order and Higher-order Logic", https://plato.stanford.edu/archIves/spr2010/entries/logic-higher-order/: general structures closed under definability, where the comprehension axioms hold.- van Benthem, "Changing a semantics: opportunism or courage?", https://arxiv.org/pdf/1411.7636: predicative or restricted comprehension goes naturally with Henkin-style models.- Benzmüller & Kirchner, "Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness", https://arxiv.org/abs/2609.07345: mechanised deep/shallow faithfulness against comprehension-closed vs general MSO readings. There is no restricted-instance ND soundness and no primitive equality.- Benzmüller, "Proofs Without Nominals", arXiv 2609.36279 v4, https://arxiv.org/abs/2609.36279: soundness over 𝓛-general models for whole-term 𝓛-proofs (Prop. prop:lgeneral). Hybrid-free derivations of ∃^E G and MC under Ax1GenTwo, Ax2a, Ax3 and Ax4 (Thm. thm:gextwo, Cor. cor:gextwo, Thm. thm:plain). G_ex from Ax1Gen, Ax2a, Ax4 and L (Thm. thm:gex). Ax1GenTwo ⇒ Ax1Gen is proved only with nominals and is stated as open without them (Sect. sec:plain, sec:open).- Benzmüller, "Gödel's and Scott's Variants … in Lean 4 and TPTP THF", arXiv 2609.26806 v3, https://arxiv.org/abs/2609.26806: notes that its object-language-only instantiations make the port's bounds hold in every model closed under the object-language operations. This is informal; there is no theorem.- 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: the source variants, with Ax1Gen, MC and G_ex proved over full/Henkin semantics only.- C. Benzmüller, "Proofs Without Nominals", arXiv 2609.36279v4 (sources/2609.36279/v4/main.tex). `def:lgeneral` and `prop:lgeneral` give soundness over 𝓛-closed models, with equality read as agreement on P and functions extended by restriction (the respect-eqT idea, assumed rather than separated). `ex:separating` gives the FM flip model on 2^ℕ refuting A∃p.(Atom p ∧ p). There is no non-respecting counterexample, no Leibniz rule at every type, and no rel-self-related carriers.- P. B. Andrews, "General models and extensionality", JSL 37(2) 1972, https://doi.org/10.2307/2272982. A general model in which Leibniz-stated extensionality fails because the sets are sparse. This is the classical form of the K3 phenomenon.- C. Benzmüller, C. E. Brown, M. Kohlhase, "Higher-order semantics and extensionality", JSL 69(4) 2004, https://projecteuclid.org/journals/journal-of-symbolic-logic/volume-69/issue-4/Higher-order-semantics-and-extensionality/10.2178/jsl/1102022211.short. Model classes with and without functional extensionality, property q, and Leibniz versus primitive equality. This is the general framework for K3/K4.- W. Degen & J. Johannsen, "Cumulative Higher-Order Logic as a Foundation for Set Theory", https://www.ifi.lmu.de/institut/personen/jjohannsen/jj_papers/kumlog.pdf. A quotient of Henkin structures under Leibniz equality, related to the self-related/collapse construction in K6.- P. Fritz, "Propositional Quantifiers" (Cambridge Element), https://philpapers.org/rec/FRIPQC, and "Nonconservative extensions by propositional quantifiers…", https://academic.oup.com/logcom/advance-article/doi/10.1093/logcom/exae043/7724499. Quantifiable general frames (domains closed under definable formulas) for propositionally quantified modal logic. This covers only the propositional level of the 𝓛-closure condition.- C. Benzmüller, "Proofs Without Nominals …", https://arxiv.org/abs/2609.36279 (v4), Example ex:separating: an atomless L-general model on 2^N (total frame, empty positivity, one individual) in which A∃p.(Atom p ∧ p) fails everywhere, formalised in Isabelle and Lean (propositional part). The paper states that this model is not a variant-2 model, and lists as open whether a separating model exists for any of the variants' axioms. K7 fills that gap for variant 2 (identity frame).- Same paper, Proposition prop:lgeneral: soundness of proofs meeting the whole-term criterion over L-general models. This is the tool that turns K7's model into "underivable in the calculus".- Some General Completeness Results