=Paper=
{{Paper
|id=Vol-3009/paper4
|storemode=property
|title=Applying Second-Order Quantifier Elimination in
Inspecting Gödel's Ontological Proof
|pdfUrl=https://ceur-ws.org/Vol-3009/paper4.pdf
|volume=Vol-3009
|authors=Christoph Wernhard
|dblpUrl=https://dblp.org/rec/conf/kr/Wernhard21
}}
==Applying Second-Order Quantifier Elimination in
Inspecting Gödel's Ontological Proof==
https://ceur-ws.org/Vol-3009/paper4.pdf
Applying Second-Order Quantifier Elimination
in Inspecting Gödel’s Ontological Proof
Christoph Wernhard
University of Potsdam, Germany
Abstract. In recent years, Gödel’s ontological proof and variations of it
were formalized and analyzed with automated tools in various ways. We
supplement these analyses with a modeling in an automated environment
based on first-order logic extended by predicate quantification. Formula
macros are used to structure complex formulas and tasks. The analysis is
presented as a generated type-set document where informal explanations
are interspersed with pretty-printed formulas and outputs of reasoners
for first-order theorem proving and second-order quantifier elimination.
Previously unnoticed or obscured aspects and details of Gödel’s proof be-
come apparent. Practical application possibilities of second-order quan-
tifier elimination are shown and the encountered elimination tasks may
serve as benchmarks.
1 Introduction
Kurt Gödel’s ontological proof is bequeathed in hand-written notes by himself
[14] and by Dana Scott [25]. Since transcriptions of these notes were published
in 1987 [26], the proof was analyzed, formalized and varied in many different
logical settings.1 Books by John Howard Sobel [27] and Melvin Fitting [13] in-
clude comprehensive discussions. Branden Fitelson, Paul E. Oppenheimer and
Edward N. Zalta [12,24] investigated various metaphysical arguments in an auto-
mated first-order setting based on Prover9 [20]. Christoph Benzmüller and Bruno
Woltzenlogel Paleo [7] initiated in 2014 the investigation of Gödel’s argument
with automated systems, which led to a large number of follow-up studies con-
cerning its verification with automated tools and the human-readable yet formal
representation, e.g., [8,16,6,17,5]. Here we add to these lines of work an inspec-
tion of Gödel’s proof in a logical setting that so far has not been considered for
this purpose. The expectation is that further, previously unnoticed or obscured
aspects and details of the proof become apparent. The used framework, PIE
(“Proving, Interpolating, Eliminating”) [29,30] embeds automated reasoners, in
particular for first-order theorem proving and second-order quantifier elimina-
tion, in a system for defining formula macros and rendering LATEX-formatted
1
Recently discovered further sources by Gödel are presented in [15].
Copyright © 2021 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
Applying SOQE in Inspecting Gödel’s Ontological Proof 99
presentations of formula macro definitions and reasoner outputs. In fact, the
present paper is the generated output of such a PIE document.2
The target logic of the macros is second-order logic, or, more precisely clas-
sical first-order logic extended by predicate quantifiers. The macro layer and the
formulas obtained as expansions can be strictly separated. In our modeling of
Gödel’s proof we proceed by expressing large-scale steps (axioms, theorems) with
macros whose relationships are verified by invocations of embedded reasoners.
In this sense our formalization of may be considered as semi-automated.
Aside of providing further material for the study of Gödel’s proof, the work
shows possibilities of applying second-order quantifier elimination in a practical
system. It appears that the functionality of the macro mechanism is necessary to
express nontrivial applications on the basis of first- and second-order logic. The
elimination problems that suggested themselves in the course of the investigation,
some of which could not be solved by the current version of PIE, may be useful
as benchmarks for implemented elimination systems.3
The rest of the paper is structured as follows: After introducing preliminaries
in Sect. 2, Gödel’s proof in the version of Scott is developed in Sect. 3. An ap-
proach to obtain the weakest sufficient precondition on the accessibility relation
for Gödel’s proof with second-order quantifier elimination is then discussed in
Sect. 4. Section 5 concludes the paper. Supplementary material is provided in
the report version [31] of the paper.
2 Preliminaries
A PIE document is a Prolog source file that contains declarative formula macro
definitions and specifications of reasoner invocations, interspersed with LATEX
comments in the manner of literate programming [18]. The PIE processor ex-
pands the formula macros, invokes the reasoners, and compiles a LATEX docu-
ment where the formula macro definitions and the results of reasoner invocations
are pretty-printed. Alternatively, the processor’s functionality is accessible from
Prolog, via the interpreter and in programs. The overall processing time for the
present paper, including reasoner invocations and LATEX processing to produce
a PDF, is about 2.5 seconds.
Formula macros without parameters can play the role of formula names.
Expressions with macros expand into formulas of first-order logic extended with
predicate quantifiers. Hence, some means of expression that would naturally be
used in a higher-order logic formalization of Gödel’s proof are not available in the
expansion results. Specifically, predicates in argument position are not permitted
and there is no abstraction mechanism to construct predicates from formulas.
2
The PIE source of this paper is available at http://cs.christophwernhard.com/pie.
3
Another recent system for second-order quantifier elimination on the basis of first-
order logic is DLS-Forgetter [2], which, like the implementation in PIE, is based
on the DLS algorithm [10]. An older resolution-based system, SCAN, [22,23] can
currently be invoked via a Web interface.
100 Christoph Wernhard
However, these higher-order features are in Gödel’s proof actually only required
with respect to specific instances that can be expressed in first-order logic.
As embedded reasoners we used the first-order theorem provers Prover9 [20]
and CMProver [9,29], the first-order model generator Mace4 [20], and an imple-
mentation [29,30] of the DLS algorithm [10] for second-order quantifier elimi-
nation, which is based on Ackermann’s Lemma [1]. Reasoner outputs computed
during processing of the PIE document are presented with the introductory
phrases This formula is valid:, This formula is not valid: and Result of
elimination:. In addition, various methods for formula simplification, clausifi-
cation and un-Skolemization are applied in preprocessing, inprocessing and for
output presentation.
The generated LATEX presentation of formulas and macro definitions bears
some footprint inherited from the Prolog syntax that is used to write formulas
in PIE documents. As in Prolog, predicate and constant symbols are written in
lower case. Macro parameters and bound logical variables that are to be instan-
tiated with fresh symbols at macro expansion are printed like Prolog variables
with a capitalized initial. Where-clauses in macro definitions are used to display
in abstracted form auxiliary Prolog code executed at macro expansion.
We write formulas of modal predicate logic as formulas of classical first-
order logic with one additional free world variable v by applying the standard
translation from [4, Sec. 11.4] (see also [3, Chap. XII]), which can be defined as
ST (P (t1 , . . . , tn )) def
= P (v, t1 , . . . , tn )
ST (¬F ) def
= ¬ST (F )
ST (F ∨ G) def
= ST (F ) ∨ ST (G)
ST (∃xF ) def
= ∃x (e(v, x) ∧ ST V (F ))
ST (♦F ) def
= ∃w (r(v, w) ∧ i s.th. x free in F e(w, xi ) ∧ ST (F ){v 7→ w})
i
An n-ary predicate P in the modal logic is translated into an n+1-ary predicate,
where the first argument represents a world. The binary predicates r and e are
used for world accessibility and membership in the domain of a world. The logic
operators ∧, →, ↔, ∀, can be understood as shorthands defined in terms of the
shown operators. As target logic we neither use a two-sorted logic nor encode
two-sortedness explicitly with relativizer predicates. However, the translation
of modal formulas yields formulas in which all quantifications are relativized
by r or by e, which seems to subsume the effect of such relativizer predicates.
To express that free individual symbols are of sort world we use the unary
predicate world. Macro 4, defined below, can be used as an axiom that relates
world and r as far as needed for our purposes. The standard translation realizes
with respect to the represented modal logic varying domain semantics (actualist
notion of quantification), expressed with the existence predicate e. Constant
domain semantics (possibilist notion of quantification) can be achieved with
axioms that state domain increase and decrease.
As technical basis for Gödel’s proof we use the presentation of Scott’s version
[25] in [7, Fig. 1], shown here as Fig. 1. The identifiers A1–A5, T1–T3, D1–D3
and C of the involved axioms, theorems, definitions and corollary follow [7]. In
addition, Lemma L is taken from [6, Fig. 1], where it is appears as L2.
Applying SOQE in Inspecting Gödel’s Ontological Proof 101
A1 Either a property or its negation is positive, but not both
∀P (Pos(¬P ) ↔ ¬Pos(P ))
A2 A property necessarily implied by a positive property is positive
∀P ∀Q ((Pos(P ) ∧ ∀x (P (x) → Q(x))) → Pos(Q))
T1 Positive properties are possibly exemplified
∀P (Pos(P ) → ♦∃x P (x))
D1 A God-like being possesses all positive properties
G(x) ↔ ∀P (Pos(P ) → P (x))
A3 The property of being God-like is positive
Pos(G)
C Possibly, God exists
♦∃x G(x)
A4 Positive properties are necessarily positive
∀P (Pos(P ) → Pos(P ))
D2 An essence of an individual is a property possessed by it and necessarily im-
plying any of its properties
Ess(P, x) ↔ P (x) ∧ ∀Q (Q(x) → ∀y (P (y) → Q(y)))
T2 Being God-like is an essence of any God-like being
∀x (G(x) → Ess(G, x))
D3 Necessary existence of an individual is the necessary exemplification of all its
essences
NE(x) ↔ ∀P (Ess(P, x) → ∃y P (y))
A5 Necessary existence is a positive property
Pos(NE)
L If a God-like being exists, then necessarily a God-like being exists
∃x G(x) → ∃x G(x)
T3 Necessarily, God exists
∃x G(x)
Fig. 1. Scott’s version of Gödel’s ontological argument [25], adapted from [7,6].
3 Rendering Gödel’s Ontological Proof
3.1 Positiveness – Proving Theorem T1
The first two axioms in Gödel’s proof, A1 and A2, are about positiveness of
properties. Theorem T1 follows from them. The following macros render the
left-to-right direction of A1 and A2, respectively.
Macro 1 ax1→ (V, P ) is defined as
world(V ) → (pos(V, N 0 ) → ¬pos(V, P 0 )),
where N 0 := ¬P ˙ ,
0 :=
P Ṗ .
Is positive is represented here by the binary predicate pos, which has a world and
an individual representing a predicate as argument. P 0 and N 0 are individual con-
stants that represent a supplied predicate P and its complement λvx.¬P (v, x),
respectively. The where clause specifies that at macro expansion they are replaced
by individual constants Ṗ and ¬P ˙ , available for each predicate symbol P .
102 Christoph Wernhard
Throughout this analysis, we expose the current world as macro parameter V ,
which facilitates identifying proofs steps where an axiom is not just applied with
respect to the initially given current world but to some other reachable world.
Macro 2 ax2 (V, P, Q) is defined as
world(V ) →
(pos(V, P 0 ) ∧
∀W (r(V, W ) →
∀X (e(W, X) → (P (W, X) → Q(W, X)))) →
pos(V, Q0 )),
where P 0 := Ṗ ,
Q0 := Q̇.
As an insight-providing intermediate step for proving T1 we can now derive
the following lemma using just a single instance of each of ax1→ and ax2 , where
verum (λx.x = x) and falsum (λx.x 6= x) are represented as binary predicates
> and ⊥, whose first argument is a world.
Macro 3 lemma1 (V ) is defined as
˙
world(V ) → ¬pos(V, ⊥).
Macro 4 r _world1 is defined as ∀v∀w (r(v, w) → world(w)).
Macro 5 topbot _def is defined as
∀v∀x (world(v) → (>(v, x) ↔ e(v, x))) ∧
∀v∀x (world(v) → (⊥(v, x) ↔ ¬e(v, x))).
To express the precondition for lemma1 we need some auxiliary macros concern-
ing > and ⊥. The following expresses equivalence of > and λvx.¬⊥(v, x).
Macro 6 topbot _equiv is defined as ∀v∀x (world(v) → (>(v, x) ↔ ¬⊥(v, x))).
This formula is valid: topbot _def → topbot _equiv.
˙ ⊥
The constants >, ˙ and ¬>˙ designate the individuals associated with >, ⊥
and λvx.¬>(v, x), respectively. The following axiom leads from the equivalence
expressed by Macro 6 to equality of the associated individuals.
Macro 7 topbot _equiv _equal is defined as topbot _equiv → ⊥˙ = ¬>.
˙
Equality is understood there with respect to first-order logic, not qualified by a
world parameter. In [31] alternatives are shown, where equality is replaced by a
weaker substitutivity property. We can now give the precondition for lemma1 .
Macro 8 pre _lemma1 (V ) is defined as
r _world1 ∧
topbot _def ∧
topbot _equiv _equal ∧
ax1→ (V, >) ∧
ax2 (V, ⊥, >).
This formula is valid: pre _lemma1 (v) → lemma1 (v).
T1 can be rendered by the following macro with a predicate parameter.
Applying SOQE in Inspecting Gödel’s Ontological Proof 103
Macro 9 thm1 (V, P ) is defined as
world(V ) →
(pos(V, P 0 ) →
∃W (r(V, W ) ∧ ∃X (e(W, X) ∧ P (W, X)))),
where P 0 := Ṗ .
Macro 10 pre _thm1 (V, P ) is defined as lemma1 (V ) ∧ ax2 (V, P, ⊥).
This formula is valid: pre _thm1 (v, p) → thm1 (v, p).
Instances of thm1 (V, P ) can be proven for arbitrary worlds V and predicates P ,
from the respective instance of the precondition pre _thm1 (V, P ). A further in-
stance of ax2 – beyond that used to prove lemma1 – is required there, with
respect to ⊥ and the given predicate P .
3.2 Possibly, God Exists – Proving Corollary C
Axiom A3 and T1 instantiated by God-like together imply corollary C. This is
rendered as follows, where God-like is represented by g.
Macro 11 ax3 (V ) is defined as
world(V ) → pos(V, ġ).
Macro 12 coro(V ) is defined as
world(V ) → ∃W (r(V, W ) ∧ ∃X (e(W, X) ∧ g(W, X))).
Macro 13 pre _coro(V ) is defined as thm1 (V, g) ∧ ax3 (V ).
This formula is valid: pre _coro(v) → coro(v).
Notice that, differently from the proofs reported in [7, Fig. 2], C, represented
here by coro, can be proven independently from the definition of God-like, D1,
which is represented here by the Macros def1→ and def1→¬ defined below.
3.3 Essence – Proving Theorem T2
With macros def1→ and def1→¬ , defined now, we represent the left-to-right direc-
tion of D1. Actually, only this direction of D1 is required for the proving the
further theorems.
Macro 14 def1→ (V, X, P ) is defined as
g(V, X) → (pos(V, P 0 ) → P (V, X)),
where P 0 := Ṗ .
Macro 15 def1→¬ (V, X, P ) is defined as
g(V, X) → (pos(V, P 0 ) → ¬P (V, X)),
where P 0 := ¬P ˙ .
The following macro val _ess renders the definiens of the essence of relation-
ship between a predicate and an individual in D2. It is originally a formula with
predicate quantification, but without application of a predicate to a predicate.
The macro val _ess exposes the universally quantified predicate as parameter Q,
permitting to use it instantiated with some specific predicate.
104 Christoph Wernhard
Macro 16 val _ess(V, P, X, Q) is defined as
P (V, X) ∧
(Q(V, X) →
∀W (r(V, W ) →
∀Y (e(W, Y ) → (P (W, Y ) → Q(W, Y ))))).
The universally quantified version of val _ess can be be expressed by prefixing
a predicate quantifier upon Q. Eliminating this second-order quantifier shows
another view on essence.
Input: ∀q val _ess(v, p, x, q).
Result of elimination:
p(v, x) ∧
∀y∀z (e(y, z) ∧ p(y, z) ∧ r(v, y) → y = v) ∧
∀y∀z (e(y, z) ∧ p(y, z) ∧ r(v, y) → z = x).
We convert the elimination result “manually” to a more clear form and prove
equivalence by referencing to the “last result” via a macro.
Macro 17 last _result is defined as F,
where last_ppl_result(F).
This formula is valid: p(v, x) ∧ ∀w (r(v, w) → ∀y (e(w, y) → (p(w, y) → w =
v ∧ y = x))) ↔ last _result.
The following definition now renders D2 as definition of the predicate ess in
terms of val _ess.
Macro 18 def2 (V, P ) is defined as
world(V ) →
∀X (ess(V, P 0 , X) ↔ ∀Q val _ess(V, P, X, Q)),
where P 0 := Ṗ .
In [31] it is shown that two observations about essence mentioned as NOTE in
Scott’s version [25] of Gödel’s proof can be derived in this modeling.
The following two macros render the right-to-left direction of axioms A1
and A4. The original axioms involve a universally quantified predicate that ap-
pears only in argument role. In the macros, it is represented by the parameter P .
Macro 19 ax1← (V, P ) is defined as
world(V ) → (¬pos(V, P 0 ) → pos(V, N 0 )),
where N 0 := ¬P ˙ ,
0 :=
P Ṗ .
Macro 20 ax4 (V, P ) is defined as
world(V ) → (pos(V, P 0 ) → ∀W (r(V, W ) → pos(W, P 0 ))),
where P 0 := Ṗ .
Theorem T2 is rendered by the following macro with ess unfolded, which per-
mits expansion into a universal second-order formula without occurrence of a
predicate in argument position.
Applying SOQE in Inspecting Gödel’s Ontological Proof 105
Macro 21 proto_thm2 (V, X) is defined as
world(V ) → (e(V, X) → (g(V, X) → ∀Q val _ess(V, g, X, Q))).
Macro 22 pre _proto_thm2 (V, X, Q) is defined as
ax1← (V, Q) ∧
∀W (r(V, W ) → ∀X (e(W, X) → def1→ (W, X, Q))) ∧
def1→¬ (V, X, Q) ∧
ax4 (V, Q).
˙ pre _proto_thm2 (v, x, q) → proto_thm2 (v, x).
This formula is valid: ∀q ∃q̇∃¬q
In this implication on the left side the constants q̇ and ¬q,˙ which represent
predicates q and λvx.¬q(v, x) in argument positions, are existentially quantified.
3.4 Necessarily, God Exists – Proving Theorem T3
The definiens of necessary existence, which is defined in Definition D3, is ren-
dered here by the following macro val _ne, expressed in terms of val _ess, the
representation of the definiens of essence, to avoid the occurrence of a predicate
representative in argument position.
Macro 23 val _ne(V, X) is defined as
∀P (∀Q val _ess(V, P, X, Q) →
∀W (r(V, W ) → ∃Y (e(W, Y ) ∧ P (W, Y )))).
Eliminating the quantified predicates shows another view on necessary existence.
Input: val _ne(v, x).
Result of elimination:
∀y (r(v, y) → y = v) ∧ ∀y (r(v, y) → e(y, x)).
The elimination result can be brought into a more clear form.
This formula is valid: ∀w (r(v, w) → w = v ∧ e(w, x)) ↔ last _result.
In analogy to the definition of the predicate ess in Macro 18 we define the
predicate ne in terms of val _ne.
Macro 24 def3 (V, X) is defined as
world(V ) → (e(V, X) → (ne(V, X) ↔ val _ne(V, X))).
The following formula renders a fragment of the definition of necessary existence
on a “shallow” level, that is, in terms of just the predicates ess and ne, without
referring to their definientia val _ess and val _ne.
Macro 25 def3→ (V, X, P ) is defined as
world(V ) →
(e(V, X) →
(ne(V, X) →
(ess(V, P 0 , X) →
∀W (r(V, W ) → ∃Y (e(W, Y ) ∧ P (W, Y )))))),
where P 0 := Ṗ .
106 Christoph Wernhard
Correctness of def3→ can be established by showing that it follows from the
definitions of ess and ne.
This formula is valid: def2 (v, p) ∧ def3 (v, x) → def3→ (v, x, p).
The following macro renders T2, in contrast to Macro 21 now expressed in
terms of the predicate ess instead of its definiens val _ess.
Macro 26 thm2 (V, X) is defined as
world(V ) → (e(V, X) → (g(V, X) → ess(V, ġ, X))).
Axiom A5 (pos(ne)) is represented as follows.
Macro 27 ax5 (V ) is defined as
world(V ) → pos(V, ne).
˙
Scott’s version [25] shows theorem T3 via the lemma L, rendered as follows.
Macro 28 lemma2 (V ) is defined as
world(V ) →
(∃X (e(V, X) ∧ g(V, X)) →
∀W (r(V, W ) → ∃Y (e(W, Y ) ∧ g(W, Y )))).
Macro 29 pre _lemma2 (V, X) is defined as
ax5 (V ) ∧
def1→ (V, X, ne) ∧
def3→ (V, X, g) ∧
thm2 (V, X).
This formula is valid: ∀v (∀x pre _lemma2 (v, x) → lemma2 (v)).
The following formula states theorem T3, the overall result to show.
Macro 30 thm3 (V ) is defined as
world(V ) → ∀W (r(V, W ) → ∃Y (e(W, Y ) ∧ g(W, Y ))).
Macro 31 pre _thm3 (V ) is defined as r _world1 ∧ ∀v lemma2 (v) ∧ coro(V ).
Macro 32 euclidean is defined as ∀x∀y∀z (r(x, y) ∧ r(x, z) → r(z, y)).
Macro 33 symmetric is defined as ∀x∀y (r(x, y) → r(y, x)).
This formula is valid: symmetric ∨ euclidean → (pre _thm3 (v) → thm3 (v)).
As observed in [7], T3 can not be just proven in the modal logic S5, but also
in KB, whose accessibility relation is just constrained to be symmetric. We
have shown here in a single statement that the proof is possible for a Euclidean
as well as a symmetric accessibility relation by presupposing the disjunction of
both properties. Precondition pre _thm3 includes coro instantiated with just the
current world and lemma2 with a universal quantifier upon the world parameter.
In fact, as shown now, using lemma2 there just instantiated with the current
world would not be sufficient to derive thm3 .
This formula is not valid: symmetric ∨ euclidean → (r _world1 ∧ lemma2 (v) ∧
coro(v) → thm3 (v)).
In [31] further aspects of Gödel’s proof are modeled, in particular modal
collapse and monotheism.
Applying SOQE in Inspecting Gödel’s Ontological Proof 107
4 On Weakening the Frame Condition for Theorem T3
In the proof of thm3 from pre _thm3 we used the additional frame condition
euclidean ∨ symmetric. The observation that the weaker KB instead of S5 suf-
fices to prove T3 was an important finding of [7]. Hence, the question arises
whether the precondition on the accessibility relation can be weakened further.
In general, the weakest sufficient condition [19,11,28] of a formula G on a
set Q of predicates within a formula F can be expressed as the second-order
formula ∀p1 . . . ∀pn (F → G), where p1 , . . . , pn are all predicates that occur free
in F → G and are not members of Q. This formula denotes the weakest (with
respect to entailment) formula H in which only predicates in Q occur free such
that H → (F → G) is valid. Second-order quantifier elimination can be applied
to this formula to “compute” a weakest sufficient condition, that is, converting it
to a first-order formula, which, of course, is inherently not possible in all cases.
For T3, the weakest sufficient condition on the accessibility relation r and
the domain membership relation and e is the second-order formula
∀g ∀v (pre _thm3 (v) → thm3 (v)).
Unfortunately, elimination of the second-order quantifier upon g fails for this
formula (at least with the current version of PIE). But elimination succeeds for
a simplified variant of the problem, which considers just propositional modal
logic and combines two instances of Lemma lemma2 with an unfolding of C.
The way in which this simplification was obtained is outlined in [31].
Macro 34 lemma2 _simp(V ) is defined as
g(V ) → ∀W (r(V, W ) → g(W )).
Macro 35 pre _thm3 _simp_inst(V ) is defined as
lemma2 _simp(V ) ∧
∃W (r(V, W ) ∧ g(W ) ∧ lemma2 _simp(W )).
Macro 36 thm3 _simp(V ) is defined as
∀W (r(V, W ) → g(W )).
This formula is valid: euclidean ∨ symmetric → (pre _thm3 _simp_inst(v) →
thm3 _simp(v)).
Input: ∀g ∀v (pre _thm3 _simp_inst(v) → thm3 _simp(v)).
Result of elimination:
∀x∀y∀z (r(x, y) ∧ r(x, z) → r(y, x) ∨ r(y, z) ∨ x = y ∨ y = z).
We write the resulting first-order formula in a slightly different form, give it a
name, verify equivalence to the original form and show some of its properties.
Macro 37 frame _cond _simp is defined as
∀x∀y∀z (r(x, y) ∧ r(x, z) ∧ y 6= x ∧ y 6= z → r(y, x) ∨ r(y, z)).
This formula is valid: frame _cond _simp ↔ last _result.
108 Christoph Wernhard
Macro 38 reflexive is defined as ∀x r(x, x).
This formula is valid: reflexive → (symmetric∨euclidean ↔ frame _cond _simp).
This formula is valid: symmetric ∨ euclidean → frame _cond _simp.
This formula is not valid: frame _cond _simp → symmetric ∨ euclidean.
Thus, the obtained frame condition frame _cond _simp is under the assumption
of reflexivity equivalent to symmetric ∨ euclidean, and without that assumption
strictly weaker. The following statement shows that this weaker frame condition
also works for our original problem, proving T3.
This formula is valid: frame _cond _simp → (pre _thm3 (v) → thm3 (v)).
Hence, via the detour through elimination applied to a simplified problem, we
have found a strictly weaker frame condition for T3 than symmetric ∨ euclidean,
but, since elimination has just been performed on the second-order formula rep-
resenting the simplified problem, we do not know whether it is the weakest one.
5 Conclusion
We reconstructed Gödel’s ontological proof in an environment that integrates au-
tomated first-order theorem proving, second-order quantifier elimination, a for-
mula macro mechanism and LATEX-based formula pretty-printing, supplementing
a number of previous works that render Gödel’s proof in other automated the-
orem proving environments. Particular observations of interest for the study of
Gödel’s proof that became apparent through our modeling include the following:
1. The presentation of the derivation of theorem T1 exhibits the few actually
used instantiations of axioms A1 and A2. The derivation is via a lemma,
which might be useful as internal interface in the proof because it can be
justified in alternate ways.
2. Corollary C can be shown independently from the actual definition of God-
like (D1) just on the basis of the assumption that T1 applies to God-like.4
3. In the whole proof, definition D1 is only used in the left-to-right direction.5
4. Second-order quantifier elimination yields first-order representations of
essence (definition D2) and necessary existence (definition D3).
5. Lemma L can be derived independently from the definiens of essence. Here
the predicate ess appears in the respective expanded formula passed to the
reasoner, but not its definiens.
6. For the derivation of theorem T3 an accessibility relationship is sufficient
that, unless reflexivity is assumed, is strictly weaker than the disjunction of
the Euclidean property and symmetry.
If non-experts in automated reasoning are addressed, the syntactical presen-
tation of Gödel’s argument is of particular importance [8]. We approached this
4
This is also apparent in [5, Fig. 4, line 20].
5
This applies if A3 is given as in Scott’s version, but not if it is derived from further
general properties of positive, as in Gödel’s original version and in [5, Fig. 4, line 19].
Applying SOQE in Inspecting Gödel’s Ontological Proof 109
requirement by means of formula macro definitions with the representation of
input formulas by Prolog terms and LATEX pretty-printing for output formulas.
Most automated formalizations of metaphysical arguments, e.g., [12,24,7,8,5],
seem closely tied to a particular system or combination of systems. Of course,
processing a PIE document similarly depends on the PIE system with specific
embedded reasoners. However, a system-independent view on the formalization
is at least obtainable: The underlying target logic of the macro expansion is
just the well-known classical first-order logic extended with predicate quantifi-
cation. Reasoning tasks are only performed on the expanded formulas. The PIE
system can output these explicitly (see, e.g., [31]), providing a low-level, but
system-independent logical representation of the complete formalization. As a
further beneficial aspect, such an explicit low-level formalization may prevent
the unnoticed interaction with features of involved special logics.
A limitation of our approach might be that there is no automated support
for the passage from the low to the high level, i.e., folding into formula macros. If
trust in proofs is an issue, steps in the overall workflow for which no proof repre-
sentations are produced may be objectionable. This concerns macro expansion,
formula normalization (see, however, [21]), pre- and postprocessing of formulas,
and in particular second-order quantifier elimination, for which the creation of
proofs seems an unexplored terrain. A practical makeshift is comparison with
the few other elimination systems [2, Sect. 4].
In principle it should be possible to integrate second-order quantifier elimi-
nation as used here also into automated reasoning environments based on other
paradigms, in particular the heterogeneous environments that involve forms of
higher-order reasoning and are applied in [7,8,6,5].
Concerning second-order quantifier elimination, an issue that might be worth
further investigation is the generalization of the method applied here ad-hoc to
weaken the precondition on the accessibility relation: We started from an elimina-
tion problem that could not be solved (at least with the current implementation
of PIE), moved to a simpler problem and then verified that the solution of the
simpler problem is also applicable to the original problem, where it does not rep-
resent the originally desired unique weakest sufficient condition, but nevertheless
a condition that is weaker than the condition known before.
Acknowledgments. The author thanks Christoph Benzmüller and anonymous
reviewers for helpful remarks. Funded by the Deutsche Forschungsgemeinschaft
(DFG, German Research Foundation) – Project-ID 457292495.
References
1. Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathemati-
schen Logik. Math. Annn. 110, 390–413 (1935). https://doi.org/10.1007/BF0144
8035
2. Alassaf, R., Schmidt, R.A.: DLS-Forgetter: An implementation of the DLS for-
getting calculus for first-order logic. In: Calvanese, D., Iocchi, L. (eds.) GCAI
110 Christoph Wernhard
2019. EPiC Series in Computing, vol. 65, pp. 127–138. EasyChair (2019). https:
//doi.org/10.29007/hvz6
3. van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis (1983)
4. van Benthem, J.: Modal Logic for Open Minds. CSLI Publications (2010)
5. Benzmüller, C.: A (simplified) supreme being necessarily exists, says the computer:
Computationally explored variants of Gödel’s ontological argument. In: Calvanese,
D., Erdem, E., Thielscher, M. (eds.) KR 2020. pp. 779–789. IJCAI organization
(2020). https://doi.org/10.24963/kr.2020/80
6. Benzmüller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis
of the Anderson-Hájek ontological controversy. Logica Universalis 11(1), 139–151
(2017). https://doi.org/10.1007/s11787-017-0160-9
7. Benzmüller, C., Woltzenlogel Paleo, B.: Automating Gödel’s ontological proof of
god’s existence with higher-order automated theorem provers. In: Schaub, T.,
Friedrich, G., O’Sullivan, B. (eds.) ECAI 2014. FAIA, vol. 263, pp. 93–98. IOS
Press (2014). https://doi.org/10.3233/978-1-61499-419-0-93
8. Benzmüller, C., Woltzenlogel Paleo, B.: The inconsistency in Gödel’s ontological
argument: A success story for AI in metaphysics. In: Kambhampati, S. (ed.) IJCAI
2016. pp. 936–942. AAAI Press (2016), https://www.ijcai.org/Proceedings/16/P
apers/137.pdf
9. Dahn, I., Wernhard, C.: First order proof problems extracted from an article in
the Mizar mathematical library. In: FTP’97. pp. 58–62. RISC-Linz Report Series
No. 97–50, Joh. Kepler Univ., Linz (1997), https://www.logic.at/ftp97/papers/da
hn.pdf
10. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited:
A reduction algorithm. JAR 18(3), 297–338 (1997). https://doi.org/10.1023/A:
1005722130532
11. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing strongest necessary and
weakest sufficient conditions of first-order formulas. In: Nebel, B. (ed.) IJCAI-
01. pp. 145–151. Morgan Kaufmann (2001), https://www.ijcai.org/Proceedings/
01/IJCAI-2001-b.pdf#page=133
12. Fitelson, B., Zalta, E.N.: Steps toward a computational metaphysics. J. Philos.
Log. 36(2), 227–247 (2007). https://doi.org/10.1007/s10992-006-9038-7
13. Fitting, M.: Types, Tableaus, and Gödel’s God. Springer (2002). https://doi.org/
10.1007/978-94-010-0411-4
14. Gödel, K.: Ontologischer Beweis – notes in Kurt Gödel’s hand (1970), transcrip-
tions published in [27, pp. 144–145] and also in [26, pp. 256–257]
15. Kanckos, A., Lethen, T.: The development of Gödel’s ontological proof. Review of
Symbolic Logic pp. 1–19 (2019). https://doi.org/10.1017/s1755020319000479
16. Kanckos, A., Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a
natural deduction calculus. Studia Logica 105, 553–586 (2017). https://doi.org/
10.1007/s11225-016-9700-1
17. Kirchner, D., Benzmüller, C., Zalta, E.N.: Computer science and metaphysics: A
cross-fertilization. Open Philosophy 2, 230–251 (2019). https://doi.org/10.1515/
opphil-2019-0015
18. Knuth, D.E.: Literate programming. Comput. J. 27(2), 97–111 (1984)
19. Lin, F.: On strongest necessary and weakest sufficient conditions. Artificial Intel-
ligence 128, 143–159 (2001). https://doi.org/10.1016/S0004-3702(01)00070-4
20. McCune, W.: Prover9 and Mace4 (2005–2010), http://www.cs.unm.edu/~mccune
/prover9
Applying SOQE in Inspecting Gödel’s Ontological Proof 111
21. de Nivelle, H.: Extraction of proofs from the clausal normal form transformation.
In: Bradfield, J. (ed.) CSL 2002. LNCS, vol. 2471, pp. 584–598. Springer (2002).
https://doi.org/10.1007/3-540-45793-3_39
22. Ohlbach, H.J.: SCAN – elimination of predicate quantifiers: System description.
In: McRobbie, M.A., Slaney, J.K. (eds.) CADE-13. LNCS (LNAI), vol. 1104, pp.
161–165. Springer (1996). https://doi.org/10.1007/3-540-61511-3_77
23. Ohlbach, H.J., Engel, T., Schmidt, R.A., Gabbay, D.M.: SCAN, http://www.me
ttel-prover.org/scan/index.html
24. Oppenheimer, P.E., Zalta, E.N.: A computationally-discovered simplification of
the ontological argument. Australasian J. Philos. 89(2), 333–349 (2011). https:
//doi.org/10.1080/00048401003674482
25. Scott, D.: Gödel’s ontological proof – notes in Dana Scott’s hand (1970), transcrip-
tions published in [27, pp. 145–146] and also in [26, pp. 257–258]
26. Sobel, J.H.: Gödel’s ontological proof. In: Thomson, J.J. (ed.) On Being and Saying:
Essays for Richard Cartwright. MIT Press, Cambridge, MA (1987)
27. Sobel, J.H.: Logic and Theism: Arguments For and Against Beliefs in God. Cam-
bridge University Press, Cambridge (2004). https://doi.org/10.1017/CBO9780511
497988
28. Wernhard, C.: Projection and scope-determined circumscription. Journal of Sym-
bolic Computation 47, 1089–1108 (2012). https://doi.org/10.1016/j.jsc.2011.12.
034
29. Wernhard, C.: The PIE system for proving, interpolating and eliminating. In:
Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR 2016. CEUR Workshop Proceed-
ings, vol. 1635, pp. 125–138. CEUR-WS.org (2016), http://ceur-ws.org/Vol-1635
/paper-11.pdf
30. Wernhard, C.: Facets of the PIE environment for proving, interpolating and elim-
inating on the basis of first-order logic. In: Hofstedt, P., et al. (eds.) DECLARE
2019, Revised Selected Papers. LNCS (LNAI), vol. 12057, pp. 160–177. Springer
(2020). https://doi.org/10.1007/978-3-030-46714-2_11
31. Wernhard, C.: Applying second-order quantifier elimination in inspecting Gödel’s
ontological proof (extended version). Tech. rep. (2021), https://arxiv.org/abs/21
10.11108