Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint) Christoph Benzmüller1,2[0000−0002−3392−3093] , Daniel Kirchner , and Luca Pasetto3[0000−0003−1036−1718]
arXiv:2605.27246v1 [cs.LO] 26 May 2026
1[0000−0001−9229−1148]
Otto-Friedrich-Universität Bamberg, Kapuzinerstraße 16, 96047 Bamberg, Germany 2 Freie Universität Berlin, Kaiserswerther Str. 16-18, 14195 Berlin, Germany 3 University of Luxembourg, P. de l’Université 2, 4365 Esch-sur-Alzette, Luxembourg
1
Abstract. This position statement looks back on two decades of work on shallow embeddings of non-classical logics in classical higher-order logic (HOL), a line of research that expanded into a range of logic embeddings in HOL and inspired the LogiKEy logic-pluralistic knowledge representation and reasoning methodology. This paper advances the case for logical pluralism at object-logic level within a unifying meta-logical framework such as LogiKEy, grounding the argument in computational metaphysics. More broadly, it advocates principled support for logical pluralism in modern proof assistants, and cautions against logical imperialism—the rigid adoption of a single foundational logic for largescale theory developments—which impedes the interdisciplinary reuse that LogiKEy is designed to enable. Keywords: Logical Pluralism · Meta-Logical Reasoning · Proof Assistants · Higher-Order Logic · Classical and Non-Classical Logics
1
Introduction
The work reported here belongs to a research line, now spanning roughly two decades, on the development, formalisation, and automation of shallow embeddings of non-classical logics in classical higher-order logic (HOL). This line grew out of a side initiative within the Leo-II higher-order theorem-prover project [15, 16]4 around 2007—at a time when the automated-reasoning community was still primarily focused on less expressive first-order and propositional logics, and had yet to appreciate the long-term importance of building systems capable of handling expressive higher-order classical and non-classical logics, which are inevitably needed to enable computer-supported studies on foundational topics in metaphysics and (meta-)mathematics. The line began with a first joint paper (of the first author, with Paulson) on the embedding of multi-modal logic in HOL [8], subsequently extended and 4
Leo-II, the winner of the CASC competition in 2010 in the higher-order (THF0) category, was developed with funding from EPSRC grant EP/D070511/1.
2
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto
superseded by two journal articles: [9], on propositional multi-modal and intuitionistic logics in HOL, and [11, 10], on higher-order quantified multi-modal logics in HOL. Building on these articles, a wide range of logic embeddings in HOL were developed, including access control logic, quantified conditional logics, multivalued logic, free logics, various deontic logics, intensional HO modal logics, and public announcement logic; see also [3, 7] and the references therein. These articles subsequently inspired what was introduced and developed in [7] as the LogiKEy logic-pluralistic knowledge representation and reasoning methodology; cf. Fig. 1 for an instantiation of the LogiKEy methodology for the application direction addressed in this paper. Publication [11] was particularly instrumental in enabling fruitful applications in computational metaphysics, including first studies [17, 19] on Gödel’s [22] and Scott’s [33] modal variants of the ontological argument. A recent article [13], co-authored by Benzmüller and Scott in a special issue of Monatshefte für Mathematik dedicated to Kurt Gödel, provides a comprehensive discussion of these applications alongside some novel results and pointers to earlier and related works on this topic. This paper—a position statement, enriched by some novel results—revisits this line of work, reflects on its development, and points toward promising directions for future research. It makes a case for logical pluralism at the object-logic level, pursued within a unifying meta-logical framework. To exemplarily ground the proposal in a concrete application, the paper argues that the possible-world semantics as, for example, employed in the formalisation of Gödel’s modal ontological argument can and should be naturally extended with additional logical and mathematical notions, allowing modalised mathematical theories and Gödel’s modal ontological theory to coexist within the sketched unified logical framework; cf. Fig. 1. This unification—and the study of its implications for the modal ontological argument—is rendered particularly compelling by Gödel’s well-documented mathematical realism, according to which mathematical objects enjoy an existence wholly independent of human cognition. Once the existence of the generally infinite objects and structures of mathematics is granted, Gödel’s modal ontological theory is confronted from the outset with infinitely many positive properties, with the consequence that trivial finite models—of the kind presented in various contributions to the literature on the modal ontological argument—are thereby excluded. The notion of positive properties in Gödel’s theory will in fact be forced to be uncountably infinite (i.e. there must exist uncountably many distinct positive properties), an observation that deserves further investigation and for which the present paper offers a starting point. From a broader perspective, this paper aims to illustrate the need for principled support for logical pluralism (cf. [32] and the references therein) within modern proof assistant systems—as opposed to what one might call logical imperialism, where a particular foundational logic is adopted as the unquestioned and immovable basis for large-scale theory developments. Such rigidity risks hindering the reuse of existing libraries for interdisciplinary research of the kind
Many Logics, One Methodology
3
L3 — Applications (using L2): Further Studies on Gödel’s Modal Ontological Argument
L1 — object-logic(s) (embedded in L0): Higher-Order Modal Logic (HOML)
LogiKEy Methodology
L2 — Domain-specific Theories (modeled in L1): Gödel’s Modal Ontological Theory enriched with Modal Maths
L0 — Meta-Logic: Classical Higher-Order Logic (HOL)
Fig. 1. The logic-pluralistic knowledge representation and reasoning methodology LogiKEy instantiated for the application direction proposed in this paper.
sketched here, where mathematical theories must interface with other disciplines that do not share—or actively reject—the foundational assumptions underlying those libraries. The remainder of this paper is organised as follows. Section 2 introduces the LogiKEy methodology in more detail, contrasts logical pluralism with what we call logical imperialism, and positions LogiKEy relative to Zalta’s Principia Logico-Metaphysica (PLM) and to Isabelle’s own original pluralistic design. Section 3 then illustrates the methodology with a concrete application: starting from a shallow embedding of higher-order modal logic (HOML) in classical higher-order logic (HOL), modalised mathematical notions are introduced and combined with Gödel’s modal ontological argument, leading to (first-time formalised) cardinality results about the set of positive properties — culminating in its uncountability. Section 4 concludes the paper. The Isabelle/HOL source files associated with this paper are contained in the LATEX-sources of the arXiv preprint package.5
2
LogiKEy: Logical Pluralism vs. Logical Imperialism
2.1
The LogiKEy methodology
The term LogiKEy, introduced in [7], refers to a logic-pluralistic knowledge representation and reasoning methodology and infrastructure that has in re5
Self-contained excerpts of the Isabelle/HOL formalisations underlying the discussion are collected in Figures 2–6; the reader is encouraged to consult Fig. 2 (the embedding of HOML in HOL) early on, as the notation introduced there—in particular the syntactic distinction between possibilist (∀, ∃) and actualist (∀E , ∃E ) quantifiers, the lifted modal connectives, Leibniz equality ≡, and global validity Mvalid—is used throughout Section 3.
4
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto
cent years been frequently deployed with Isabelle/HOL [28] as its host environment—benefiting from its simultaneous support for interactive proof, proof automation, and (counter-)model finding. LogiKEy is the acronym of “Logic and Knowledge Engineering Framework and Methodology”. The methodology applies logic-based knowledge representation and reasoning to engineering tasks in which the underlying object-logic itself is a negotiable part of the design space. More concisely, the LogiKEy methodology proceeds by first embedding an object-logic of interest—e.g., a higher-order modal, deontic, conditional, or free logic—inside a meta-logic (here classical HOL) by interpreting its formulas as world- or, more generally, context-relativised predicates in HOL; domain-specific theories are then formalised on top, and applications on top of those, yielding a layered architecture (cf. Fig. 1; the layers include, but are not limited to: L0— meta-logic, L1—object-logic(s), L2—domain theories, and L3—applications).6 Because the embedding lives inside HOL, the host system’s full automation, model-finding, and proof-reconstruction infrastructure is available at every layer, and the object-logic itself becomes a negotiable parameter that can be explicitly analysed, revised, exchanged, compared, combined, etc.—exactly the pluralistic stance this paper advocates. The LogiKEy methodology is not bound to Isabelle/HOL, however, and any proof assistant based on a sufficiently strong logic can serve as host instead. The initial embedding work and the early studies on Gödel’s modal ontological argument [17, 19] used the ATP Leo-II [15], which in turn influenced the built-in support for logical pluralism in its successor Leo-III [36, 35]. Early studies using Rocq (formerly Coq) [20] as host have also been carried out [18]. Beyond computational metaphysics, the LogiKEy methodology has more recently been applied to logics and formalisms for normative and legal reasoning [7]. A key feature across both areas is that within the HOL meta-logic, object-logics—such as higher-order (multi-)modal logics or deontic logics—become first-class objects of study: they are developed, examined, and refined in direct interaction with the application domain. Shallow embeddings, adequacy, and consistency. Two concerns about the approach deserve acknowledgement. The first is that the embeddings used within LogiKEy have historically been shallow, in the sense that object-logic formulas are identified with HOL terms (e.g., via the standard translation). Such an embedding is, strictly speaking, a model construction rather than a syntactic representation of the object-logic, so one loses access to logic-specific syntactic tooling. However, (i) in exchange one gains the full automation stack of a mature classical higher-order prover—Sledgehammer, Nitpick, Metis, SMT bridges, and the like—which empirically scales to substantial formalisations; and (ii) the methodology is in fact not committed to the shallow choice: recent work [2, 6] shows that a deep embedding (as an inductive datatype of formulas) can be developed alongside the shallow one inside the same Isabelle/HOL theory, with mutual faithfulness proofs mechanised and largely automated (demonstrated so far for 6
This historically meant shallow embeddings; the methodology, however, is not committed to that choice (see the discussion at the end of this subsection).
Many Logics, One Methodology
5
propositional and first-order modal logic). The same layered LogiKEy architecture accommodates shallow and deep variants—and indeed their combination— at the L1 level. Lifting this deep-and-shallow methodology to HOML, and onward to further (existing and novel) object-logics in the LogiKEy portfolio, is a high priority for future work. The second concern is that combining HOL with objectlogic-specific axioms yields a hybrid system whose relative consistency does not follow directly from either component—a familiar issue from HOLZF [29] and Paulson’s ZFC in HOL [31]. In our setting, however, HOML is introduced purely by definitions, with any axiomatic content (e.g., Gödel’s axioms in Fig. 6) layered on top and open to inspection (cf. Sect. 3); relative consistency therefore reduces in the standard way. Soundness and completeness of the shallow embeddings have, moreover, been established by pen-and-paper proofs for many LogiKEy logics (cf. [9, 11] and the broader LogiKEy literature); what has so far been missing is a mechanisation of such results inside Isabelle/HOL itself— which the extended deep-and-shallow LogiKEy methodology now initiates. 2.2
Logical imperialism: monoculture and invisible assumptions
The LogiKEy methodology stands in contrast to the prevailing tendency in the development of mathematics libraries in modern proof assistants—a tendency we have somewhat provocatively termed logical imperialism above. Such systems implicitly privilege a particular logical or foundational framework—based, for instance, on dependent type theory, constructive logic, first-order set theory, or classical HOL—as the default or sole correct basis for all formal reasoning. The consequences are threefold: it fosters monoculture by design, where adopting an alternative foundation incurs significant encoding overhead; cultural dominance, where it becomes increasingly difficult to even ask “what if we used a different logic?”; and it may embed invisible assumptions—such as the law of excluded middle, existential import, the axiom of choice, impredicativity, extensionality, the treatment of undefinedness, and others—directly into the system, rendering them largely opaque to the user. One might argue that the recent successes of generative AI offer an easy remedy, since future generations of such systems could eventually assist in adapting existing large libraries to alternative logical foundations. While this may well prove true, it does not count against the LogiKEy methodology—on the contrary, when used in combination with this approach, such adaptations should be even better and more transparently supported, given the availability of explicit object-level–meta-level connections as formal data. Isabelle was originally designed by Paulson with logical pluralism in mind [30]. It is a generic proof assistant framework built around a minimal meta-logic (Isabelle/Pure), on top of which different object-logics can be instantiated—Isabelle/HOL, Isabelle/ZF, and Isabelle/FOL being prominent examples. It is worth noting that Isabelle’s choice of a minimal meta-logic, over which object-logics are axiomatised, constitutes a key architectural difference from LogiKEy’s preferred approach, which takes classical HOL as its meta-logic and treats different object-logics as naturally embedded substructures rather than
6
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto
axiomatically introduced ones. This distinction carries practical benefits—for proof automation in particular. In the Isabelle landscape, Isabelle/HOL has come to dominate the ecosystem in practice, with the vast majority of libraries, tools, and community efforts built exclusively around it. In this sense, the original pluralistic vision of Isabelle has been partially set aside in practical applications—including, notably, the development of formalised mathematics libraries—even if it remains present in the underlying architecture. The situation is no better in other current systems and library developments, and is arguably worse in those that were never designed with logical pluralism in mind. It must be acknowledged that, for pragmatic reasons, such foundational commitments must eventually be made in order to achieve meaningful progress on ambitious library projects. A prominent recent example is Mathlib [37], built on Lean’s [26] dependent type theory—specifically, a variant of the Calculus of Constructions with universes—with global commitments to classical logic, the axiom of choice, and Boolean extensionality. While this pragmatic stance enables the remarkable scale and coherence of such projects, it risks coming, as we fear, at the cost of foundational inflexibility and, in places, mathematically or philosophically questionable consequences.
2.3
The hidden costs of pragmatic conventions
A telling example is the treatment of division by zero in combination with existential import. One pragmatically motivated choice is to stipulate 1/0 = 0 by definition, which makes statements such as ∃x. 1/0 = x and ∃x.∀y. y/0 = x theorems. The first is merely odd; the second—asserting that all division-byzero expressions collapse to a single, even “existing” object—would strike most philosophers of mathematics as foundationally untenable. From a Platonist or structuralist perspective, these are not mathematical truths but formal artefacts of a particular definitional choice. From a formalist or fictionalist perspective they are valid, but only within the chosen system—and that qualification is precisely what tends to remain invisible to future generations of library users.7 7
It must be acknowledged, however, that this convention is not without genuine pragmatic merit: a totally defined division operator allows unconditional rewriting steps such as (x + y)/z = x/z + y/z without the side condition z ̸= 0, and may thus streamline proof automation in large mathematics libraries. Moreover, such conventions are easily translated between proof assistants—HOL Light’s x/0 = 0 and HOL4’s “undefined arbitrary value” relate via a suitable if-then-else wrapper—and can be refined locally on top of a classical HOL library by a conditional definition such as y ̸= 0 =⇒ div x y = x/y, without modifying the underlying logic. Our concern is therefore not that such conventions are illegitimate, but that, once built into libraries reused as if they were neutral mathematical bedrock, they become invisible logical assumptions; we plead for their visibility and revisability, not their abolition. The case for logical pluralism is accordingly stronger in foundational and philosophical contexts—such as the metaphysical applications discussed below—than in many
Many Logics, One Methodology
7
Crucially, this need not be an inevitable trade-off. Logics such as free logic [24, 34]—which can in fact be embedded in HOL in a straightforward manner [12]—are specifically designed to handle partial functions and undefinedness in a principled way, without resorting to junk values. We stress that adopting such a logic is by no means the only way to keep one’s foundational options open (e.g., a conditional definition layered on top of a total HOL operator may afford comparable flexibility within HOL itself). The deeper concern is neither the particular convention adopted nor the fact that pragmatic choices are made—such choices are arguably unavoidable at the scale of a modern mathematics library— but rather their explicit visibility and how they are received downstream. When future users—and future AI systems!—build on such libraries, there is a real risk that they will inherit their foundational commitments unreflectedly, treating them as neutral mathematical bedrock rather than as one considered option among several, each carrying its own philosophical commitments and formal consequences. More pressing still is that foundational flexibility and logical pluralism are not merely desirable but necessary for certain interdisciplinary applications of formalised reasoning that seek to bridge distinct domains—say, mathematics with philosophy and metaphysics. In metaphysical studies such as those concerned with Gödel’s modal ontological argument, principles routinely taken for granted in classical mathematics libraries must frequently be rejected outright to avoid trivialisation, paradox, and inconsistency. At the same time, the metaphysical structures under investigation often stand in deep and important relationships to cognate mathematical structures. A case in point is Gödel’s notion of positive properties in his modal ontological theory, which corresponds to a modalised ultrafilter on sets, or equivalently on properties [5, 13]—an insight that calls for a unified framework in which both the metaphysical and mathematical dimensions can be investigated together.8 This demand is further reinforced by Gödel’s nuanced mathematical realism, which motivates enriching his modal ontological theory with foundational mathematical concepts and structures—e.g. a theory of natural numbers—and which, as we argue, would thereby rule out trivial finite interpretations of positive properties. This provides yet another compelling reason to pursue a unified foundational framework that is both logically flexible and interdisciplinarily adequate. industrial verification settings, where a single, well-understood, classically total foundation may be the most effective engineering choice. 8 Readers unfamiliar with these notions may wish to know in advance that “positive properties” is a primitive notion in Gödel’s modal ontological argument, governed by axioms that, taken together, force this set of properties to behave as an ultrafilter in the modal setting; the precise formal counterpart—a modal ultrafilter on the world-relativised power set—is defined in Section 3 and Fig. 3, and the connection to Gödel’s axioms is reviewed there. “Positive” here is the term Gödel inherits from Leibniz, and—in Gödel’s own words—is intended “in the moral aesthetic sense (independently of the accidental structure of the world)” [22]; it has no connection to any of the technical uses of “positive” in logic or computer science.
8
2.4
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto
Principled monism: Zalta’s PLM as alternative
At this point it is worth noting that philosophers have developed principled approaches aimed at proper foundations for all of the sciences, including pluralistic entry points for mathematics. Zalta’s Principia Logico-Metaphysica (PLM) [40] is one such serious and sophisticated system. It formalises abstract object theory (AOT) [38, 39] within a higher-order hyperintensional modal logic, with a carefully crafted treatment of encoding versus exemplification, existence, and undefinedness, based on a relational base logic, and it has been used to formalise a remarkable range of metaphysical results. Briefly, AOT distinguishes two modes of predication: ordinary objects exemplify properties (the familiar predication of standard logic), while abstract objects, in addition, may encode properties—i.e. have them as constitutive parts of their nature without instantiating them in the usual sense; this distinction underwrites Zalta’s reconstructions of Fregean numbers, Platonic forms, situations, possible worlds, fictional and mythical objects, and Leibnizian concepts, among others (see [40] for the full catalogue). The system is also hyperintensional, in the sense that necessarily equivalent properties are not automatically identified, which is essential for the metaphysical distinctions just listed. A sophisticated challenge to the logical pluralism advocated here might therefore be posed as follows. Rather than keeping the object-logic negotiable, why not choose, in the spirit of logical monism, a single foundation rich enough that negotiation becomes unnecessary? PLM thus by no means represents crude or unreflective logical imperialism, but a principled response to it: a foundation specifically engineered to be adequate for both mathematics and metaphysics simultaneously. We resist this conclusion, for two reasons. First, PLM’s very richness is a liability as much as an asset: its foundational commitments are substantial and distinctive—the encoding/exemplification distinction, the choice of a relational base logic, the specific treatment of definite descriptions and undefinedness, and the strict hyperintensionality of property identity, to name only the most visible ones—and researchers who do not endorse this particular package (for instance, because they wish to remain neutral on hyperintensionality, prefer a functional-style base logic, or are exploring weaker or alternative metaphysical commitments) find themselves working against the grain of the system rather than with it. Second, and more fundamentally, PLM is a foundational theory—a specific set of ontological and logical commitments advanced as the correct foundation—whereas LogiKEy is a methodology, one that treats the choice of objectlogic, and to some extent even the choice of meta-logic, as itself an object of study rather than a settled question. A vivid illustration of this distinction comes from the second author’s earlier work [23], in which the LogiKEy methodology—with appropriate adaptations— was used to embed the logical foundations of PLM and AOT as an object-logic within classical higher-order logic. This made PLM itself an object of formal study, with a notable outcome: a previously known paradox, which had been inadvertently reintroduced without detection, was identified through interaction
Many Logics, One Methodology
9
with Isabelle/HOL and subsequently corrected. Far from undermining PLM, this episode exemplifies exactly what logical pluralism enables: the ability to step outside any given system, examine its foundations critically, and compare it with alternatives. Furthermore, LogiKEy is not committed to a fixed meta-logical layer. The current choice of classical HOL rests on pragmatic grounds: it offers a concise and well-understood syntax and semantics, together with comparatively mature automation support relative to other logics of comparable expressiveness.9 But this choice is not constitutive of the LogiKEy methodology. Conceptually, additional layers can be introduced, so that within an ultimate meta-logic—HOL, or something beyond it—expressive foundational logics and theories, including AOT and PLM itself, can be embedded as object-logics, which may in turn serve as meta-logics for yet further encodings. This regress is not vicious but productive: it is precisely what distinguishes a methodology from a foundation. A foundation forecloses; a methodology explores. PLM, in this sense, narrows the logical landscape by design—whereas LogiKEy maps it. That said, the dialogue between the two approaches has proven mutually illuminating, and there is no reason to regard them as adversaries rather than complements. It is worth noting that the unifying formalisation tasks motivated and initiated in this work could in principle be carried out using PLM as a foundation— and related work connecting Gödel’s theory with mathematical structures has indeed been presented recently by Zalta [41]. The distinction discussed above nonetheless persists: the only currently available means of verifying such work on a computer is through the embedding of PLM in HOL described in [23], following the LogiKEy methodology. A dedicated, native proof assistant for AOT and PLM could, of course, be developed, but doing so would require considerable effort if undertaken manually—though, as noted above, generative AI may eventually prove helpful in this regard. Furthermore, the broad foundational ambitions of AOT and, in particular, its fine-grained hyperintensionality and its careful treatment of philosophical nuances in modal reasoning10 makes meaningful automation support challenging to achieve, at least in comparison to HOL. The point here is methodological rather than principled: AOT is presented as a list of axioms over a relational, hyperintensional base logic, and crucial reasoning steps—e.g. moving between encoded and exemplified predication—are governed by axioms and rules for which contemporary automated theorem provers lack tailored calculi. By contrast, reasoning in the shallow embedding of HOML in HOL remains closer to reasoning in the meta-logic, so that the resulting proof obligations can be discharged more easily using the rich tool stack already availIn fact, for reasons of purity and to support reuse, applications of LogiKEy so far have always aimed to stay as close as possible to Church’s simple type theory as meta-logic, avoiding the use of additional built-in theories and mechanisms in Isabelle/HOL at the meta-logical layer wherever possible. 10 E.g. AOT distinguishes between modally-strict reasoning and reasoning from necessities that may be consequences of contingent axioms. 9
10
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto
able for classical HOL (resolution and superposition provers, SMT solvers, model finders, Sledgehammer, etc.). It is also worth noting that, as in PLM, foundational notions of mathematics—including their modalised counterparts—can be identified in HOL as analysable objects that arise naturally, without requiring additional axiomatic postulates (with the exception of an axiom of infinity). This is hinted at in lines 32–35 of Fig. 4, which follows Andrews’ textbook [1], from which these definitions and abbreviations are drawn; we refer the reader there for further details. A thorough formalisation of this material within the LogiKEy framework remains, of course, a task for future work.
3
Gödel’s Theory Extended with Mathematical Notions
Prior joint work with colleagues [5, 13] has formally established that the set of positive properties in Gödel’s framework constitutes a modal set ultrafilter—and it has introduced the necessary modal machinery (modalised filter and ultrafilter definitions) to do so rigorously within the HOL meta-logic via the LogiKEy methodology. This even includes the careful distinction between modal ultrafilters defined on intensions versus extensions of positive properties [5], and the distinction of actualist (varying domain) versus possibilist (constant domain) quantifiers in the involved postulates (see Fig. 2). Further mathematical notions will be required for the studies proposed here, covering foundational concepts such as natural numbers, equipollence, cardinality, and infinity. With these in place, one may investigate the formal effects of assuming such structures in interaction with Gödel’s modal ontological theory, thereby reflecting his nuanced realist stance. The remainder of this paper offers an illustration of this direction, graphically captured in Fig. 1; a full treatment is left for future work. 3.1
Shallow embedding of HOML in HOL
The starting point for our illustration is the shallow embedding of HOML in HOL, together with the definition of modal ultrafilters on top of it, in exactly the form used in [13, 14]. These encodings (extracted from [13]) are presented in Fig. 2 and Fig. 3, and they provide the embedding of HOML in HOL that is the basis for what follows below; the captions provide relevant information, and we refer the reader to [13] for full details. 3.2
Church’s postulates at the HOML layer
Building on the embedding of HOML in HOL, Fig. 4 (lines 6–17) presents a study of the modalised versions of core postulates of Church’s Type Theory [21, 4],11 an axiom system for HOL. The postulates of Church are lifted to the 11
Description and Choice are still left out here, but could easily be added.
Many Logics, One Methodology
11
Fig. 2. Shallow embedding of higher-order modal logic (HOML) in the classical higherorder logic (HOL) of Isabelle/HOL utilizing the LogiKEy methodology. Reader’s guide: ι is the type of (possibly non-actual) individuals, µ the type of worlds, and o the HOL Booleans; the abbreviations σ := µ → o and τ := ι → σ collect world-relativised propositions and world-relativised (individual) properties, respectively (occurrences of (ι → σ) in the figure may be read as τ ). HOML connectives are introduced as definitions on σ: negation, implication, and the other propositional connectives are taken world-wise, and the box □ is universal quantification over accessible worlds via the relation r : µ → µ → o. existsAt: ι → µ → o (line 35) specifies which entities exist at which worlds and underwrites the actualist quantifiers ∀E and ∃E , in contrast to the possibilist quantifiers ∀ and ∃ that range over the entire type. Two notions of equality appear: HOL identity = on the underlying carrier, and Leibniz equality ≡, defined as the modalised statement that every property holding of one argument holds of the other. Global validity Mvalid φ abbreviates ∀w. φ w, the criterion under which HOML formulas are taken as theorems. Lines 12 and 13, postulating the axioms Rrefl, Rsymm and Rtrans—the only axioms introduced—configure the accessibility relation r; making all three available, as here, specialises HOML to a higher-order analogue of modal logic S5, while subsets of these axioms recover modal logics K, T, S4, etc.
12
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto
Fig. 3. Set filter and ultrafilter formalised for our modal logic setting. The types here can be read off as follows: a modal set is a world-relativised predicate of type τ (so it picks out, at each world, a subset of individuals), and a modal set of modal sets accordingly has type τ → σ. With this typing, Subset relates two modal sets (the inclusion is required to hold at every world), whereas Element relates a modal set to a modal set of modal sets—the difference in the two relations is forced by the difference in types and is exactly the modal analogue of the standard ⊆ versus ∈ distinction.
Fig. 4. Modalised versions of core (schematic) postulates of Church’s Type Theory are proven as lemmata, and further modalised mathematical notions are provided as naturally embedded and analysable concepts in HOL. Two notes may help to read the figure. First, CardinalNumbers (line 26) holds of a (modal) collection u when u is the equipollence class of some witness p. Second, the successor operator S on cardinals (line 33) is not a Church-numeral, fold-style definition: given a cardinal u, S u is the cardinal of p ∪ {∗} for some witness p of u and a fresh element ∗—the standard Cantor– Bernstein successor in modal-set form.
Many Logics, One Methodology
13
HOML layer and formulated as lemmata. All of these lemmata are shown to be derivable in HOML from the principles of the underlying meta-logic HOL—with one exception: the non-trivial direction of Boolean extensionality, i.e. the lemma corresponding to Church’s axiom Ax7σ (Fig. 4, line 15). This is to be expected, since blocking Boolean extensionality is precisely the point of modal logic: unrestricted Boolean extensionality would permit arbitrary substitution of logically equivalent formulas even within the scope of modal operators, which is what modal logic is designed to prevent. Boolean extensionality can, however, be recovered in HOML under certain constraints. One option is to restrict the lemma to a particular fixed world—for instance, the actual world.12 A more drastic option, also illustrated here, is to establish Boolean extensionality for the degenerate case in which only a single world is assumed—a condition that would ultimately collapse the embedded HOML object-logic into full alignment with the meta-logic HOL.13 The above thus demonstrates that Church’s prominent postulates for HOL are, with the expected exceptions, valid also for the embedded—and pragmatically more expressive—logic HOML. In principle, one could now proceed to encode and prove (largely automatically) the stepwise development of the foundations of higher-order logic and mathematics as carried out with great precision in Andrews’ textbook [1]; see Fig. 5 below for an illustration. 3.3
Modalised mathematical notions in HOML
In Fig. 4, however, we proceed differently. First, we use Isabelle’s model finder Nitpick at the HOL meta-level to confirm the consistency of our development so far by generating a model; see line 19. Alternative formulations of consistency statements are shown in lines 20 and 21. All of these are of course entirely trivial, as the reader may readily observe: no axiom whatsoever—except for Rrefl, Rsymm and Rtrans—has been introduced in the embedding of HOML Since the embedding of HOML in HOL has access to the underlying Kripke structures at the HOL meta-layer, fixing and referring to particular worlds can be encoded straightforwardly (and has been done in prior work); the LogiKEy embedding technique thus scales naturally to hybrid logic. 13 One could reasonably object that the OneWorld hypothesis ought not to be needed at all to recover the non-trivial direction of Boolean extensionality at the HOML level. That it genuinely is needed can be seen from a countermodel that Nitpick returns once the OneWorld assumption is omitted. With a domain of two worlds i1 , i2 and the total accessibility relation R (so that every world sees every world), take φ to be false at both worlds and ψ to be false at i1 but true at i2 , and evaluate at w = i1 . At w = i1 the lifted equivalence φ ↔ ψ holds, since both φ and ψ are false there; yet φ and ψ differ at i2 , so the HOL identity φ = ψ—which requires agreement at every world—fails. The lifted equivalence is, by design, only a world-relativised statement asserting agreement at the world of evaluation, and the local hypothesis it supplies at any single w is therefore strictly weaker than the global HOL identity it is being asked to support. Once the carrier of worlds is collapsed to a single world by OneWorld, “every world” and “the given w” coincide, and the lemma goes through. 12
14
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto
in HOL. Instead, the embedding shows, using definitions (resp. abbreviations) alone, that HOML can be identified as a substructure already naturally present within the meta-logic HOL.14 This embedding of HO(M)L in HOL could of course be iterated further, giving rise to multiple reflection layers of embedded expressive logics within HOL—with the effect that each embedded object-logic remains open to formal study at its respective meta-level. More relevant for the purposes of this paper, however, is the content presented from line 23 of Fig. 4 onward: an encoding of modalised variants of mathematical notions relevant to the work envisioned ahead. These include equipollence, cardinality, cardinal numbers, alternative notions of infinity, natural numbers, and finiteness; for details on these notions we refer the reader to Andrews’ textbook [1]. Importantly, all of these mathematical notions are introduced purely as definitions—or more precisely, as abbreviations for λ-terms in HOL—and thus require no additional axioms.
3.4
Cardinality of positive properties
Using the material introduced above, further experiments with Gödel’s modal ontological argument are now possible, providing evidence for the effect mentioned earlier: namely, that assumptions about the existence of certain entities—mathematical ones, for instance—bear directly on the cardinality of the set of positive properties in Gödel’s modal ontological theory. This is illustrated in Fig. 6, starting from line 39. Lines up to 38 reproduce the experiments from Fig. 7 in [13] (with some interactive steps omitted for brevity), presenting a successful verification of the original version of Gödel’s modal ontological argument as outlined in his 1970 manuscript [22]. Lines 39– 47 then show that assuming two existing entities within Gödel’s theory yields two distinct positive properties; three existing entities yield four distinct positive properties; and so on.
3.5
Uncountability via a modal Cantor argument
This line of reasoning is then extended to the infinite case. From line 48 onward, we verify that infinitely many distinct entities imply infinitely many distinct 14
Concretely, propositions of type σ := µ → o are simply the world-indexed subsets of the (HOL) carrier of worlds. The set of positive properties, viewed as a filter, can in fact be given a topological reading: under suitable closure conditions (e.g. closure under arbitrary conjunctions and finite disjunctions) it forms a topology, and the modal ultrafilter perspective on Gödel’s axioms (cf. [5, 13] for the underlying filter/ultrafilter structure) then aligns with a familiar order-theoretic, indeed topological, picture—positive properties as “large” sets, modal necessity as a closure operator. This is a useful organising image rather than a load-bearing technical claim in the present paper, and the reader who prefers to read past it may safely take the embedding simply as world-indexed subsets of HOL.
Many Logics, One Methodology
15
Fig. 5. Checking/verifying parts of Andrews’ textbook [1] at the layer of HOML; the development is useful also for educational purposes. (This formalisation of Andrews’ development is exploratory and partial: it is intended to illustrate the approach rather than to provide a complete treatment, which is left for an extended version of this paper.)
16
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto
Fig. 6. The verification of Gödel’s original modal ontological argument [22] from [13], enriched by a preliminary study on the cardinality of positive properties under the assumption of different existing (e.g., mathematical) entities.
Many Logics, One Methodology
17
positive properties, as expected.15 Using a modalised and suitably constrained variant of the surjective Cantor theorem, we then strengthen this result and prove that the resulting infinite set of positive properties is in fact uncountable. The variant of Cantor’s theorem used can be stated informally as follows: there is no surjective mapping F from the set e of entities into the set P of (modalised) positive properties (over entities). The corresponding theorem statement CantorArgument appears in Fig. 6, line 89, which depends on the crucial lemma L1. Note that the construction of the diagonal set, extracted here as an explicit definition D which is used in the automated proof of lemma L1, is related to but significantly more involved in comparison to the standard proof (cf. [13, Fig.2] and [25]) of the surjective Cantor argument. Concretely, we show—and formally verify in Isabelle/HOL—that assuming an infinite domain of entities, together with Gödel’s axioms, gives rise to infinitely many—indeed uncountably many—distinct positive properties. The next step in this project is to examine Gödel’s generalised, third-order axiom Ax1Gen (Fig. 6, line 20) and its implications for the cardinality considerations of the present study—in particular the case where properties, viewed as mathematical objects, are themselves treated as existing entities. This line of inquiry will, however, inevitably encounter challenges arising from the hierarchy of simple types underlying HOL. To state the objective of this work in more abstract terms: when the mathematical realist Gödel assumes that the objects of mathematics exist, then this rules out trivial finite and countable interpretations of positive properties—and with them, any finitely grounded or countable conception of God-likeness in his theory; cf. also [27]. In this ongoing work, the LogiKEy methodology again plays a central role, enabling systematic variation of the precise HOML under consideration—encompassing, for instance, variations between actualist and possibilist quantifiers, or between intensional and extensional interpretations of positive properties.
4
Conclusion
This position paper has reflected on the potential of combining logical pluralism with the LogiKEy shallow embedding methodology as a unifying framework for the computer-assisted study of foundational questions in mathematics, 15
Our automated Isabelle proof of InfPosSet (Fig. 6, line 79) establishes the existence of infinitely many distinct positive properties by reasoning at the HOL meta-layer about the HOML embedding—an injection from the natural numbers into the entities is mapped into pairwise distinct positive properties, and the resulting obligations are discharged via auxiliary lemmata (lines 59, 66, and 72) that connect to the theory of natural numbers at the meta-layer—rather than arguing entirely inside the embedded HOML layer, using only our modalised mathematics and the lifted Church postulates. There is nothing wrong with this proof in principle—it arguably illustrates a virtue of LogiKEy—but constructing an additional, pure HOML-level proof remains interesting future work.
18
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto
metaphysics, and theology. By embedding HOML in HOL, we have provided evidence that Church’s postulates for HOL carry over, with one expected and wellunderstood exception, to the modal setting, and that Gödel’s modal ontological argument, extended with modalised mathematical notions naturally contained in HOL as analysable objects, can be studied with considerable formal precision and a useful degree of automation. Our experiments further suggest that Gödel’s mathematical realism may have direct and precise formal consequences: the assumption of mathematical entities forces the cardinality of positive properties beyond any finite and countable bound, with potentially far-reaching implications for the notion of God-likeness at the heart of his theory. The LogiKEy methodology has proven valuable throughout, enabling systematic variation of underlying logics and supporting (relative) consistency checking. A particularly promising methodological extension—hinted at in Sect. 2—is the integration of the deep-and-shallow embedding methodology recently developed for propositional and first-order modal logic [2, 6] into the HOML-based investigations pursued here: this would give the cardinality theorems on positive properties not only a mechanically verified semantic statement, but also a syntactic, deepembedded counterpart; adequacy between the two would then be formally established as a theorem of HOL. Consolidating these findings, extending the analysis further, and maintaining careful attention to relative consistency constitute the central tasks ahead—with the broader aim of contributing to a rigorous, tool-supported dialogue between (meta-)logic, mathematics, metaphysics, and theology. Acknowledgements. We thank the reviewers for their valuable comments, which significantly improved this paper. We are also grateful to all LogiKEy collaborators over the past two decades, in particular the co-authors of the referenced papers. Special thanks go to Ed Zalta for fruitful discussions and to Dana Scott for his collaboration on [13]. We also thank Claude.ai for dialogs that helped improve the paper and shorten the novel proofs in Fig. 6. The work of Luca Pasetto is supported by the Luxembourg National Research Fund (FNR) (INTER/DFG/23/17415164/LODEX).
References [1] [2]
[3]
P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Second. Kluwer Academic Publishers, 2002. C. Benzmüller. “Faithful Logic Embeddings in HOL – Deep and Shallow”. In: Automated Deduction – CADE-30 – 30th International Conference on Automated Deduction, Proceedings. Ed. by C. Barrett and U. Waldmann. Vol. 15943. LNCS. Preprint: arXiv:2502.19311. Springer, 2025, pp. 280–302. doi: 10.1007/978-3031-99984-0_16. C. Benzmüller. “Universal (Meta-)Logical Reasoning: Recent Successes”. In: Science of Computer Programming 172 (2019), pp. 48–62. doi: 10.1016/j.scico. 2018.10.008.
Many Logics, One Methodology [4]
[5]
[6] [7]
[8]
[9] [10]
[11] [12] [13] [14]
[15] [16]
[17]
19
C. Benzmüller and P. Andrews. “Church’s Type Theory”. In: The Stanford Encyclopedia of Philosophy. Ed. by E. N. Zalta and U. Nodelman. Spring 2024. Metaphysics Research Lab, Stanford University, 2024. url: https : / / plato . stanford.edu/archives/spr2024/entries/type-theory-church/. C. Benzmüller and D. Fuenmayor. “Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel’s Ontological Argument”. In: Bulletin of the Section of Logic 49.2 (2020), pp. 127–148. doi: 10.18778/0138-0680.2020.08. C. Benzmüller and D. Kirchner. “First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness”. In: Submitted. 2026. C. Benzmüller, X. Parent, and L. van der Torre. “Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support”. In: Artificial Intelligence 287 (2020), p. 103348. doi: 10 . 1016 / j . artint.2020.103348. C. Benzmüller and L. C. Paulson. “Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II”. In: Reasoning in Simple Type Theory — Festschrift in Honor of Peter B. Andrews on His 70th Birthday. Ed. by C. Benzmüller, C. Brown, J. Siekmann, and R. Statman. Studies in Logic, Mathematical Logic and Foundations. College Publications, 2008, pp. 386–406. url: http://www.collegepublications.co.uk/logic/mlf/?00010. C. Benzmüller and L. C. Paulson. “Multimodal and Intuitionistic Logics in Simple Type Theory”. In: The Logic Journal of the IGPL 18.6 (2010), pp. 881–892. doi: 10.1093/jigpal/jzp080. C. Benzmüller and L. C. Paulson. Quantified Multimodal Logics in Simple Type Theory. Tech. rep. DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str. 5, D–28359 Bremen, Germany: Saarland University, 2009. doi: 10.48550/arXiv.0905.2435. C. Benzmüller and L. C. Paulson. “Quantified Multimodal Logics in Simple Type Theory”. In: Logica Universalis (Special Issue on Multimodal Logics) 7.1 (2013), pp. 7–20. doi: 10.1007/s11787-012-0052-y. C. Benzmüller and D. S. Scott. “Automating Free Logic in HOL, with an Experimental Application in Category Theory”. In: Journal of Automated Reasoning 64.1 (2020), pp. 53–72. doi: 10.1007/s10817-018-09507-7. C. Benzmüller and D. S. Scott. “Notes on Gödel’s and Scott’s Variants of the Ontological Argument”. In: Monatshefte für Mathematik 208 (2025), pp. 569– 611. doi: 10.1007/s00605-025-02078-x. C. Benzmüller and D. S. Scott. “Notes on Gödel’s and Scott’s Variants of the Ontological Argument (Isabelle/HOL dataset)”. In: Archive of Formal Proofs (2025). url: https : / / www . isa - afp . org / entries / Notes _ On _ Goedels _ Ontological_Argument.html. C. Benzmüller, N. Sultana, L. C. Paulson, and F. Theiss. “The Higher-Order Prover LEO-II”. In: Journal of Automated Reasoning 55.4 (2015), pp. 389–404. doi: 10.1007/s10817-015-9348-y. C. Benzmüller, F. Theiss, L. C. Paulson, and A. Fietzke. “LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic (System Description)”. In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Proceedings. Ed. by A. Armando, P. Baumgartner, and G. Dowek. Vol. 5195. LNCS. Springer, 2008, pp. 162–170. doi: 10.1007/978-3-540-71070-7_14. C. Benzmüller and B. Woltzenlogel Paleo. “Automating Gödel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers”. In:
20
[18]
[19] [20] [21] [22] [23] [24] [25]
[26]
[27]
[28] [29] [30] [31] [32] [33]
Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto ECAI 2014. Ed. by T. Schaub, G. Friedrich, and B. O’Sullivan. Vol. 263. Frontiers in Artificial Intelligence and Applications. IOS Press, 2014, pp. 93–98. doi: 10.3233/978-1-61499-419-0-93. C. Benzmüller and B. Woltzenlogel Paleo. “Interacting with Modal Logics in the Coq Proof Assistant”. In: Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings. Ed. by L. D. Beklemishev and D. V. Musatov. Vol. 9139. LNCS. Springer, 2015, pp. 398–411. doi: 10.1007/978-3-319-20297-6_25. C. Benzmüller and B. Woltzenlogel Paleo. “The Inconsistency in Gödel’s Ontological Argument: A Success Story for AI in Metaphysics”. In: IJCAI 2016. Ed. by S. Kambhampati. Vol. 1-3. AAAI Press, 2016, pp. 936–942. Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development. Springer, 2004. A. Church. “A Formulation of the Simple Theory of Types”. In: Journal of Symbolic Logic 5.2 (1940), pp. 56–68. doi: 10.2307/2266170. K. Gödel. “Appendix A: Notes in Kurt Gödel’s Hand”. In: Logic and Theism. Ed. by J. Sobel. Cambridge University Press, 1970, pp. 144–145. D. Kirchner. “Computer-Verified Foundations of Metaphysics and an Ontology of Natural Numbers in Isabelle/HOL”. PhD thesis. Freie Universität Berlin, 2022. doi: 10.17169/refubium-35141. K. Lambert. “The Definition of E(xistence)! in Free Logic”. In: Abstracts: The International Congress for Logic, Methodology and Philosophy of Science. Stanford U. Press, 1960. F. W. Lawvere. “Diagonal Arguments and Cartesian Closed Categories with Author Commentary”. In: Reprints in Theory and Applications of Categories 15 (2006). Reprint, with commentary, of the 1969 original (Lecture Notes in Mathematics, vol. 92, Springer), pp. 1–13. url: http : / / www . tac . mta . ca / tac / reprints/articles/15/tr15abs.html. L. de Moura and S. Ullrich. “The Lean 4 Theorem Prover and Programming Language”. In: Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Proceedings. Ed. by A. Platzer and G. Sutcliffe. LNCS. Springer, 2021, pp. 625–635. doi: 10.1007/978-3-030-79876-5_37. C. Mühlenbeck and C. Benzmüller. “On the maximality of positive properties and modal collapse in variants of Gödel’s ontological proof of God”. In: Logic and Logical Philosophy (2026), pp. 1–21. doi: 10.12775/LLP.2026.007. url: https://apcz.umk.pl/LLP/article/view/55901. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Vol. 2283. LNCS. Springer, 2002. doi: 10.1007/3-54045949-9. S. Obua. “Partizan Games in Isabelle/HOLZF”. In: Theoretical Aspects of Computing – ICTAC 2006. Vol. 4281. LNCS. Springer, 2006, pp. 272–286. doi: 10. 1007/11921240_19. L. C. Paulson. “Isabelle: The Next 700 Theorem Provers”. In: CoRR cs.LO/9301106 (1993). url: https://arxiv.org/abs/cs/9301106. L. C. Paulson. ZFC in HOL. Archive of Formal Proofs. 2019. G. Russell and C. Blake-Turner. “Logical Pluralism”. In: The Stanford Encyclopedia of Philosophy. Ed. by E. N. Zalta and U. Nodelman. Fall 2023. Metaphysics Research Lab, Stanford University, 2023. D. Scott. “Appendix B: Notes in Dana Scott’s Hand”. In: Logic and Theism. Ed. by J. Sobel. Cambridge University Press, 1972, pp. 145–146.
Many Logics, One Methodology [34]
[35] [36] [37]
[38] [39] [40] [41]
21
D. Scott. “Existence and description in formal logic”. In: Bertrand Russell: Philosopher of the Century. Ed. by R. Schoenman. (See also: Philosophical Application of Free Logic, edited by K. Lambert. Oxford:OUP, 1991, pp. 28 - 48). George Allen & Unwin, London, 1967, pp. 181–200. A. Steen and C. Benzmüller. “Extensional Higher-Order Paramodulation in LeoIII”. In: Journal of Automated Reasoning 65.6 (2021), pp. 775–807. doi: 10 . 1007/s10817-021-09588-x. A. Steen, G. Sutcliffe, and C. Benzmüller. “Solving Quantified Modal Logic Problems by Translation to Classical Logics”. In: Journal of Logic and Computation 35.4 (2025), pp. 1–23. doi: 10.1093/logcom/exaf006. The mathlib Community. “The lean mathematical library”. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2020. New Orleans, LA, USA: Association for Computing Machinery, 2020, pp. 367–381. doi: 10.1145/3372885.3373824. E. N. Zalta. Abstract Objects: An Introduction to Axiomatic Metaphysics. Vol. 160. Synthese Library. Dordrecht, Boston, and Lancaster: D. Reidel Publishing Company, 1983, pp. xiii + 193. E. N. Zalta. Intensional Logic and the Metaphysics of Intentionality. Bradford Books. Cambridge, MA: The MIT Press, 1988, pp. xiii + 256. E. N. Zalta. “Principia Logico-Metaphysica (Draft/Excerpt)”. Available at https://mally.stanford.edu/principia.pdf [accessed 24-May-2026]. 2026. E. N. Zalta. “Unifying and Validating Some Ideas of Kurt Gödel”. Awarded contribution to the 2025 Kurt Gödel Essay Prize; available online at https : //tinyurl.com/35t36nvz [accessed 26-May-2026]. 2025.