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 become apparent. Practical application possibilities of second-order quantifier elimination are shown and the encountered elimination tasks may serve as benchmarks.
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 classical 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
approach 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 [
A PIE document is a Prolog source file that contains declarative formula macro
definitions and specifications of reasoner invocations, interspersed with ALTEX
comments in the manner of literate programming [
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
firstorder logic is DLS-Forgetter [
As embedded reasoners we used the first-order theorem provers Prover9 [
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 instantiated 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 firstorder 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 ∨ G) def ¬STS T(F( F)∨) ST (G) = = ST (∃ xF ) def ST (♦F ) def ∃ x (e(v, x) ∧ ST (F )) = = ∃ w (r(v, w) ∧ Vi s.th. xi free in F e(w, xi) ∧ ST (F ){ v 7→ w} ) 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
[
∀ 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 implying 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 T3 Necessarily, God exists
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)
∃ x G(x)
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 , ˙
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 constants 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 P˙ and ¬ ˙P , available for each predicate symbol P .
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 where world(V ) (pos(V, P 0) ∀ W (r(V, W )
∀ X (e(W, X) → pos(V, Q0)), (P (W, X) →
Q(W, X)))) ˙ P 0 := P ,
˙ 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, ⊥ ˙ ).
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 concerning > 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 [
This formula is valid: pre_lemma1 (v) → lemma1 (v).
T1 can be rendered by the following macro with a predicate parameter. Macro 9 thm1 (V, P ) is defined as world(V ) (pos(V, P 0) ∃ W (r(V, W ) ∧ ∃ →
→ 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 instance of ax2 – beyond that used to prove lemma1 – is required there, with respect to ⊥ and the given predicate P .
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, g˙ ).
Macro 12 coro(V ) is defined as world(V ) → ∃ W (r(V, W ) ∧ ∃
X (e(W, X) ∧ g(W, X))).
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 def 1→ and def 1→¬ defined below. 3.3
Essence – Proving Theorem T2 With macros def 1→ and def 1→¬ , defined now, we represent the left-to-right direction of D1. Actually, only this direction of D1 is required for the proving the further theorems.
Macro 14 def 1→ (V, X, P ) is defined as
g(V, X) → (pos(V, P 0) → P (V, X)), where where Macro 15 def 1→¬ (V, X, P ) is defined as g(V, X) → (pos(V, P 0) → ¬
The following macro val_ess renders the definiens of the essence of relationship 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. 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.
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)),
In [
The following two macros render the right-to-left direction of axioms A1 and A4. The original axioms involve a universally quantified predicate that appears only in argument role. In the macros, it is represented by the parameter P . Theorem T2 is rendered by the following macro with ess unfolded, which permits expansion into a universal second-order formula without occurrence of a predicate in argument position.
(¬ pos(V, P 0) →
N 0 := ¬ ˙P ,
˙ P 0 := P . Macro 21 proto_thm2 (V, X) is defined as Macro 22 pre_proto_thm2 (V, X, Q) is defined as world(V ) → (e(V, X) → (g(V, X) → ∀
Q val_ess(V, g, X, Q))). ax1← (V, Q) ∀ W (r(V, W ) → ∀ def 1→¬ (V, X, Q) ax4 (V, Q).
X (e(W, X) →
∧ def 1→ (W, X, Q))) ∧ ∧ This formula is valid: ∀ q ∃ q˙∃ ¬ ˙q pre_proto_thm2 (v, x, q) → proto_thm2 (v, x).
3.4
Necessarily, God Exists – Proving Theorem T3 The definiens of necessary existence, which is defined in DefinitionD3, is rendered 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 predicatesess and ne, without referring to their definientia val_ess and val_ne.
Macro 25 def 3→ (V, X, P ) is defined as where world(V ) (e(V, X) (ne(V, X) (ess(V, P 0, X) ∀ W (r(V, W ) → ∃
Y (e(W, Y ) ∧ P (W, Y )))))),
˙ P 0 := P .
→ → → → Correctness of def 3→ 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) → def 3→ (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, g˙ , X))).
Axiom A5 (pos(ne)) is represented as follows.
Macro 27 ax5 (V ) is defined as
world(V ) → pos(V, n˙e).
Scott’s version [
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)).
This formula is valid: symmetric ∨ euclidean → (pre_thm3 (v) → thm3 (v)).
As observed in [
This formula is not valid: symmetric ∨ euclidean → coro(v) → thm3 (v)). (r _world1 ∧ lemma2 (v) ∧
In [
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
suffices to prove T3 was an important finding of [
In general, the weakest sufficient condition [
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) →
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 [
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 ) → This formula is valid: euclidean ∨ symmetric → thm3 _simp(v)). g(W )).
Result of elimination: thm3 _simp(v)).
(pre_thm3 _simp_inst(v) → ∀ 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 → This formula is valid: frame_cond_simp ↔ last_result. r(y, x) ∨ r(y, z)).
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) →
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 representing the simplified problem, we do not know whether it is the weakest one. 5
We reconstructed Gödel’s ontological proof in an environment that integrates automated first-order theorem proving, second-order quantifier elimination, a formula macro mechanism and LATEX-based formula pretty-printing, supplementing a number of previous works that render Gödel’s proof in other automated theorem 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 Godlike (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
presentation of Gödel’s argument is of particular importance [
Most automated formalizations of metaphysical arguments, e.g., [
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
representations are produced may be objectionable. This concerns macro expansion,
formula normalization (see, however, [
In principle it should be possible to integrate second-order quantifier
elimination 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 [
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 elimination 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 represent 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.