PaperlayerView exact revision on arXiv

Source-linked AI summary

Proofs Without Nominals: G\"odel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

Christoph Benzmüller

arXiv:2609.36279v2cs.LOcs.AImath.LO

TL;DR

The embedding’s higher-order property quantifiers can admit nominal and satisfaction-operator terms, so a valid embedding proof need not be a result of the modal object language. This paper mechanically audits proof instantiations and settles the Notes’ three open questions hybrid-free, while showing that the conjunction axiom must exclude degenerate cases.

  • Problem

    The embedding admits property terms outside the modal object language, so a theorem proved with such an instantiation need not be a result of the arguments’ modal logic.

    Source: §1 · p. 2

  • Method

    The paper mechanically analyzes the embedding’s proof terms to check whether property and proposition instantiations stay within the object language.

    Source: §1 · p. 2

  • Results

    The three open questions are settled hybrid-free under a conjunction axiom restricted to at least two different conjuncts, and the established results are verified in Isabelle/HOL and Lean 4.

    Source: §1 · p. 3, §8 · p. 19

  • Takeaways & Limitations

    The criterion certifies that an embedding proof stays within the object language, but does not provide an object-level derivation or establish that the theorem has one.

    Source: §8 · p. 19

    The restriction has no force when the axioms make accessibility the identity, since the degenerate conjunction instances become available again in variant 3.

    Source: §6.2 · p. 14

Abstract

from arXiv · show

The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzm\"uller and Scott's Notes on G\"odel's and Scott's variants of the ontological argument (2025), reaches beyond the modal object language of the arguments: its property quantifiers range over terms that may also express nominals and satisfaction operators of hybrid logic, and a proof using one proves a theorem of the embedding that need not be one of the modal logic. That the framework affords this is not new, and whether a result is one of the modal logic can be settled in two ways: by replaying it in an explicit proof calculus, done by hand for chosen theorems, or by analysing the proofs the embedding itself produces, done here mechanically, for every result at once. Every statement the Notes prove has a proof inside the object language: 294 written out by hand and machine-checked, none using a nominal. The proofs the Notes themselves give instantiate no nominal either; what the detector flags there are terms a prover substituted. The three questions the Notes leave open are settled too, without nominals, but the conjunction axiom has to be emended: generalised in the Notes to G\"odel's "any number of summands", it covers the conjunction of no properties, and of one; the empty one alone settles all three, and the two together yield what a separate axiom of G\"odel's is for. This article restricts the conjunction axiom to at least two different conjuncts, the reading G\"odel's footnote suggests, and the questions are settled again, by proofs that turn on the argument rather than a degenerate instance. The restriction holds of the object language only: with a nominal the axioms make the accessibility relation the identity and the readings coincide. Every theorem is verified in Isabelle/HOL and independently in Lean 4; the countermodels are Nitpick's, certified by the build.

1 Introduction

The embedding’s property quantifiers admit hybrid terms outside the modal object language, so its theorems need not belong to the intended modal logic. The article mechanically audits proof instantiations and settles the Notes’ three open questions hybrid-free, with a restricted conjunction axiom.

1 Introduction

  • HOL property domains admit terms expressing nominals and satisfaction operators that the modal object language cannot express.A proof using such a term is valid in the embedding but need not establish a result of the arguments’ modal logic.Source: §1 · p. 2
  • Mechanical analysis of embedding-generated proofs determines whether their property or proposition instantiations stay inside the object language.Unlike replaying selected theorems in an explicit calculus, this approach applies to every result of the Notes at once.Source: §1 · p. 2
  • The targets were Th3 for repaired-essence Gödel in S4, Th3 and essence-uniqueness lemmas for repaired-inclusion Gödel, and Scott’s T3 under Ax1Gen.The first two were open in S4 and S5 respectively; Scott’s S4 countermodels were unreproduced and no proof had been found.Source: §1 · p. 2
  • The Notes’ first two questions comprise ten open statements across actualist, possibilist, and mixed quantifier settings; the third has no recorded statement.The possibilist and mixed copies are settled as well.Source: §1 · p. 2
  • The three open questions are settled hybrid-free only after restricting Ax1Gen to at least two different conjuncts.The unrestricted axiom’s empty and singleton instances make it too strong; variant 3 also requires the essence repair to be confined to the essence itself.Source: §1 · p. 3
  • Every statement proved in the Notes has an object-language proof in Lean 4 and Isabelle/HOL.The Isabelle proof is either the Notes’ own proof or one written for the purpose when the detector did not certify it.Source: §1 · p. 3

2 The embedding and the three developments

The paper sets out the modal framework and the three developments of Gödel’s and Scott’s arguments that supply the open questions. Their proof structure makes symmetry central to the S4 questions, while the conjunction axiom’s generalization traces to a later rendering of Gödel’s footnote.

2 The embedding and the three developments

  • Worlds are type i, individuals type e, propositions predicates on worlds, and properties functions from individuals to propositions.S4 assumes reflexivity and transitivity; no other accessibility condition is assumed unless stated.Source: §2 · p. 3
  • The three developments are considered in S4; variant 2’s mixed-quantifier setting is also introduced in K.The work began after a talk raised whether AI systems could help settle the open proofs; early proofs prompted the question because nominals appeared to do work.Source: §2 · p. 3
  • The generalized conjunction axiom follows Anderson and Gettings and Fitting’s later rendering of Gödel’s “any number of summands” footnote.A related proposal appears in Gödel’s Nachlass.Source: §2 · p. 3
  • Of 427 original proofs read in full, 403 were certified and none instantiated a nominal.The other 24 contained prover-substituted terms: fourteen world-dependent Skolem functions and ten HOL library constants.Source: §2 · p. 3
  • Variant 2 combines positivity axioms with Ax1Gen, the generalized conjunction axiom, and defines God-likeness, essence, and necessary existence.Its essence definition includes the conjunct that repairs Gödel’s 1970 definition.Source: §2 · p. 4
  • Variant 3 uses Gödel’s original essence definition but places the non-emptiness repair in necessary property inclusion.The including property is required to be non-empty.Source: §2 · p. 4
  • Scott’s variant replaces A3, positivity of God-likeness, with Ax1Gen; the paper states that God-likeness then follows as Lemma L.Its essence and necessary-existence definitions match variant 2.Source: §2 · p. 4
  • In all three developments, possible existence and essentiality results need no frame condition, but deriving Th3, T3, and modal collapse uses symmetry.Th3 remains the open question in S4.Source: §2 · p. 4

3 Hybrid witnesses

The paper defines the Notes’ modal object language and tests proof terms by checking whether their property and proposition instantiations are expressible in that language. This criterion excludes hybrid witnesses while leaving individual and lifted-type variables outside its target.

3 Hybrid witnesses

  • L comprises the Notes’ lifted connectives, modal operators, individual quantifiers, declared constants, and bound variables; HOL terms can fall outside it.Nominals and satisfaction operators are not expressible in L, even though the embedding admits corresponding HOL terms.Source: §3 · p. 4
  • A proof is hybrid-free when every term substituted for a property or proposition variable belongs to L.The relevant instantiations occur in axiom instances, definitions, the generalized conjunction set, and lemmas or hypotheses applied to properties or propositions.Source: §3 · pp. 4–5
  • The criterion targets higher-type domains because object-language readings restrict those domains, whereas individual witnesses remain elements of the modal model’s domain.The detector extracts world-lifted-type instantiations from proof terms and checks them against L’s grammar; its flags identify forms such as world equations, accessibility relations, and world quantifiers.Source: §3 · p. 5

4 A God-like being exists at every world

With Ax1Gen as stated, the argument derives an actual God-like being at every world and further frame-free results. But the derivation turns on the empty conjunction, so these answers must be revisited with degenerate conjunctions excluded.

The empty conjunction

  • The proof makes “no actual God-like being exists” positive by applying Ax1Gen where its world-dependent conjunction has no conjuncts.That positivity combines with Ax4 and the positivity of G to contradict Ax2a’s exclusivity.Source: §4 · pp. 5–6

Conjunction construction

  • The proof’s conjunction construction establishes that the properties selected by χ form a conjunction, including vacuously where Φ is empty.The lemma’s proof uses L and ⌊P G⌋ in Lean 4; the Isabelle/HOL metis proof is also given Ax2a but does not need it.Source: §4 · pp. 5–6

Existence at every world

  • In both variant 2 and Scott’s variant, Ax1Gen with the other stated axioms yields an actual God-like being at every world, without a frame condition.The proof for variant 2 uses Ax1Gen, Ax2a and Ax4; Scott’s uses Ax1Gen, A1 and A2.Source: §4 · p. 6

Consequences

  • The resulting existence theorem gives Th3 and Th5/T3, while modal collapse also follows, all without a frame condition.The section also derives OneWorld by applying modal collapse to a nominal; that frame correspondent is hybrid.Source: §4 · p. 6

Scope of the result

  • These results are too quick as answers to the open questions because the empty conjunction instance makes Ax1Gen too strong.The empty and singleton instances together yield the possible existence of a God-like being, the role of a separate axiom; the answers are given again after excluding degenerate instances.Source: §4 · p. 6

5 Variant 3: there is exactly one world

Variant 3 yields strong collapse results: with a nominal, its definitions alone force a single world, while hybrid-free proofs establish essence membership and uniqueness even without frame conditions. The section also distinguishes those results from findings that rely on Ax1Gen as stated.

Modified property inclusion

  • With modified property inclusion, Th3, Th5 and modal collapse hold hybrid-free and frame-free; the stronger essence and uniqueness results come from definitions, at the price of nominals.The nominal-dependent results are distinguished from hybrid-free results that can be proved without it.Source: §5 · p. 7

Collapse from the definitions

  • With a nominal witness, variant 3’s definitions alone force exactly one world, so an essence there can only be “being x.”This route uses no conjunction axiom and is hybrid.Source: §5 · p. 7

No necessary existence

  • If two worlds differ, variant 3’s necessary-existence predicate is empty; the proof uses reflexivity but no axiom, and is hybrid.Its witnesses are “being x at w” and “being at v.”Source: §5 · p. 7

Frame consequences

  • In variant 3, Th3 follows from Ax3 and reflexivity, while Ax2a, Ax3 and Ax4 together force any two worlds to be equal.The latter argument proceeds by deriving a contradiction from the assumption that two worlds differ.Source: §5 · p. 7

Tools for the hybrid-free proofs

  • Ax2a, Ax3 and Ax4 imply seriality, and the section also proves a hybrid-free reachability lemma without frame conditions.Reach_K says every non-empty property is exemplified at a successor of every world; the seriality lemma supplies a successor even without a frame assumption.Source: §5 · pp. 7–8

Essence uniqueness

  • Theorem 9 proves hybrid-free that an essence is had by its individual and that both uniqueness lemmas hold.The argument uses reachability to rule out a non-empty property that would contradict the uniqueness result.Source: §5 · p. 8

Answer to question 2

  • In K, Th3 and both uniqueness lemmas hold in variant 3; the uniqueness results follow because the modal structure has collapsed.The Notes had expected the uniqueness lemmas, but not for this reason.Source: §5 · pp. 7–8

Quantifier settings and scope

  • The hybrid-free results extend to possibilist and mixed settings, but the mixed setting’s argument for Th3 does not work with actualist existence.The proofs are re-established under Ax1GenTwo, with stated side conditions and variant 3’s emended form; the results resting on Ax1Gen as stated retain the earlier reservation.Source: §5 · pp. 8–9

6 Emendations of the conjunction axiom

The section restricts Ax1Gen to conjunctions of at least two different properties, then reassesses derivability under the emended reading, including variant 3’s non-emptiness clause. It separates the effects of degenerate conjunction instances from world-dependence and notes that nominals erase the distinction between readings.

6 Emendations of the conjunction axiom

  • The empty and singleton instances of Ax1Gen violate requirement (ii), so the section adopts Ax1GenTwo, requiring at least two different conjuncts.The restriction removes only the degenerate instances; Ax1 is redundant because the two-conjunct case yields it when the conjuncts coincide.Source: §6 · pp. 9–10

6.1 Ax1GenTwo: at least two different conjuncts

  • In variant 2, Ax1GenTwo yields L, and Th4 follows from Ax2a, Ax4, and L; the collapse results follow under Corollary 12’s conditions.At worlds with a positive property other than the universal property, an actual God-like being exists; the corollary also covers worlds where every world has an actual individual.Source: §6.1 · pp. 10–11
  • Scott’s Ax1GenTwo variant proves L_Two from A1, A2, and A5, plus actual God-like existence where a positive property is non-universal, hence everywhere if every world has an actual individual, then T3 and MC, without frame conditions or hybrids.In variant 3, Ax1GenTwo yields neither Th4 nor G_ex, even in S4; taking Th4 as a hypothesis brings the answers back. Whether (†) can be dropped from the hybrid-free proof remains open.Source: §6.1 · pp. 11–12

6.2 Variant 3: where the non-emptiness clause belongs

  • In variant 3, confining the non-emptiness clause to the essence while using plain inclusion in Ax4 restores hybrid-free results, including L, Th4, and collapse conclusions.The universal property’s positivity follows from Ax3 and Ax4 without a conjunction axiom, and the repaired variant is consistent with Ax1GenTwo.Source: §6.2 · pp. 13–14
  • With nominals, variant 3 forces identity accessibility and recovers full Ax1Gen, so Ax1GenTwo and Ax1Gen become equivalent; hybrid-free equivalence remains open.The proof of this equivalence uses nominal arguments, and the two-conjunct restriction has force only in the object language.Source: §6.2 · pp. 13–14
  • Across four settings, 44 of 76 Ax1Gen-dependent results carry over verbatim and 30 need local repair; only AllExist is lost in emended variant 3.AllExist has a genuine countermodel in the possibilist setting; no downstream result depends on it.Source: §6.2 · p. 14

6.3 Two neighbouring readings

  • Ax1GenOne satisfies the first two requirements and gives collapse without a proviso, but its full results with nominals leave hybrid-free variant 3 open.Its singleton instance recovers full Ax1Gen with a nominal; the hybrid-free question remains unresolved.Source: §6.3 · p. 15
  • Ax1GenBox blocks the collapse proof but fails requirement (ii), since Ax1GenBox and Ax2a alone yield Th4; in variant 3 it is idle.Scott’s variant has the same pattern, while variant 3’s base axioms force one world and recover Ax1Gen.Source: §6.3 · p. 15

6.4 Assessment

  • For variant 3′, Theorem 16 gives the separate Ax1GenTwo results; Ax1GenOne inherits them, Ax1Gen follows from variant 3, and Ax1GenBox is idle because the axioms force one world.Theorem 16’s results are the only separate results among the four readings for variant 3′.Source: §6.4 · p. 16
  • In variant 3, collapse is hybrid-free and frame-free under Ax1Gen, while Ax1GenBox’s collapse passes through the one-world argument with nominals.With Th4 as a hypothesis in variant 3, Theorem 15 applies.Source: §6.4 · p. 16
  • In variant 2, both cardinality restrictions meet all three requirements, and the two-conjunct reading matches Gödel’s footnote.It differs from the other restriction by omitting the singleton instance, the closure of positivity under necessary coextension.Source: §6.4 · p. 16
  • Ax1Gen’s strength comes from empty- and singleton-conjunction instances: the derivation violating requirement (ii) needs both, so excluding the empty instance suffices.Both cardinality restrictions exclude the empty instance.Source: §6.4 · p. 16
  • Only Ax1GenBox removes collapse caused by world-dependent Φ, but it incurs failure of requirement (ii) and helps only when collapse is not already definitionally forced.In variant 3, the definitions already produce the collapse.Source: §6.4 · p. 16

7 The audit of the Notes

The audit finds an object-language proof for every statement the Notes prove, while distinguishing prover-substituted terms from witnesses the arguments require. A separate Lean 4 port confirms that its 294 hand-written proofs use no nominal.

The audit of the Notes

  • 403 of the Notes’ 427 proofs are certified as written; the other 24 use prover-substituted terms, and none of the counted witnesses is a nominal.Each of the 24 has a separately written proof that Isabelle/HOL certifies.Source: §7 · p. 16
  • The Lean 4 port supplies an object-language proof for every statement the Notes prove, including the 24 whose original Isabelle/HOL proofs are not certified.The port’s hand-written proofs and Isabelle/HOL’s original-proof audit address different proof sets.Source: §7 · pp. 16–17
  • A hybrid-witness flag in the original proofs records a prover substitution, not a need of the argument; Th4 also has a hybrid-free, frame-free proof in K.That proof corrects the Notes’ claim that symmetry is needed for Th4 in the mixed-quantifier setting.Source: §7 · pp. 16–17
  • All 294 hand-written proofs of the Notes’ results in Lean 4 are unflagged, and every property or proposition instantiation is a term of L.The port records 318 distinct instantiations in 44 shapes; none depends on sorry.Source: §7 · p. 17
  • The two audits are complementary: Isabelle/HOL reads the Notes’ original proofs, while Lean 4 reads proofs written for the purpose.They count 1,177 and 318 instantiations respectively because the Isabelle/HOL automation reaches facts through quantifier rules.Source: §7 · p. 17

8 Discussion

The discussion separates theorems of the embedded higher-order logic from results reproducible in the modal object language, and weighs the audit’s reach against its limits. It also examines how the conjunction axiom and frame assumptions shape the results.

Discussion

  • The generalized conjunction axiom’s empty and singleton instances already yield possible existence of a God-like being with Ax2a, without Ax4.Because the property set may depend on the world, the empty-conjunction instance can transport the absence of an actual God-like being into positivity.Source: §8 · pp. 17–18
  • Under Ax1Gen, modal collapse follows in K; in variant 3, the axioms reduce the model to one world and erase the actualist–possibilist distinction.That erasure is specific to variant 3 with those quantifiers; under the emendation, AllExist has a countermodel.Source: §8 · p. 18
  • Hybrid-free proofs establish theorems even for property domains closed only under object-language operations, while nominal-based frame results concern the broader HOL models.No model finder over the shallow embedding can produce a countermodel to the object-language reading by omitting nominal properties from its domains.Source: §8 · pp. 18–19
  • The detector is cheaper and scales to hundreds of proofs, but it certifies only that a proof stays in the object language, not that no such proof exists.A rejected proof may still have an object-language derivation, as the two replaced nominal proofs show.Source: §8 · p. 19
  • The theorem results are checked in Isabelle/HOL and Lean 4, whose independent kernels, embeddings, and hand-written proof terms provide a second check.The two systems’ detectors agree on the flagged and certified results described in the discussion.Source: §8 · p. 19
  • Lean 4 supplies no comparable model finder or proof-search counterpart in this study, so its proofs do not reproduce the negative results.The authors qualify this as a limitation of the tools as used, not a verdict on the systems.Source: §8 · p. 19
  • With Ax1Gen or Ax1GenTwo, the results are frame-free; only under Ax1GenBox does the S4 question yield the countermodel the Notes expected.S4 and KB are incomparable, but the frame is trivialized under the first two readings.Source: §8 · p. 19
  • The embedding’s higher-order property quantifiers can range over nominals, so a proof using one need not be reproducible in the modal object language.The proposed detector checks proof substitutions mechanically across a development; it does not itself produce an object-language derivation.Source: §8 · p. 20

9 Verification

The verification section reports formalizations, audits, and reproducible checks in Isabelle/HOL and Lean 4. It explains how the proof and dependency records support the results and where the systems’ verification roles differ.

Verification

  • The formalization pairs Isabelle/HOL theories with Lean 4 modules and audits 197 Isabelle/HOL results, flagging 17 as hybrid and certifying 180.Lean’s detector agrees on the flagged results and inheritance; Table 1 records the proof dependencies and detector verdicts.Source: §9 · p. 20, Table 1 · p. 22
  • Hand-written proofs replace two automation proofs whose instantiations would otherwise be flagged, making both object-language arguments certifiable.These are the proof of L and UniqueEss3; the latter’s port proof uses Leibniz identity rather than a nominal.Source: §9 · pp. 20–21
  • Recorded Isabelle/HOL proof terms and Lean 4’s #print axioms provide matching accounts of the postulates each proof uses.The account shows symmetry in 61 Notes results, transitivity only in test theories, and reflexivity in those theories and variant-1 Th3.Source: §9 · p. 21
  • Table 1 groups results by development and reading, distinguishing hybrid proofs from inherited hybridness and marking frame assumptions and side conditions.The caption identifies separate blocks for open questions, quantifier variants, collapse results, and Ax1GenTwo and Ax1GenBox readings.Source: §9 · p. 21, Table 1 · p. 22
  • The build certifies all 72 Nitpick searches through expect annotations across sixteen Isabelle/HOL sessions: 34 expect genuine countermodels, 23 expect none within given cardinalities, and 15 record that the search gives up.Source: §9 · p. 21
  • Positive results are kernel-checked and negative results are build-certified, so the claims rest on reproducible artefacts rather than AI-assisted drafting.The article reports the AI coding assistant’s role and notes that the detector’s verdicts changed during development and review.Source: §9 · p. 23

A The detector

The detector applies a language-membership criterion to proof substitutions at world-lifted types. Separate Isabelle/HOL and Lean 4 implementations reconstruct or traverse proof terms, then test the resulting witnesses against that criterion.

The detector

  • The criterion asks whether proof terms instantiate world-lifted variables only with terms of the modal object language L.It applies to any proof term over the shallow embedding, not only the ontological-argument development.Source: A The detector · p. 23
  • The Isabelle/HOL detector reconstructs recorded proofs, traverses nested automation proofs, and checks collected witness terms against a grammar for L.It also scans definitions and abbreviations so a witness cannot hide behind an audited constant.Source: A The detector · pp. 23–24
  • The Lean 4 detector traverses theorem proof terms, listing lifted-type instantiations and testing them for hybrid witnesses.It unfolds definitions inside witnesses and examines terms in witness positions of meta-level constructs.Source: A The detector · p. 24
  • Both implementations are tested against 23 out-of-language probes and 17 terms of L, with every probe required to receive its expected verdict.The probes include nominals, satisfaction operators, accessibility terms, and ordinary object-language terms that must not be flagged.Source: A The detector · p. 24

B The two runs in detail

The Isabelle/HOL detector reconstructs theorem proofs and nested bodies, then distinguishes argument instantiations from proof-method machinery. The section reports its tally, an Isar cross-check, and a Lean 4 census of instantiations.

Isabelle/HOL proof reading

  • The detector reconstructs proofs and nested bodies, replacing unreadable MinProof leaves with placeholders; 102,656 sub-derivations remain unread.The unread statements include 28 world-equation clauses, all from smt proofs of Th1 and Th2 in variant 3; these are prover-made clauses, not argument substitutions.Source: B The two runs in detail · pp. 24–25

Counting criterion

  • 19,668 of 19,699 flagged terms belong to proof-method machinery, and all 164 world-equation occurrences are prover Skolem terms rather than argument substitutions.The detector counts substitutions for variables in the developments’ facts or witnesses in HOL quantifier rules, while descending into other terms without counting their own arguments.Source: B The two runs in detail · p. 25

Isabelle/HOL tally

  • 1,177 counted instantiations occur across 427 Isabelle/HOL facts, including 851 quantifier witnesses and 364 arguments of definitional equations.The remaining 98 instantiate named development facts; Ax1Gen accounts for twenty and Ax4 for fourteen.Source: B The two runs in detail · p. 25

Flagged witnesses

  • Fourteen results carry a prover-generated Skolem function of a world through L, while ten flags are library terms and one is an object-definable existence predicate.The handwritten proofs of the fourteen L-dependent statements use the set of positive properties; the library terms denote equality, a universal property, or an arbitrary property.Source: B The two runs in detail · pp. 25–26

Isar cross-check

  • 76 counted instantiations across 19 Isar cross-check theories produce no flags, and the axiom-dependency account is independent of proof reconstruction.The cross-check includes replayed results, variant 2 proofs, and proofs of statements whose automated proofs used library terms.Source: B The two runs in detail · p. 26

Lean 4 census

  • The Lean 4 census finds 318 instantiations in 44 shapes; 72 of the Notes’ 77 statements closed with oops lack counterparts in the port.Questions 1 and 2 are among the statements left open in the port; the instantiation shapes include complements of property variables, G, and the empty and universal properties.Source: B The two runs in detail · p. 26
Loading 2609.36279v2…