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 axiomatizations 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 modifications by Leibniz, and distinctly more complex than the modern ontological proof of 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 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]).

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. Characteristic for the intuitionistic system is that we do not have the classically valid interdefinability of connectives, quantifiers, and modal operators. However, the disjunction rules have been suppressed due to formal reasons in theorem (8) where permutation conversions would otherwise be needed.

𝐴 𝐵 𝐴 ∧ 𝐵∧𝐼 𝐴 ∧ 𝐵 𝐴 ∧𝐸 1 𝐴 ∧ 𝐵 𝐵 ∧𝐸 2 ⊥ 𝐴 ⊥𝐸 r𝐴s 𝑛 . . . .

𝐵 𝐴 → 𝐵

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 ∃𝐸. 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.

𝜔 ∶ . . . . 𝐴 𝑣 ∶ 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. 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♦𝐴

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 𝐻 𝑂𝑀𝐿 `𝐴𝑥.

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. Note that in a constant domain setting the derivations of lemmas (1 & 2) could be even simpler.

r𝜑𝐸𝑠𝑠

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 𝐸.

Proof.

𝜔 1 ∶ 𝑃p𝐺q 𝜔 2 ∶ 𝑃p𝐺q 𝜔 2 ∶ r𝐺p𝑥qs 1 𝜔 2 ∶ ∀𝜑.r𝑃p𝜑q ↔ l𝜑p𝑥qs 𝐷𝑒𝑓 𝜔 2 ∶ 𝑃p𝐺q ↔ l𝐺p𝑥q ∀𝐸 𝜔 2 ∶ 𝑃p𝐺q → l𝐺p𝑥q ∧𝐸 𝜔 2 ∶ l𝐺p𝑥q →𝐸 𝜔 3 ∶ 𝐺p𝑥q . . . . 𝜔 3 ∶ 𝑃p𝜑q → l𝜑p𝑥q r𝑃p𝜑qs 2 l♦𝑃p𝜑q 𝐵 ll♦𝑃p𝜑q p4q 𝜔 1 ∶ l♦𝑃p𝜑q l𝐸 𝜔 2 ∶ ♦𝑃p𝜑q l𝐸 𝜔 3 ∶ 𝑃p𝜑q ♦𝐸 𝜔 3 ∶ l𝜑p𝑥q 𝜔 2 ∶ ♦l𝜑p𝑥q ♦𝐼 𝜔 2 ∶ 𝜑p𝑥q 𝐵 ω2 ∶ 𝐺p𝑥q → 𝜑p𝑥q →𝐼 ,1 𝜔 2 ∶ 𝐸p𝑥q → r𝐺p𝑥q → 𝜑p𝑥qs →𝐼 𝜔 2 ∶ ∀𝑥.r𝐺p𝑥q → 𝜑p𝑥qs ∀ 𝐼 𝜔 1 ∶ l∀𝑥.r𝐺p𝑥q → 𝜑p𝑥qs l𝐼 𝜔 1 ∶ 𝑃p𝜑q axiom 𝐴2 l𝑃p𝜑q l𝐼 𝑃p𝜑q → l𝑃p𝜑q →𝐼 ,2

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∃𝑥.

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. 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.

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 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 𝜈 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𝐴 → 𝐴 𝐵 ˚. . . . 𝜈 ∶ ♦l𝐴 𝜈 ∶ 𝐴

∃𝑥.𝐺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. 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 Π.

∃𝐼

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.

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.

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 selfconsistency 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.