Intuitionistic Derivability in Anderson’s Variant of the Ontological Argument Annika Kanckos1 1 Department of Philosophy, P.O.Box. 24, 00014 Helsinki University, Finland Abstract Anderson’s emendation [1] of Gödel’s ontological proof is known as a variant that does not entail modal collapse, that is, derivability of 𝐮 ↔ l𝐮 ↔ ♩𝐮 for all formulas 𝐮. This variant of the axiomatization is here investigated as a case study of intuitionistic derivability using natural deduction. The formal system đ» 𝑂𝑀𝐿𝑖 presented for higher-order modal logic simulates a varying domain semantics in the domain of objects in a manner that seems to have been intended by Anderson. The objects (numbers) are separate from the individuals of higher type and may occur in the existence predicate 𝐾 (figure 2). Intuitionistic derivability is shown to be limited because âˆƒđ‘„.đșpđ‘„q (i.e. x is a godlike individual of the base type) is not derivable. The classical proof of â™Šâˆƒđ‘„.đșpđ‘„q, can be compared to the compatibility argument of Leibniz or Scott’s version that uses a form of indirect proof. Keywords Higher-order Modal Logic, Intuitionistic Logic, Minimal Logic, Consistency, Ontological Argument 1. Introduction Anselm of Canterbury’s ontological proof is a proof of the existence of a maximal being, identified as God, that possesses all perfections or positive properties in the terminology of Gödel. Gödel’s ontological proof is a formal axiomatization of St. Anselm’s proof of the necessary existence of God. In its original 1970-version [12] it provides definitions, axioms, and provable theorem within a theory for higher-order modal logic. Because the axioms quantify over positive properties the theory within which the proof can be formalised requires a higher order logic in addition to the modal operators. The proof defines a predicate as the conjunction of all positive properties and concludes that this property is necessarily inhabited if it is inhabited at all, but also the possible inhabitation of the predicate is derivable. Thus, it derives the necessary inhabitation of the predicate unconditionally by standard modal principles (such as 𝑆5 or potentially some weaker theory), in other words, the existence of God. The ontological proof nowadays refers to a collection of versions for formal axiomatiza- tions in higher order modal logic where a predicate đșpđ‘„q (interpreted as đ‘„ is godlike) is necessarily inhabited. Gödel’s proof is inspired by Anselm of Canterbury, with modifi- cations by Leibniz, and distinctly more complex than the modern ontological proof of ARQNL 2022: Automated Reasoning in Quantified Non-Classical Logics, 11 August 2022, Haifa, Israel Envelope-Open annika.kanckos@helsinki.fi (A. Kanckos) Orcid 0000-0003-3959-3547 (A. Kanckos) © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 Inter- national (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) ARQNL 2022 46 CEUR-WS.org Hartshorne (see [16], [18], and [27]). The original proof by Gödel dated Feb 10, 1970 has been published in [13] and [25] where the axioms, definitions and theorems of the original ontological proof are stated. A version of the proof based on conversations with Gödel by Dana Scott is published side by side with Gödel’s original notes in [23]. The former 1970-proof can be considered to be Gödel’s last version though his work on the ontological proof developed earlier in many forms [17]. A much debated issue concerning the proof is that the axioms may lead to a so-called modal collapse [20, 26]. Modal collapse occurs if a formula, its necessitation, as well as its possibility are equiderivable. đ» 𝑂𝑀𝐿 ` Gödel’s axioms ⊱ 𝐮 ↔ l𝐮 ↔ ♩𝐮 The subtle differences between a formal system where the modals retain their meaning and a theory that implies modal collapse give a hint of the exceptional status of the formula âˆƒđ‘„.đșpđ‘„q that states the existence of a godlike individual of the base type. The modal collapse was first noticed by Jordan Howard Sobel [24], [25] and since then emendations of Gödel’s proof have been made in order to prevent the modal collapse. Therefore, several emendations of the axioms exist at least partially motivated by the modal collapse [1, 2, 7, 8], but also restrictions of the comprehension principle have been investigated [14, 15], and in [10] intentional versus extensional versions of the quantification provides another solution to the modal collapse. The emendation of Anderson [1] spurred a controversy between HĂĄjek and Anderson [6] where the emendation was claimed to have superfluous axioms, a claim that was later retracted, because the superfluous axioms were thought to be relevant within a varying domain semantics [9] as opposed to the simpler constant domain semantics. The claims were later settled by a computer assisted investigation [6] concluding that axioms (A4) and (A5) of Andersons variant are indeed redundant, because they are derivable, also within a varying domain setting. The computer assisted analysis of the available ontological arguments is by now a well-established method for developing tools for higher-order modal logic [4, 22]. These investigations have so far focused on questions, such as, consistency of the axiomatizations [5] and strength of the modal principles necessary for each variant [19]. In this article I wish to take the investigation of the ontological proof one step further by considering the argument in a formal intuitionistic system with the purpose of following up the successful computer assisted analysis of this particular axiomatization in [6]. The emendation of Anderson will serve as a case study of the ontological argument in an intuitionistic system of natural deduction. We will simulate varying domains (see [10, pp. 89–90] for a motivation) with an external existence predicate 𝜔 ∶ 𝐾pđ‘„q which holds if the object đ‘„ exists in the world 𝜔. The predicate is utilized in the first-order quantification such that âˆ€đ‘„.𝐮pđ‘„q can only be introduced if 𝐾pđ‘„q → 𝐮pđ‘„q is derivable for an eigenvariable đ‘„. Similarly, the existential quantification âˆƒđ‘„.𝐮pđ‘„q is derivable only if the conjunction 𝐾p𝑡q ∧ 𝐮p𝑡q is derivable for some 𝑡. The system for higher-order modal logic simulates a varying domain semantics on the domain of individuals of the base type in a manner that seems to have been intended by Anderson. This case study takes the analysis of [6] to an 47 intuitionistic theory and can be the base for a computer assisted analysis in intuitionistic higher order modal logic. As will be shown the intuitionistic derivability is in general limited to conditional statements where đșpđ‘„q is assumed, whereas the derivability of đșpđ‘„q itself is proved to be impossible if the formal system presented for higher-order modal logic is consistent. This shows that the classical proof for â™Šâˆƒđ‘„.đșpđ‘„q of Scott’s variant is not circumventable. This may not be a surprise because already a straightforward formal analysis of Leibniz argument could be considered to have a classical component (see for example [10, pp. 137–138]). 2. The formal system for intuitionistic higher-order modal logic We will present a formal system for intuitionistic higher-order modal logic đ» 𝑂𝑀𝐿𝑖 where the classical rule for indirect proof (reductio ad absurdum) has been suppressed. The propositional rules of (figure 1) is for a system without disjunction. The modal axioms of (figure 3) are based on [19]. The quantifier rules of (figure 2) are adapted to varying domains for the individuals of the base type (the natural numbers) which depend on the existence predicate. For the higher types the quantifier rules do not have any dependence on existence of objects of the base type in any particular world. Because the natural deduction in [19] is constructed with constant domains for each possible world, it is as such insufficient for treating Anderson’s emendation if the intended varying domain approach is accepted as a prerequisite for axiomatization. Due to the naturalness of reasoning and its close relation to standard theorem provers we will use an adopted natural deduction that simulates varying domains with an additional existence predicate 𝜔 ∶ 𝐾pđ‘„q, that corresponds to existence of the object đ‘„ in the world 𝜔. For another kind of formal treatment of varying domains in a proof system for Gödel’s ontological proof I refer to the tableaux-style proofs in [10]. In the formal system defined below, đ» 𝑂𝑀𝐿𝑖 , for intuitionistic higher-order modal logic we take disjunction, negation and equivalence to be defined concepts. We have negation ¬𝐮 ≡ 𝐮 → ⊄ and equivalence 𝐮 ↔ đ” ≡ p𝐮 → đ”q ∧ pđ” → 𝐮q. The formal system đ» 𝑂𝑀𝐿𝑖 consists of a propositional part, quantification that we treat differently for individuals and higher-order respectively, and modal rules as well as modal axioms. 𝐮 đ” âˆ§đŒ 𝐮 ∧ đ” ∧𝐾 𝐮 ∧ đ” ∧𝐾 1 2 đŽâˆ§đ” 𝐮 đ” r𝐮s𝑛 .. .. ⊄ âŠ„đž đ” â†’đŒ ,𝑛 𝐮 𝐮 → đ” →𝐾 𝐮 đŽâ†’đ” đ” Figure 1: Propositional rules Characteristic for the intuitionistic system is that we do not have the classically valid interdefinability of connectives, quantifiers, and modal operators. However, the 48 disjunction rules have been suppressed due to formal reasons in theorem (8) where permutation conversions would otherwise be needed. To derive a statement in the intuitionistic setting we require a direct proof. However, we will not prove structural properties, such as normalization or the disjunction property, which are usually the basis for proving that the system is indeed constructive. As it turns out normalization is however tacitly required for the unprovability results of section (6). 𝐾pđ›Œ0 q → 𝐮pđ›Œ0 q âˆ€đ‘„.𝐮pđ‘„q 𝐾p𝑡q ∧ 𝐮p𝑡q âˆƒđ‘„.𝐮pđ‘„q âˆ€đŒ ∀𝐾 âˆƒđŒ ∃𝐾 âˆ€đ‘„.𝐮pđ‘„q 𝐾p𝑡q → 𝐮p𝑡q âˆƒđ‘„.𝐮pđ‘„q 𝐾pđ›œ0 q ∧ 𝐮pđ›œ0 q 𝐮pđ›Œq ∀𝜓 .𝐮p𝜓q 𝐮p𝜑q ∃𝜓 .𝐮p𝜓q âˆ€đŒ ∀𝐾 âˆƒđŒ ∃𝐾 ∀𝜓 .𝐮p𝜓q 𝐮p𝜑q ∃𝜓 .𝐮p𝜓q 𝐮pđ›œq Eigenvariable condition: In an ∀-introduction inference the eliminated variable đ›Œ must not have been introduced by any ∃-elimination inference; In an ∃-elimination inference the introduced variable đ›œ must be eliminated in an ∃-introduction. Variable condition: The eigenvariables may not occur in the conclusion of the derivation. Type condition: The variables of âˆ€đŒ and âˆ€đŒ are distinct and similarly for ∃𝐾 and ∃𝐾. Figure 2: Quantifier rules Note, that the eigenvariable conditions are formulated in a standard top-down manner. Note also that the proof of this article depends on that the standard detour conversions for quantifiers hold. As modal axioms we allow the standard 𝑇 , đŸ , đ”, 4, 5 and do not intend to limit the modal part to any weak system less than 𝑆5 where all axioms are assumed. However, we will indicate the use of 𝑇 , đ”, 4, 5 in all the derivations to show the explicit modal dependence. The axiom đŸ is derivable in the system đ» 𝑂𝑀𝐿𝑖 . The following modal rules are required for an intuitionistic calculus where we take both l and ♩ as primitive. The lđŒ rule corresponds to the rule of conditional necessitation where we are allowed to assume necessitated formulas l𝐮1 , 
 , l𝐮𝑛 . If 𝑛 “ 0 we have the standard necessitation rule. Note that the eigen-box condition in the modal rules (fig. 3), have world labels đ‘€ or 𝜔 for an arbitrary world. We allow the degenerate inference 𝑇 of l𝐾 with 𝑣 ≡ đ‘€. The ♩-rules are dual, with â™ŠđŒ which due to the eigen-box condition is required to be accessed by one strong rule, which must be one occurrence of ♩𝐾 . The box-labels are either a specific label đ‘€ or an arbitrary box-label 𝜔. An assumption may be labelled by đ‘€ or 𝜔, but the latter label is only allowed in hypothetical reasoning where the assumption is discharged by implication introduction. If the label is absent, then we are reasoning in the actual world. 49 .. 𝑣 ∶ l𝐮 l .. 𝐾 đœ”âˆ¶ 𝐮 𝐮. lđŒ .. 𝑣 ∶ l𝐮 đ‘€âˆ¶ . .. 𝑣 ∶ ♩𝐮 .. ♩𝐾 đ‘€âˆ¶ 𝐮 𝐮. ♩ .. 𝑣 ∶ ♩𝐮 đŒ đœ”âˆ¶ . Eigen-box condition: lđŒ and ♩𝐾 are strong modal rules: 𝜔 must be a fresh label for the box they access and cannot be the label of the conclusion. Every box must be accessed by exactly one strong modal inference or 𝑣 ≡ đ‘€. Boxed assumption condition: Assumptions should be discharged within the box where they are created. Figure 3: Modal rules We can extend the modal system, which is so far a system for TK, with the following modal axioms that may also be converted into rules. Rules are produced by taking the antecedent of the axiom as a premise and the succedent of the implication as a conclusion. For the derivability of axiom K see [19, Theorem 1] and derivablity of 𝑇 is trivial. Concerning the two versions of Brouwer’s axiom, đ” and đ”Ëš , note the discussion on an axiom for symmetry in [11]. T l𝐮 → 𝐮 K lp𝐮 → đ”q → pl𝐮 → lđ”q B 𝐮 → l♩𝐮 B˚ ♩l𝐮 → 𝐮 4 l𝐮 → ll𝐮 5 ♩𝐮 → l♩𝐮 Figure 4: Modal axioms 3. Anderson’s emendation of the ontological proof The axioms for Anderson’s emendation [1] found in figure (5) are identical to one of the computer analyzed variants [6]. To the formal system đ» 𝑂𝑀𝐿 we add the axioms A1-A5 and also include in the language the predicates 𝑃 and đș for positive properties and God respectively. Thus, giving us the language for đ» 𝑂𝑀𝐿 ` đŽđ‘„. Anderson’s essence relation 𝜑𝐾𝑠𝑠𝐮 đ‘„ which states that the property variable 𝜑 is an essence of individual đ‘„, and necessary existence 𝑁 𝐾 are given a definition below. 50 A1 ∀𝜑.r𝑃p𝜑q → ¬𝑃p¬𝜑qs A2 ∀𝜑.∀𝜓 .rp𝑃p𝜑q ∧ lâˆ€đ‘„.p𝜑pđ‘„q → 𝜓pđ‘„qqq → 𝑃p𝜓qs D1 đșpđ‘„q ≡ ∀𝜑.r𝑃p𝜑q ↔ l𝜑pđ‘„qs A3 𝑃pđșq A4 ∀𝜑.r𝑃p𝜑q → l𝑃p𝜑qs D2 𝜑𝐾𝑠𝑠𝐮 đ‘„ ≡ ∀𝜓 .rl𝜓pđ‘„q ↔ l∀𝑩.p𝜑p𝑩q → 𝜓p𝑩qqs D3 𝑁 𝐾pđ‘„q ≡ ∀𝜑.r𝜑𝐾𝑠𝑠𝐮 đ‘„ → l∃𝑩.𝜑p𝑩qs A5 𝑃p𝑁 𝐾q Figure 5: Anderson’s emendation of the ontological proof. 4. Derivability of axioms A5 and A4 It can be shown that axiom A5 is derivable within the system if we assume A2 and A3. This is a known result of [6]. Axiom A2 makes it possible to generate new positivity statements that are necessarily derivable from the basic statement of positivity of 𝑃pđșq. Noteworthy is that as a subderivation we obtain necessary existence 𝑁 𝐾pđ‘„q derivable without any of the axioms 𝐮1 ÂŽ 𝐮5. However, to utilize the implication hidden behind the definition of 𝑁 𝐾pđ‘„q we essentially need to derive that some property is an essence of the individual đ‘„. Lemma 1. The formula 𝑁 𝐾pđ‘„q is derivable in đ» 𝑂𝑀𝐿𝑖 without using any of the axioms of section (3) if we are allowed to quantify over 𝐾 as a property. Proof. We can derive 𝑁 𝐾pđ‘„q without assumptions if we are allowed to quantify over 𝐾 as a property. 51 r𝜑p𝑩qs1 r𝐾p𝑩qs2 âˆ§đŒ 𝜑p𝑩q ∧ 𝐾p𝑩q â†’đŒ ,1 r𝜑𝐾𝑠𝑠𝐮 đ‘„s3 𝜑p𝑩q → p𝜑p𝑩q ∧ 𝐾p𝑩qq đ·đ‘’đ‘“ â†’đŒ ,2 ∀𝜓 .rl𝜓pđ‘„q ↔ l∀𝑩.p𝜑p𝑩q → 𝜓p𝑩qqs 𝐾p𝑩q → 𝜑p𝑩q → p𝜑p𝑩q ∧ 𝐾p𝑩qq ∀𝐾 âˆ€đŒ lp𝜑pđ‘„q ∧ 𝐾pđ‘„qq ↔ l∀𝑩.p𝜑p𝑩q → p𝜑p𝑩q ∧ 𝐾p𝑩qqq ∀𝑩.p𝜑p𝑩q → p𝜑p𝑩q ∧ 𝐾p𝑩qq ∧𝐾 lđŒ l∀𝑩.p𝜑p𝑩q → 𝜑p𝑩q ∧ 𝐾p𝑩qq → lp𝜑pđ‘„q ∧ 𝐾pđ‘„qq l∀𝑩.p𝜑p𝑩q → p𝜑p𝑩q ∧ 𝐾p𝑩qq →𝐾 lp𝜑pđ‘„q ∧ 𝐾pđ‘„qq l𝐾 𝜔 ∶ 𝜑pđ‘„q ∧ 𝐾pđ‘„q âˆƒđŒ 𝜔 ∶ âˆƒđ‘„.𝜑pđ‘„q lđŒ lâˆƒđ‘„.𝜑pđ‘„q â†’đŒ ,3 𝜑𝐾𝑠𝑠𝐮 đ‘„ → lâˆƒđ‘„.𝜑pđ‘„q âˆ€đŒ ∀𝜑.r𝜑𝐾𝑠𝑠𝐮 đ‘„ → lâˆƒđ‘„.𝜑pđ‘„qs đ·đ‘’đ‘“ 𝑁 𝐾pđ‘„q Lemma 2. The axiom 𝑃p𝑁 𝐾q is derivable in đ» 𝑂𝑀𝐿𝑖 with only the axioms A2 and A3 assumed if we are allowed to quantify over 𝐾 as a property. Proof. We can use lemma (1) with axioms A2 and A3 to derive the sought conclusion. .. .. 𝑁 𝐾pđ‘„q lđŒ l𝑁 𝐾pđ‘„q l𝐾 𝜔 ∶ 𝑁 𝐾pđ‘„q â†’đŒ 𝜔 ∶ đșpđ‘„q → 𝑁 𝐾pđ‘„q â†’đŒ 𝜔 ∶ 𝐾pđ‘„q → pđșpđ‘„q → 𝑁 𝐾pđ‘„qq âˆ€đŒ 𝜔 ∶ âˆ€đ‘„.pđșpđ‘„q → 𝑁 𝐾pđ‘„qq axiom 𝐮3 lđŒ 𝑃pđșq lâˆ€đ‘„.pđșpđ‘„q → 𝑁 𝐾pđ‘„qq axiom 𝐮2 𝑃p𝑁 𝐾q Note that in a constant domain setting the derivations of lemmas (1 & 2) could be even simpler. The other main derivability result of [6] related to Anderson’s emendation, that A4 is derivable, is also possible in an intuitionistic setting. Lemma 3. The axiom 𝑃p𝜑q → l𝑃p𝜑q is derivable in đ» 𝑂𝑀𝐿𝑖 if axioms A2 and A3 are assumed and if we are allowed to vacuously introduce an implication on 𝐾. 52 Proof. 𝜔2 ∶ rđșpđ‘„qs1 đ·đ‘’đ‘“ 𝜔2 ∶ ∀𝜑.r𝑃p𝜑q ↔ l𝜑pđ‘„qs ∀𝐾 𝜔2 ∶ 𝑃pđșq ↔ lđșpđ‘„q r𝑃p𝜑qs2 ∧𝐾 đ” 𝜔2 ∶ 𝑃pđșq 𝜔2 ∶ 𝑃pđșq → lđșpđ‘„q l♩𝑃p𝜑q →𝐾 p4q 𝜔2 ∶ lđșpđ‘„q ll♩𝑃p𝜑q l𝐾 𝜔3 ∶ đșpđ‘„q 𝜔1 ∶ l♩𝑃p𝜑q .. l𝐾 .. 𝜔2 ∶ ♩𝑃p𝜑q ♩𝐾 𝜔3 ∶ 𝑃p𝜑q → l𝜑pđ‘„q 𝜔3 ∶ 𝑃p𝜑q 𝜔3 ∶ l𝜑pđ‘„q â™ŠđŒ 𝜔2 ∶ ♩l𝜑pđ‘„q ˚ đ” 𝜔2 ∶ 𝜑pđ‘„q â†’đŒ ,1 𝜔2 ∶ đșpđ‘„q → 𝜑pđ‘„q â†’đŒ 𝜔2 ∶ 𝐾pđ‘„q → rđșpđ‘„q → 𝜑pđ‘„qs âˆ€đŒ 𝜔2 ∶ âˆ€đ‘„.rđșpđ‘„q → 𝜑pđ‘„qs lđŒ 𝜔1 ∶ 𝑃pđșq 𝜔1 ∶ lâˆ€đ‘„.rđșpđ‘„q → 𝜑pđ‘„qs axiom 𝐮2 𝜔1 ∶ 𝑃p𝜑q lđŒ l𝑃p𝜑q â†’đŒ ,2 𝑃p𝜑q → l𝑃p𝜑q 5. Conditional derivability results for the ontological argument We can derive further conditional statements relevant for the ontological proof. First, we obtain that đșpđ‘„q implies that đș is the essence of đ‘„. Theorem 4. The conditional statement âˆƒđ‘„.đșpđ‘„q → âˆƒđ‘„.pđș𝐾𝑠𝑠𝐮 đ‘„q is derivable in đ» 𝑂𝑀𝐿𝑖 . Proof. Note that lđșpđ‘„q is derivable from đșpđ‘„q as in the proof of lemma (3). Firstly, we let Π0 be the following subderivation: râˆƒđ‘„.đșpđ‘„qs3 đșpđ‘„q .. .. lđșpđ‘„q l𝐾 𝜔 ∶ đșpđ‘„q đ·đ‘’đ‘“ . 𝜔 ∶ ∀𝜓 .r𝑃p𝜓q ↔ l𝜓pđ‘„qs rl𝜓pđ‘„qs2 →𝐾 p4q 𝜔 ∶ 𝑃p𝜓q ↔ l𝜓pđ‘„q ll𝜓pđ‘„q ∧𝐾 l𝐾 𝜔 ∶ l𝜓pđ‘„q → 𝑃p𝜓q 𝜔 ∶ l𝜓pđ‘„q →𝐾 𝜔 ∶ 𝑃p𝜓q 53 Then, let Π1 be the following subderivation of one direction of the essence equivalence: 𝜔 ∶ rđșp𝑩qs1 rl𝜓pđ‘„qs2 , râˆƒđ‘„.đșpđ‘„qs3 .. .. .. .. Π0 𝜔 ∶ 𝑃p𝜓q → l𝜓p𝑩q 𝜔 ∶ 𝑃p𝜓q →𝐾 𝜔 ∶ l𝜓p𝑩q 𝑇 𝜔 ∶ 𝜓p𝑩q â†’đŒ ,1 𝜔 ∶ đșp𝑩q → 𝜓p𝑩q â†’đŒ 𝜔 ∶ 𝐾p𝑩q → rđșp𝑩q → 𝜓p𝑩qs âˆ€đŒ 𝜔 ∶ ∀𝑩.pđșp𝑩q → 𝜓p𝑩qq lđŒ l∀𝑩.pđșp𝑩q → 𝜓p𝑩qq â†’đŒ ,2 l𝜓pđ‘„q → l∀𝑩.pđșp𝑩q → 𝜓p𝑩qq â†’đŒ ,3 âˆƒđ‘„.đșpđ‘„q → rl𝜓pđ‘„q → l∀𝑩.pđșp𝑩q → 𝜓p𝑩qqs The other direction Π2 is similarly obtained: râˆƒđ‘„.đșpđ‘„qs2 .. .. 𝑃pđșq rl∀𝑩.pđșp𝑩q → 𝜓p𝑩qqs1 axiom 𝐮2 𝑃p𝜓q → l𝜓pđ‘„q 𝑃p𝜓q →𝐾 l𝜓pđ‘„q â†’đŒ ,1 l∀𝑩.pđșp𝑩q → 𝜓p𝑩qq → l𝜓pđ‘„q â†’đŒ ,2 âˆƒđ‘„.đșpđ‘„q → rl∀𝑩.pđșp𝑩q → 𝜓p𝑩qq → l𝜓pđ‘„qs We can easily combine the two directions into a derivation of our sought conclusion âˆƒđ‘„.đșpđ‘„q → đș𝐾𝑠𝑠𝐮 đ‘„ based on the definition of essence. râˆƒđ‘„.đșpđ‘„qs1 râˆƒđ‘„.đșpđ‘„qs1 .. .. .. .. l𝜓pđ‘„q → l∀𝑩.pđșp𝑩q → 𝜓p𝑩qq l∀𝑩.pđșp𝑩q → 𝜓p𝑩qq → l𝜓pđ‘„q âˆ§đŒ l𝜓pđ‘„q ↔ l∀𝑩.pđșp𝑩q → 𝜓p𝑩qq râˆƒđ‘„.đșpđ‘„qs1 âˆ€đŒ .. ∀𝜓 .rl𝜓pđ‘„q ↔ l∀𝑩.pđșp𝑩q → 𝜓p𝑩qs .. đ·đ‘’đ‘“ . đș𝐾𝑠𝑠𝐮 đ‘„ 𝐾pđ‘„q âˆ§đŒ 𝐾pđ‘„q ∧ đș𝐾𝑠𝑠𝐮 đ‘„ âˆƒđŒ âˆƒđ‘„.đș𝐾𝑠𝑠𝐮 đ‘„ â†’đŒ ,1 âˆƒđ‘„.đșpđ‘„q → đș𝐾𝑠𝑠𝐮 đ‘„ Theorem 5. The conditional statement âˆƒđ‘„.đșpđ‘„q → lâˆƒđ‘„.đșpđ‘„q is derivable in đ» 𝑂𝑀𝐿𝑖 . 54 Proof. Lem.1 .. theorem.4 .. .. .. 𝑁 𝐾pđ‘„q đ·đ‘’đ‘“ . râˆƒđ‘„.đșpđ‘„qs1 âˆƒđ‘„.đșpđ‘„q → đș𝐾𝑠𝑠𝐮 đ‘„ ∀𝜑.r𝜑𝐾𝑠𝑠𝐮 đ‘„ → lâˆƒđ‘„.𝜑pđ‘„qs →𝐾 ∀𝐾 đș𝐾𝑠𝑠𝐮 đ‘„ đș𝐾𝑠𝑠𝐮 đ‘„ → lâˆƒđ‘„.đșpđ‘„q →𝐾 lâˆƒđ‘„.đșpđ‘„q â†’đŒ ,1 âˆƒđ‘„.đșpđ‘„q → lâˆƒđ‘„.đșpđ‘„q 6. Intuitionistic unprovablity results We now turn our attention to the limitations of the intuitionistic calculus and statements that are not derivable. To be able to combinatorially analyse the proof structures of đ» 𝑂𝑀𝐿𝑖 ` Ax which denotes the system of đ» 𝑂𝑀𝐿𝑖 plus the axioms A1-A5 of figure (5), we extend the system of section (2) to an auxiliary system đ» 𝑂𝑀𝐿â€Č𝑖 ` Ax with the following composition rule. The composition rule is introduced to be able to eliminate implication detours (i.e. pairs of introduction and elimination rules) without increasing the length of the derivation. This auxiliary concept of composition allows us to define the induction measure proving nonprovability in theorem (8). The use of composition as and auxiliary concept is based on the work of Dag Prawitz. r𝐮pđ›Œqs1 .. .. .. .. đ”pđ›Œq 𝐮p𝜑q đ¶đ‘œđ‘šđ‘.,1 đ”p𝜑q Note that đ›Œ is an eigenvariable and 𝜑 is an arbitrary property. The rank of the composition is the rank of the discharged assumption 𝑟𝑘p𝐮pđ›Œqq. Figure 6: Admissible rule of composition We conclude that these two systems đ» 𝑂𝑀𝐿𝑖 ` Ax and đ» 𝑂𝑀𝐿â€Č𝑖 ` Ax are equally strong. Lemma 6. The rule of composition is derivable in the system đ» 𝑂𝑀𝐿𝑖 . Proof. Assuming that the premises of the composition rule are derivable we can derive the conclusion in đ» 𝑂𝑀𝐿𝑖 by an implication detour and substitution of 𝜑 for đ›Œ. Lemma 7 (Substitution of labels). We can substitute the labels of a box and eliminate a detour of the modal rules. 1. If we have a subderivation of 𝜔 ∶ 𝐮, derived without assumptions in đ» 𝑂𝑀𝐿â€Č𝑖 , and the given formula occurrence 𝜔 ∶ 𝐮 is followed by a lđŒ and l𝐾 concluding đ‘€ ∶ 𝐮, then we can substitute the label đ‘€ for 𝜔 and derive đ‘€ ∶ 𝐮 without the detour. 55 2. If we have a subderivation of đ‘€ ∶ 𝐮, derived without assumptions in đ» 𝑂𝑀𝐿â€Č𝑖 , and the given formula occurrence đ‘€ ∶ 𝐮 is followed by a â™ŠđŒ and ♩𝐾 concluding 𝜔 ∶ 𝐮, then we can derive the conclusion of the theorem, say 𝑣 ∶ đ” by eliminating the detour. Proof sketch. We sketch a proof for the two cases. 1. If 𝜔 ∶ 𝐮 is derivable and the premise of the rule lđŒ , in a derivation, then there is no other strong rule (♩𝐾 ) introducing the label 𝜔. Thus, the label can only be introduced by l𝐾 where the label is arbitrary or any leaf is a modal axiom or axiom 𝐮1 ÂŽ 𝐮5 which hold, in every world, and therefore for any label including đ‘€. 2. Let đ‘€ ∶ 𝐮 be followed by â™ŠđŒ and ♩𝐾 concluding 𝜔 ∶ 𝐮. Note that by the eigen-box conditions the label 𝜔 cannot be the label of the conclusion and ♩𝐾 is the only strong inference accessing the box with the label 𝜔. Thus, below the detour we must have a weak rule â™ŠđŒ that eliminates the eigen-label 𝜔. Because, â™ŠđŒ is a weak rule, we may eliminate the detour and substitute the label 𝜔 with đ‘€ for all occurrences of 𝜔 and still derive 𝑣 ∶ đ”. A more formal proof of the second case could be obtained by induction on the number of inferences below the detour. When we aim to prove some unprovability results we notice the following properties of the axioms. The axioms as presented in section (3) all are statements about positivity of formulas. Axioms A3 and A5 conclude the positivity of properties. Axioms A2 and A4 respectively state an implication with the succedent a positivity statement or the necessity of a positivity statement. Therefore, if these axioms are used as the major premise in an elimination rule, then we can only conclude positivity statements. Similarly, axiom A1 concludes the negation of a positivity statement. We consider negation defined by implication of falsity, so if the axiom is used as a major premise in elimination rules, then we must have derivations of both 𝑃p𝜑q and 𝑃p¬𝜑q which make ⊄ derivable using axiom A1. This cannot be the case if we assume the system to be consistent. We summarize these observations in the proof of the following theorem. Theorem 8. If the system of đ» 𝑂𝑀𝐿â€Č𝑖 ` Ax is consistent, then the formula âˆƒđ‘„.đșpđ‘„q is not derivable. Proof. Assume that âˆƒđ‘„.đșpđ‘„q is derivable in đ» 𝑂𝑀𝐿â€Č𝑖 ` Ax with a derivation Π. Let there be conjectured a tentative measure that decreases with weak normalization. Namely, a reduction in the thread beginning with the conclusion and tracing up through major premises, is assumed to decrease the measure. We prove that there is a derivation of âˆƒđ‘„.đșpđ‘„q with a lower number as given by the conjectured inductive measure 𝑀pΠq. Base case. Note as the base case that âˆƒđ‘„.đșpđ‘„q is not an axiom and therefore not derivable with the measure 1. Inductive cases. Assume that âˆƒđ‘„.đșpđ‘„q is derived by some last inference. We trace from the conclusion through major premises of elimination rules and composition rules (possibly 56 an empty set of rules). If the trace reaches a discharged formula of composition, then continue the trace from the minor premise of the composition. This is the major thread of the derivation. Note that the elimination rules conclude a formula with existential quantification, or a higher type universal formula, or a higher type variable in its positive part. Thus, we can consider how to derive such a formula. Case 1. When the trace ends the current formula cannot be a discharged assumption because there are no implication introduction rules below. Because the derivation has no assumptions the formula cannot either be an open assumption. Furthermore, none of the elimination rules can be âŠ„đž, because then the major premise ⊄ would be derivable and the system inconsistent. Case 2. By considering the axioms A2-A5 we see that elimination rules on axioms A2- A5 can only conclude formulas of the form 𝑃p𝜑q or l𝑃p𝜑q for some 𝜑 and these axioms are therefore excluded. To conclude ⊄ from axiom A1 would render the system inconsistent with both 𝑃p𝜑q and 𝑃p¬𝜑q derivable without assumptions. Case 3. Now assume that the trace ends with a modal axiom đ”, đ”Ëš , 4, 5 as the major premise of an E-rule. Note that 𝑇 and đŸ are derivable axioms and can therefore be excluded. The minor premise is a formula 𝐮, ♩l𝐮, l𝐮, ♩𝐮 respectively which has been derived without assumptions. Consider axiom đ” (𝐮 → l♩𝐮) as an example whence the derivation Π is of the form: .. .. đ” 𝜈 ∶ 𝐮 → l♩𝐮 đœˆâˆ¶đŽ →𝐾 𝜈 ∶ l♩𝐮 l𝐾 đ‘€ ∶ ♩𝐮 ♩𝐾 𝜔 ∶. 𝐮 .. . âˆƒđ‘„.đșpđ‘„q Note that the subderivation of 𝜈 ∶ 𝐮 has no open assumptions, but derives the formula 𝜈 ∶ 𝐮 for a label 𝜈. We consider two subcases that depend on the eigen-box condition. Subcase 3.1. If 𝜈 ≡ đ‘€, then the displayed ♩𝐾 is the only strong inference accessing the box with label 𝜔. Thus, we may use the weak inference â™ŠđŒ on đ‘€ ∶ 𝐮 with identical label: .. .. đ‘€ âˆ¶đŽ ♩ đŒ đ‘€ ∶ ♩𝐮 ♩𝐾 𝜔 ∶. 𝐮 .. . âˆƒđ‘„.đșpđ‘„q The identical label is allowed by the eigen-box condition because we assume reflexivity of the frame. Therefore, the reduction of the derivation decreases the measure. Subcase 3.2. If 𝜈 ı đ‘€, then there is a strong inference ♩𝐾 accessing the box labelled 𝜈 57 in the subderivation of 𝜈 ∶ 𝐮. Therefore, we may derive .. .. đœˆâˆ¶đŽ ♩ đŒ đ‘€ ∶ ♩𝐮 ♩𝐾 𝜔 ∶. 𝐮 .. . âˆƒđ‘„.đșpđ‘„q The reduction of the derivation decreases the measure. Case 3 (cont.). The derivation Π with modal axioms 4 or 5 can be similarly shortened. Now consider modal axiom đ”Ëš (♩l𝐮 → 𝐮). In this case the shortening procedure does not create a derivation with fewer formulas, in fact, replacing đ”Ëš with p4q produces a longer derivation but with fewer occurrences of axiom đ”Ëš and the increase of length is less than 5. We transform the derivation Π to the derivation on the right: .. .. 𝜈 ∶ ♩l𝐮 p4q ♩𝐾 .. 𝜔 ∶ l𝐮 → ll𝐮 𝜔 ∶ l𝐮 →𝐾 .. 𝜔 ∶ ll𝐮 đ”Ëš l𝐾 𝜈 ∶ ♩l𝐮 → 𝐮 𝜈 ∶ ♩l𝐮 𝜈 ∶ l𝐮 →𝐾 l𝐾 𝜈 ∶. 𝐮 𝜈 ∶. 𝐮 .. .. . . âˆƒđ‘„.đșpđ‘„q ↩ âˆƒđ‘„.đșpđ‘„q Thus accordingly, the inductive measure decreases. Note that the detour via axiom p4q is required due to the eigen-box condition that every box must be accessed by exactly one strong inference or have the same label. Case 4. Assume that the trace ends with an introduction rule and that there is at least one 𝐾-rule below it. Thus, we must have an elimination rule (different from ⊄-E) with the major premise derived by an introduction inference. Therefore we can eliminate the pair of rules, in the case of implication we replace the pair with a composition inference, reducing the measure of the derivation. In the case of the modal rules we can by the lemma (7) for substitution of box labels eliminate an đŒ ÂŽ 𝐾-pair. Case 4.2 Assume that the trace ends with an đŒ ÂŽ 𝐾-pair, but the pair is separated by an instance of composition. Then we can reduce the derivation to a shorter derivation with lower complexity of the composition formulas where the eigenvariable of the composition does not occur in the formulas. Here đ¶p𝜑q is for example the derivable formula 𝜑 → 𝜑 which does not occur as an assumption in the derivation of 𝐮 and we therefore can use the Composition rule as a substitution rule. r𝐮p𝜑qs2 .. .. .. .. .. .. .. .. r𝐮p𝜑qs2 .. r𝐮pđ›Œq → đ”pđ›Œqs1 𝐮pđ›Œq đ”p𝜑q 𝐮pđ›Œq đ¶p𝜑q .. →𝐾 â†’đŒ ,2 đ¶đ‘œđ‘šđ‘. đ”pđ›Œq 𝐮p𝜑q → đ”p𝜑q 𝐮p𝜑q đ”p𝜑q đ¶đ‘œđ‘šđ‘.,1 đ¶đ‘œđ‘šđ‘.,2 đ”p𝜑q ↩ đ”p𝜑q 58 The case of existential quantifier is similar. Note that we do not have the eigenvariable đ›Œ free in the conclusion đ¶. Thus đ¶p𝜙{đ›Œq ≡ đ¶ and we can reduce the rank of the composition formula. .. .. .. .. r∃𝜓 .𝐮p𝜓 , đ›œqs1 𝐮p𝜙, 𝜑q 𝐮p𝜙, 𝜑q đŒ âˆƒđŒ 𝐮pđ›Œ, đ›œq ∃𝜓 .𝐮p𝜓 , 𝜑q ∃𝜓 .𝐮p𝜓 , 𝜑q r𝐮pđ›Œ, 𝜑qs1 .. đ¶đ‘œđ‘šđ‘.,1 ∃𝐾 .. 𝐮pđ›Œ, 𝜑q 𝐮pđ›Œ, 𝜑q .. .. .. .. .. .. đ¶ 𝐮p𝜙, 𝜑q đ¶đ‘œđ‘šđ‘.,1 đ¶ ↩ đ¶ ↩ đ¶ Case 5. Lastly, assume that the conclusion âˆƒđ‘„.đșpđ‘„q is derived by an introduction rule with no 𝐾-rule below it. Note that the same kind of shortening argument, as above, applies to derivations with the conclusion 𝐾p𝑡q ∧ đșp𝑡q, đșp𝑡q, as well as 𝑃p𝜑q ↔ l𝜑p𝑡q, and 𝑃p𝜑q → l𝜑p𝑡q. Thus, we may assume that these formulas have been derived by introduction rules through the definition of đșp𝑡q. The derivation Π has the following form, with 𝜑 an eigenvariable: 𝑃p𝜑q .. .. l𝜑p𝑡q â†’đŒ 𝑃p𝜑q → l𝜑p𝑡q .. .. âˆƒđ‘„.đșpđ‘„q Thus, we can shorten the derivation by replacing 𝜑 with đș. Note that in the derivation below we have used the subderivation of 𝐾p𝑡q from Π. r𝑃p𝜑qs1 .. .. l𝜑p𝑡q 𝑃pđșq .. 𝑇 đ¶đ‘œđ‘šđ‘.,1 .. lđșp𝑡q → đșp𝑡q lđșp𝑡q →𝐾 𝐾p𝑡q đșp𝑡q âˆ§đŒ 𝐾p𝑡q ∧ đșp𝑡q âˆƒđŒ âˆƒđ‘„.đșpđ‘„q Note that the defined inductive measure decreases through the modification of the derivation. Thus, in all inductive cases we can decrease the inductive measure of the derivation. Thus, there cannot exist a derivation of âˆƒđ‘„.đșpđ‘„q. We can conclude that the same unprovability result holds in a system without the rule of composition because the systems are equally strong. Corollary 9. The formula âˆƒđ‘„.đșpđ‘„q is not derivable assuming đ» 𝑂𝑀𝐿𝑖 ` Ax is consistent. Corollary 10. The formula đș𝐾𝑠𝑠𝐮 đ‘„ is not derivable assuming đ» 𝑂𝑀𝐿𝑖 ` Ax is consistent. 59 Proof. Assume that đș𝐾𝑠𝑠𝐮 đ‘„ is derivable, then we have the following derivation of âˆƒđ‘„.đșpđ‘„q, contradicting theorem (8): 𝐿𝑒𝑚.1 .. .. 𝑁 𝐾pđ‘„q .. đ·đ‘’đ‘“ .. ∀𝜑.r𝜑𝐾𝑠𝑠𝐮 đ‘„ → lâˆƒđ‘„.𝜑pđ‘„qs ∀𝐾 đș𝐾𝑠𝑠𝐮 đ‘„ đș𝐾𝑠𝑠𝐮 đ‘„ → lâˆƒđ‘„.đșpđ‘„q →𝐾 lâˆƒđ‘„.đșpđ‘„q 𝑇 âˆƒđ‘„.đșpđ‘„q For the same reason we have a negative solution to the derivability of lâˆƒđ‘„.đșpđ‘„q. The main theorem of Gödel’s ontological proof, that the existence of a godlike individual is necessary, is simply not intuitionistically derivable. Corollary 11. The formula lâˆƒđ‘„.đșpđ‘„q is not derivable assuming đ» 𝑂𝑀𝐿𝑖 ` Ax is consistent. 7. Consistency of constructive Higher-order modal logic Note that in the proof of theorem (8) we only assume consistency of đ» 𝑂𝑀𝐿𝑖 when dealing with axiom A1 and âŠ„đž , therefore let Axâ€Č be the set of axioms A2-A5, and đ» 𝑂𝑀𝐿″ 𝑚 the system of minimal logic where âŠ„đž has been excluded from the propositional rules. We can conclude the following consistency corollary. â€Č Corollary 12. The formula âˆƒđ‘„.đșpđ‘„q is not derivable in đ» 𝑂𝑀𝐿″ 𝑚 ` Ax . â€Č Note that if we have a derivation of 𝑃p𝜑q → l𝜑pđ‘„q in đ» 𝑂𝑀𝐿″ 𝑚 ` Ax , and assume the additional axiom 𝐾p0q that the domain of objects is provably non-empty, then we could derive âˆƒđ‘„.đșpđ‘„q as in case 5 in the proof of theorem (8). Thus, derivability of 𝑃p𝜑q → l𝜑pđ‘„q â€Č in đ» 𝑂𝑀𝐿″ 𝑚 ` Ax ` 𝐾p0q contradicts theorem (8). â€Č Hence we conclude that 𝑃p𝜑q → l𝜑pđ‘„q is not derivable in đ» 𝑂𝑀𝐿″ 𝑚 `Ax `𝐾p0q. However, ″ â€Č if ∀𝜑.l𝜑pđ‘„q were to be derivable in đ» 𝑂𝑀𝐿𝑚 ` Ax ` 𝐾p0q, then 𝑃p𝜑q → l𝜑pđ‘„q could be easily derived by vacuous implication introduction. Thus, ∀𝜑.l𝜑pđ‘„q cannot be derivable â€Č in đ» 𝑂𝑀𝐿″ 𝑚 ` Ax ` 𝐾p0q nor in minimal higher-order modal logic without disjunction đ» 𝑂𝑀𝐿″ 𝑚. Theorem 13 (Consistency of Minimal Higher-Order Modal Logic). The formula ∀𝜑.l𝜑pđ‘„q is not derivable in đ» 𝑂𝑀𝐿″ 𝑚. â€Č If ∀𝜑.𝜑pđ‘„q were derivable in đ» 𝑂𝑀𝐿″𝑚 ` Ax ` 𝐾p0q, then we could derive by modal rule lđŒ , and from this derive ∀𝜑.l𝜑pđ‘„q contradicting theorem (13). Thus, we conclude that the system of minimal higher-order logic without disjunction đ» 𝑂𝐿″ 𝑚 is consistent. Corollary 14 (Consistency of Minimal Higher-Order Logic). The formula ∀𝜑.𝜑pđ‘„q is not derivable in đ» 𝑂𝐿″ 𝑚. 60 Note that the formula ∀𝜑.𝜑pđ‘„q can be taken as a definition of ⊄. This allows us to conclude that the premise of the rule âŠ„đž is not a derivable theorem. Thus, implying that we may reintroduce the rule of âŠ„đž and đ» 𝑂𝐿″ 𝑖 as well as đ» 𝑂𝑀𝐿𝑖 are consistent. 8. Conclusions At the core of the ontological argument is not only the conditional statement that âˆƒđ‘„.đșpđ‘„q implies lâˆƒđ‘„.đșpđ‘„q which in the proof presented above is derivable using intuitionistic logic. Another central element is the derivability of the compatibility of the positive properties, in other words, that â™Šâˆƒđ‘„.đșpđ‘„q is derivable. This latter statement is not intuitionistically derivable. The problem arising with â™Šâˆƒđ‘„.đșpđ‘„q is that the standard derivation uses reductio ad absurdum, a form of indirect proof, which is inherently classical. The notes from 1970 which were written by Dana Scott based on conversations with Gödel give an indisputably classical proof of this statement. There the statement lâˆ€đ‘„.ÂŹđșpđ‘„q is assumed, and is easily shown to imply a contradictory statement, such as 𝑃p⊄q using axiom A2. From the contradiction we can derive the negation ÂŹlâˆ€đ‘„.ÂŹđșpđ‘„q which is classically equivalent to â™Šâˆƒđ‘„.đșpđ‘„q. Needless to say, this does not suffice in a constructive theory. However, already Leibniz, who argued informally through a requirement of self- consistency of perfections, could have been an inspiration for the classical principles of Gödel’s formal ontological proof. This hypothesis is based on a contested reading of Leibniz (see for example [21, Section 3] and the computer assisted analysis of [3]). Leibniz assumed that perfections are unanalysable and therefore it is impossible to demonstrate that these are incompatible. Thus, it is (classically) possible that there is an individual that satisfies all perfections [10, pp. 137–138]. Note however that Leibniz may be formally interpreted in a more versatile manner [21, Section 5]. We conclude that the intuitionistic unprovability of â™Šâˆƒđ‘„.đșpđ‘„q is an obstacle for the formal system đ» 𝑂𝑀𝐿𝑖 ` Ax where only conditional statements that all depend on âˆƒđ‘„.đșpđ‘„q are provable. As soon as âˆƒđ‘„.đșpđ‘„q is assumed a multitude of relevant statements become constructively provable. Acknowledgments This article is part of the Gödeliana research project led by Jan von Plato, which is funded by the European Research Council (ERC), under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 787758) and from the Academy of Finland (Decision No. 318066). Partial funding has also been received through Sara Negri’s project Modalities and Conditionals: Systematic and Historical Studies from the Academy of Finland (Project No.1308664). The author is indebted to the referees for the valuable comments on an early draft. Any potential errors in this article should be communicated to the author as this is a work in progress at the time of writing. 61 References [1] Anderson, C. A. (1990). Some Emendations of Gödel’s Ontological Proof. Faith and Philosophy, Vol. 7, Issue 3, pp. 291-303. [2] Anderson, C. A.& Gettings, M. (1996). Gödel’s ontological proof revisited. In: edited by HĂĄjek P. Gödel ’96, Springer. [3] Bentert M., BenzmĂŒller C., Streit D., & Woltzenlogel Paleo, B. (2016). Analysis of an Ontological Proof Proposed by Leibniz. In Charles Tandy (ed.), Death and Anti-Death, Volume 14: Four Decades After Michael Polanyi, Three Centuries After G.W. Leibniz. Ria University Press. [4] BenzmĂŒller, C. & Woltzenlogel Paleo, B. (2014). Automating Gödel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers. Frontiers in Artificial Intelligence and Applications. Vol 263. IOS Press. [5] BenzmĂŒller, C., & Woltzenlogel Paleo, B. (2016). The Inconsistency in Gödel’s Ontological Argument: A Success Story for AI in Metaphysics, in S. Kambhampati (ed.), Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence–IJCAI, AAAI Press, Menlo Park, CA. [6] BenzmĂŒller, C. & Weber, L. & Woltzenlogel Paleo, B. (2016). Computer-Assisted Analysis of the Anderson-HĂĄjek Ontological Controversy. In: Logica Universalis 10. [7] BenzmĂŒller, C. (2022). A Simplified Variant of Gödel’s Ontological Argument. To appear in Sophia. [8] BjĂžrdal, F. (1999). Understanding Gödel’s Ontological Argument, in Timothy Childers (ed.) The Logica Yearbook 1998, pp. 214-217, Filosofia. [9] N. B. Cocchiarella. (1969). A Completeness Theorem in Second Order Modal Logic. In: Theoria 35, pp. 81–103. [10] Fitting, M. (2002). Types, Tableaus, and Gödel’s God, Kluwer Academic Publishers. [11] Garson, J. (2018). Modal Logic. Entry in Stanford Encyclopedia of Philosophy. [12] Gödel, K. (1970). Ontological Proof, in [13] [13] Gödel, K. (1995). Kurt Gödel Collected Works: Unpublished essays and lectures, Vol. 3, Oxford University Press. [14] HĂĄjek, P. (1996). Magari and others on Gödel’s Ontological Proof, in Ursini et alii (eds.) Logic and Logical Algebra, pp. 125–136, Marcel Dekker. [15] HĂĄjek, P. (2002). A new small emendation of Gödel’s ontological proof, Studia Logica vol 71, no. 2, pp. 149–164. [16] Hartshorne, Charles. (1962). The Logic of Perfection. LaSalle, Il.: Open Court Publishing Company. [17] Kanckos, A., & Lethen, T. (2021). The Development of Gödel’s Ontological Proof. The Review of Symbolic Logic, 14(4), 1011–1029. [18] Kanckos, A. & Lethen, T. (2022), Kurt Gödel’s reception of Charles Hartshorne’s ontological proof. in E Ramharter (ed.), The Vienna Circle and Religion. Vienna Circle Institute Yearbook, Springer International Publishing, Cham, pp. 183–196. [19] Kanckos, A. & Wolzenlogel Paleo, B. (2016). Variants of Gödel’s ontological proof in a Natural Deduction Calculus, Studia Logica 105(3). 62 [20] Kovac̆, S. (2012). Modal collapse in Gödel’s ontological proof. In: Ontological Proofs Today, Chapter: 15. Publisher: Frankfurt etc.: Ontos, Editors: M. Szatkowski, pp. 323–343. [21] Lenzen, W. (2017). Leibniz’s Ontological Proof of the Existence of God and the Problem of Impossible Objects. Log. Univers. 11, 85–104. [22] Muskens, R. (2006). Higher Order Modal Logic. In P. Blackburn, J.F.A.K. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, Studies in Logic and Practical Reasoning, pp. 621-653. Elsevier, Dordrecht. [23] Scott, D. (1970). Notes in Dana Scotts hand. In: Sobel, J. H. 2001. Logic and Theism: Arguments for and against Beliefs in God, Cambridge University Press. [24] Sobel, J. H. (1987). Gödel’s Ontological Proof. In: edited by J. J. Thompson. On being and saying : essays for Richard Cartwright, MIT Press. [25] Sobel, J. H. (2001). Logic and Theism: Arguments for and against Beliefs in God, Cambridge University Press. [26] Sobel, J. H. (2006). On Gödel’s ontological proof, In: edited by H. Lagerund et al., (eds.), Modality matters: Twenty-five essays in honour of Krister Segerberg, Uppsala Philosophical Studies. [27] Wang, H. (1996). A Logical Journey: From Gödel to Philosophy, MIT Press. 63