=Paper=
{{Paper
|id=Vol-3326/ARQNL2022_paper3
|storemode=property
|title=Intuitionistic Derivability in Anderson's Variant of the Ontological Argument
|pdfUrl=https://ceur-ws.org/Vol-3326/ARQNL2022_paper3.pdf
|volume=Vol-3326
|authors=Annika Kanckos
|dblpUrl=https://dblp.org/rec/conf/cade/Kanckos22
}}
==Intuitionistic Derivability in Anderson's Variant of the Ontological Argument==
https://ceur-ws.org/Vol-3326/ARQNL2022_paper3.pdf
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