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 ↔ is here investigated as a case study of intuitionistic derivability using natural deduction. The formal 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).
♦ for all formulas . This variant of the axiomatization
CEUR
CEUR
Workshop Proceedings (CEUR-WS.org)
Hartshorne (see [
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.
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 [
The emendation of Anderson [
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 [
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
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 [
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
where
refer to the tableaux-style proofs in [
In the formal system defined below, 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. , for intuitionistic higher-order modal logic ∧ ⊥ ⊥ ∧ r s 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 q ∀
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 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 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.
trivial. Concerning the two versions of Brouwer’s axiom, and ˚, note the discussion
on an axiom for symmetry in [
T K B B
˚ 4 5 lp → q → pl →
l q l → → ♦l → l → ♦ → l♦ ll l♦
The axioms for Anderson’s emendation [
which states that the property variable is an essence of individual , and necessary existence are given a definition below. ≡ ∀ . rl p q ↔ l∀ . p p q → p qqs p q ≡ ∀. r p q
It can be shown that axiom A5 is derivable within the system if we assume A2 and A3.
This is a known result of [
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. 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.
l ppqq l ∶ p q l ∶ p q → p q →
→ ∶ p q → p p q → p qq ∀ ∶ ∀. p p q → p qq
l 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 [
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 . 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 ppqq l ∶ ∀. r p q ↔ l p qs → ∶ p q ↔ l p q ∶ l p q → p q ∧
. ∶ p q ∶ l p q p4q l → Then, let Π1 be the following subderivation of one direction of the essence equivalence: ∶ r p qs1 ∶ p q → p q →,1 ∶ p q → r p q → p qs → ∶ ∀. p p q → p qq l l∀. p p q → p qq
∀ l p q → l∀. p p q → p qq →,2 ∃. p q → rl p q → l∀. p p q → p qqs →,3 The other direction Π2 is similarly obtained: r∃. p qs2 ∃. p q → rl∀. p p q → p qq → l p qs →,2
rl∀. p p q → p qqs1 axiom 2 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 l∀. p p q → p qq → l p q ∧ r∃. p qs1 . . .
. p q ∧ Theorem 5. The conditional statement ∃. p q → l∃. p q is derivable in . . . . .
∀ . p q ∧ ∃. ∃
∃. p q → →,1
r∃. p qs1 ∃. p q → theor.em.4
→
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 rank of the composition is the rank of the discharged assumption p p qq.
` 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 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 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.
derivable.
′ ` Ax is consistent, then the formula ∃. p q is not conjectured inductive measure pΠq. derivable with the measure 1.
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
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 A2A5 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♦ ∶ ♦ ∶ . . .
. ∃. p q . . .
.
∶ l ♦ → 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: 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 ∶ ♦l →
˚ 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 ∶∶ ♦ll ♦ → 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 q → p qs1 p q p q → p q r p. qs2 . .
. p q
.,2 ll ∶ ll ∶ l ∶. . .
. ∃. p q
l l
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
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: Thus, we can shorten the derivation by replacing with . Note that in the derivation below we have used the subderivation of p q from Π.
p q → l p q
→ p q l 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 Proof. Assume that
is derivable, then we have the following derivation of ∃. p q, contradicting theorem (8): 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.
Note that in the proof of theorem (8) we only assume consistency of with axiom A1 and ⊥ , therefore let Ax′ be the set of axioms A2-A5, and when dealing ″ 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
Note that if we have a derivation of p q → l p q in ″ ` Ax′.
″ ` Ax′, and assume the derive ∃. in in additional axiom p0q that the domain of objects is provably non-empty, then we could p q as in case 5 in the proof of theorem (8). Thus, derivability of p q → l p q ″ ` Ax′ ` p0q contradicts theorem (8).
Hence we conclude that p q → l p q is not derivable in if ∀. l p q were to be derivable in easily derived by vacuous implication introduction. Thus, ∀. l p q cannot be derivable ″ ` Ax′ ` p0q nor in minimal higher-order modal logic without disjunction ″ ` Ax′ ` p0q, then p q → l p q could be ″ `Ax′ ` p0q. However, Theorem 13 (Consistency of Minimal Higher-Order Modal Logic). The formula ∀. l p q is not derivable in ″ 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 ″
″ ` Ax′ ` p0q, then we could derive by modal rule
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.
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 [
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.
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. [20] Kova˘c, 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.