A Gödelian Ontological Proof with More Plausible Axiological Principles

Johan E. Gustafsson; Johan E. Gustafsson

doi:10.3998/ergo.9866

A drawback of the standard modal ontological proof is its assumption that it's possible that there is something godlike. Kurt Gödel's ontological proof seeks to establish this possibility with the help of some axiological principles. But the axiological principles he relies on are implausible. And the same goes for other Gödelian ontological proofs in the literature. In this paper, I put forward a Gödelian ontological proof that only relies on plausible axiological principles. And I adapt the proof both for constant and varying domains. Nevertheless, the proof still needs the axiom that being godlike is positive in the sense of being a "purely good"-making property.

How to Cite: Gustafsson, J. E. (2026) “A Gödelian Ontological Proof with More Plausible Axiological Principles”, Ergo an Open Access Journal of Philosophy. 13(0). doi: https://doi.org/10.3998/ergo.9866

The standard modal ontological proof for the existence of a godlike being runs as follows: It’s possible that something godlike exists. That something godlike exists strictly entails that it’s necessary that something godlike exists. Therefore, by standard principles of modal logic, something godlike exists.¹

A drawback of this proof is its assumption that it’s possible that there is something godlike. Kurt Gödel’s ontological proof seeks to establish this possibility with the help of some axiological principles. Given these principles, he shows that it’s possible that there is something godlike.² But the axiological principles he relies on are implausible. And the same goes for other Gödelian ontological proofs in the literature. In this paper, I will put forward a Gödelian ontological proof that only relies on plausible axiological principles. And I will adapt the proof for both constant and varying domains.

Gödel’s proof relies on the principle that, for all properties, exactly one of the property and its complement is positive:³

Here,

P (ϕ)

states that property

ϕ

is positive. A positive property is, according to Gödel, a property that is “positive in the moral aesthetic sense.”⁴ He adds that positive properties can be interpreted as perfective properties—that is, “purely good”-making properties.⁵

The right-to-left direction of (1) is implausible. There seem to be neutral properties such that neither the property nor its complementary property is positive.⁶ The property of being male seems neutral and hence not positive, but the property of not being male also seems neutral and not positive.⁷

Gödel’s proof also relies on the principle that any property that is entailed by a positive property is likewise positive:⁸

Yet this principle is implausible as well. Let

G

be the property of being godlike and

D

be the property of being devil-like. While

G

seems positive (as we will assume later on),

G ∨ D

(the property of being godlike or devil-like) does not seem positive.⁹ Yet

G

implies

G ∨ D

. So, according to (2), if

G

is positive, then

G ∨ D

is positive too. But there seems to be no more reason to regard

G ∨ D

as positive than to regard it as negative.¹⁰ (If one doesn’t accept that the magnitude of the negativity of

D

matches the magnitude of the positivity of

G

, one could replace

G

and

D

with some other pair whose positive and negative properties are alike in magnitude.)

Similarly, tautological properties like

G ∨ ¬ G

(the property of being godlike or not godlike) do not seem positive even if one of their disjuncts is positive.¹¹ But, according to (2), if

G

is positive, then

G ∨ ¬ G

is also positive.

Furthermore, it seems that, if (2) holds for the logic of positivity, then the following analogous principle should hold for the logic of negativity, where

N (ϕ)

states that property

ϕ

is negative:

This is the principle that any property that is entailed by a negative property is likewise negative. If we accept both (2) and (3), we find that

G ∨ D

is both positive and negative, which conflicts with the following principle:¹²

This principle (that no property is both positive and negative) is plausible given an axiological form of positivity and negativity. It mirrors a standard principle of the logic of value, namely, that nothing is both intrinsically good and intrinsically bad.¹³

Petr Hájek’s version of the ontological proof relies on the following principle:¹⁴

This principle states that all positive properties are logically compatible. If any Gödelian ontological proof is to have any success in showing that there is a godlike being that has all positive properties, then those properties need to be logically compatible. But it’s unclear why we should accept this principle. It has no compelling analogue in the logic of value.

It may then seem that Gödelian ontological proofs need to rely on questionable axiological principles. In the following, however, I will put forward a Gödelian ontological proof that does not rely on such principles.

1. Constant Domain

We adopt two general formal axiological principles as axioms. The first axiom states that co-entailing properties are alike in positivity:¹⁶

(C1)
$∀ ϕ ∀ ψ (□ ∀ x (ϕ (x) ≡ ψ (x)) ⊃ (P (ϕ) ≡ P (ψ))) .$

The second axiom states that contradictory properties are not positive:¹⁷

(C2)
$∀ ϕ ¬ P (ϕ & ¬ ϕ) .$

In an earlier work, I showed that these principles are sufficient to derive the first half of Gödel’s proof—that is, that, if a property is positive, then it’s possible that there exists something that has that property.¹⁸ Here, however, we will show that we can prove the necessary existence of something godlike without assuming any other formal axiological principles (still, we will need a substantial axiological axiom).

We define the property of being godlike as follows:¹⁹

(C3)
$G (x) = df ∀ ϕ (P (ϕ) ⊃ □ ϕ (x)) .$

That is, something is godlike if and only if it has all positive properties necessarily. And we adopt the following substantial axiological axiom:²⁰

(C4)
$P (G) .$

That is, the property of being godlike is positive.

We seek to prove that it’s necessary that there exists something godlike:

(C5)
$□ ∃ x G (x) .$

We can prove the following theorem:

Theorem 1: Given axioms and definitions (C1), (C2), (C3), and (C4), we can derive (C5) in second-order system KB.

For proof, see Appendix A.

Our two general axiological principles, (C1) and (C2), both mirror standard principles of the logic of value.

Axiom (C1) mirrors the principle that logically equivalent states of affairs have the same intrinsic value.²¹ There is a straightforward rationale for (C1): If two properties mutually entail each other, any goodness and badness that is entailed by one of them is also entailed by the other. Hence the properties necessarily have the same advantages and disadvantages and so should be alike in positivity.²²

Axiom (C2) mirrors the principle that contradictory states of affairs are not intrinsically good.²³ And there is a rationale also for (C2): contradictions entail everything; so, for every good or bad thing they entail, they also entail the complement. Contradictions are symmetrical in their relation to the good and the bad. Hence they are neither intrinsically good nor positive.²⁴

The proof of the theorem relies on second-order system KB.²⁵ System K is normal modal logic, that is, propositional logic combined with the necessitation rule and the distribution axiom:²⁶

K
$□ (p ⊃ q) ⊃ (□ p ⊃ □ q) .$

System KB is system K combined with the Brouwerian axiom:²⁷

B
$p ⊃ □ ◇ p .$

Possibility, here, is defined as the dual of necessity:²⁸

$◇ p = df ¬ □ ¬ p .$

Note that system KB does not include the necessity axiom:²⁹

T
$□ p ⊃ p .$

So one may wonder whether our assumptions allow us to derive that something godlike exists:

(C6)
$∃ x G (x) .$

Nevertheless, we can prove the following corollary:

Corollary 1: Given axioms and definitions (C1), (C2), (C3), and (C4), we can derive (C6) in second-order system KB.

For proof, see Appendix B.

2. Varying Domain

One worry about Theorem 1 is that it relies on a constant domain.³⁰ To get around this, we can move to a varying-domain setting with an existence predicate.³¹ Let $E$ be a predicate applied to individuals, with $E (x)$ read as ‘ $x$ concretely exists.’ Then we adopt the following definitions:³²

$∀ E x ϕ (x)$ $= df$ $∀ x (E (x) ⊃ ϕ (x)) .$
$∃ E x ϕ (x)$ $= df$ $∃ x (E (x) & ϕ (x)) .$

We adopt the following axiological principles as axioms, where (V1) is a varying-domain analogue of (C1) and where (V2) is the same as (C2):³³

(V1)
$∀ ϕ ∀ ψ (□ ∀ E x (ϕ (x) ≡ ψ (x)) ⊃ (P (ϕ) ≡ P (ψ))) .$
(V2)
$∀ ϕ ¬ P (ϕ & ¬ ϕ) .$

We define the property of being godlike as before:³⁴

(V3)
$G (x) = df ∀ ϕ (P (ϕ) ⊃ □ ϕ (x)) .$

And we adopt the following substantial axiological axiom:³⁵

(V4)
$P (G & E) .$

That is, the property of being godlike and concretely existing is positive. And we seek to prove that it’s necessary that there concretely exists something godlike:

(V5)
$□ ∃ E x G (x) .$

We can prove the following theorem:

Theorem 2: Given axioms and definitions (V1), (V2), (V3), and (V4), we can derive (V5) in second-order system KB.

For proof, see Appendix C.

Our assumptions also let us derive that something godlike concretely exists:

(V6)
$∃ E x G (x) .$

That is, we can prove the following corollary:

Corollary 2: Given axioms and definitions (V1), (V2), (V3), and (V4), we can derive (V6) in second-order system KB.

For proof, see Appendix D.

3. Are These Proofs Compelling?

Given that (C1), (C2), (V1), and (V2) are plausible axiological principles, are these proofs compelling arguments for their conclusion? Since (C3) and (V3) are definitions and the required modal system (second-order system KB) is fairly weak, it seems that whether we should accept the argument rests on whether we should accept the remaining axioms, (C4) and (V4). Unlike the other axiological axioms, (C4) and (V4) are not general formal axiological principles—that is, general principles about the formal structure of the positivity or value of properties. They are substantial axiological claims—that is, claims that a specific property is positive.

If we grant that there are positive properties and that they are jointly consistent, then it’s plausible that $G$ or $G & E$ is positive. The trouble is that it’s unclear why we should grant this.³⁶

That said, the upshot of this paper is still that, if we grant that $G$ or $G & E$ is positive, the conclusion follows. And, unlike earlier Gödelian ontological proofs, we have shown this without relying on implausible axiological principles.

Notes

Hartshorne (1962: 51) and Plantinga (1974a: 111; 1974b: 214). ⮭

Gödel (1987; 1995a), following in the tradition of Leibniz (1676/1969: 167). Nonetheless, Anderson (2015: 286–288), who once defended a Gödelian ontological proof in Anderson (1990), prefers Hartshorne’s standard modal ontological proof. Gödel, however, was critical of Hartshorne’s proof. See Wang (1996: 146) and Kanckos and Lethen (2022: 188–190). ⮭

Gödel (1987: 256; 1995a: 403). Magari (1988: 13), Fitting (2002: 146, 165), and Kovač (2003: 572) rely on the same principle. If

ϕ

is a property, then

¬ ϕ

is an abbreviation of

λ x (¬ (ϕ (x)))

, where

λ x (f (x))

is a property an individual

y

has in virtue of being such that

f (y)

. If

ϕ

and

ψ

are properties, then

ϕ ∨ ψ

is an abbreviation of

λ x (ϕ (x) ∨ ψ (x))

. Likewise,

ϕ & ψ

is an abbreviation of

λ x (ϕ (x) & ψ (x))

. See Carnap (1947: 3). ⮭

Gödel (1987: 257; 1995a: 404). Bjørdal (1999: 215) defines positivity in terms of godlikeness rather than in terms of value—namely, he takes a positive property to be a property such that it’s necessary that any godlike being has the property. This does not fit with an axiological interpretation of positivity, since, on Bjørdal’s view, tautological properties would be positive (whereas, axiologically, they seem to be neutral rather than positive). Alternatively, Gödel (1987: 257; 1995a: 404; 1995b: 435) suggests that ‘positive’ could be understood as ‘attribution’ (as opposed to ‘privation’). See Hazen (1998: 375–376), however, for an objection to the attribution approach. ⮭

Gödel (1995b: 435). Presumably, we need to restrict positivity to intrinsic properties—see Sobel (2004: 561, fn 20), Kovač (2003: 569), and Koons (2006: 239–240)—and to non-limiting properties, that is, properties that are non-limiting in the sense that they do not rule out that one has a good-making property to some greater degree. For example, the property of being benevolent to the positive degree

n

seems to be a good-making property but it rules out being benevolent to any higher degree. (I thank Krister Bykvist for this point.) ⮭

Anderson (1990: 295). ⮭

Gustafsson (2020: 232). ⮭

Gödel (1995a: 403). Scott (1987: 257), Magari (1988: 14), Anderson (1990: 291), Kovač (2003: 572), Maydole (2003: 301), Johnson (1999: 99; 2004: 121), Pruss (2009: 347; 2012: 203, 205), and Benzmüller (2020: 786; 2022: 958) also rely on this principle. Fitting (2002: 165) relies on a varying-domain analogue. ⮭

Hájek (2002: 150). ⮭

Sobel (2004: 122). See, however, Kovač (2003: 581) for an objection to this claim; and see Gustafsson (2020: fn 11) for a response. ⮭

Sobel (2004: 120; 2006a: 406–407; 2006b: 286) and van Inwagen (2007: 142). ⮭

Gustafsson (2020: 233). ⮭

Chisholm and Sosa (1966: 248). ⮭

Hájek (2002: 156). See also Gödel (1995b: 435) and Cook (2004: 106) for similar principles. ⮭

There is some evidence that Gödel favoured a constant-domain setting. See Kanckos and Lethen (2021: 1014). ⮭

Gustafsson (2020: 235). One may worry that (C1) could fail to hold if we make hyperintensional distinctions among properties—for example, distinguishing being triangular from being trilateral. See Cresswell (1975: 25). One way to mitigate this worry could be to weaken the principle to just say that, if a first property is logically equivalent to the contradictory property of both having and not having the first property, then those properties are alike in positivity:

(C1*)
$∀ ϕ (□ ∀ x (ϕ (x) ≡ ϕ & ¬ ϕ (x)) ⊃ (P (ϕ) ≡ P (ϕ & ¬ ϕ))) .$

The proofs in Appendices A and B still work if (C1) is replaced by (C1*). Even if one might think that being triangular differs in positivity from being trilateral due to a hyperintensional distinction, it seems less plausible that the property of being a triangular circle differs in positivity from the property of being both (i) a triangular circle and (ii) not a triangular circle. Since both properties involve the same concepts, it’s less plausible that a hyperintensional distinction would make a difference for positivity. ⮭

In Gustafsson (2020: 234), I instead used the axiom that the property of being self-different is not positive. But it seems that the reason for believing that the property of being self-different isn’t positive is that it is contradictory. So (C2) seems more fundamental. It may be objected—following Halldén (1957: 41) and Åqvist (1968: 268)—that (C2) is a substantive axiological claim (rather than a formal axiological principle), since it makes a claim about the value of specific properties. But, as I argued in Gustafsson (2020: fn 11), the denial of the positivity of contradictory properties can be done on formal grounds—that is, we can deny their positivity because of their contradictory structure. ⮭

Gustafsson (2020: 234–236). ⮭

Anderson (1990: 294–295) has a biconditional instead of a conditional in the definiens. Hájek (2002: 156) defines that something is godlike as that its necessary properties are those needed to have all positive properties. My definition is weaker in the sense that anything that is godlike by their definitions is also godlike by mine. Note that only the left-to-right direction of my definition is used in the proofs. So we could replace definition (C3) by the following axiom:

(C3*)
$G (x) ⊃ (∀ ϕ (P (ϕ) ⊃ □ ϕ (x))) .$

Since (C3*) can be derived from both Anderson’s and Hájek’s definitions, we could also use their definitions. Anderson’s definition, however, has the drawback that—unless tautological properties are positive—godlike beings are impossible. Gödel (1987: 256; 1995a: 403) defines being godlike as the property of having all positive properties:

(C3**)
$G (x) = df ∀ ϕ (P (ϕ) ⊃ ϕ (x)) .$

That definition, however, is insufficient for the results in this paper. ⮭

Scott (1987: 257). ⮭

Rescher (1966: 58) and Åqvist (1968: 259). ⮭

Gustafsson (2020: 235). ⮭

von Wright (1972: 163–164) and Hansson (2001: 119). ⮭

Gustafsson (2020: 234–235). ⮭

For system KB, see Chellas (1980: 131). ⮭

For system K, see Chellas (1980: 131). And, for axiom K, see Feys (1950: 500) and Chellas (1980: 7). ⮭

For axiom B, see Lewis and Langford (1932: 497) and Chellas (1980: 16). ⮭

Aristotle (Int. 13, 22

b

22–23; An. pr. 1.13 32

a

21–28; 2025: 44, 64), Carnap (1947: 186), and Chellas (1980: 7). ⮭

Carnap (1947: 186) and Chellas (1980: 6). ⮭

Another worry is that it seems to allow a parallel argument that there exists something devil-like. Replacing

G

and

P

with

D

and

N

respectively in (C1)–(C5) seems to yield a similarly plausible argument. If, however, concrete existence is positive and its negation is negative as suggested in Smullyan (2002: 47), then the parallel negative variant of the varying-domain argument in this section is blocked. ⮭

Anderson (1990: fn 14). ⮭

Cresswell (1991: 275, 277), Fitting and Mendelsohn (1998: 106), and Fitting (2002: 90). ⮭

Gustafsson (2020: fn 15). Like before, we could weaken (V1) as follows:

(V1*)
$∀ ϕ (□ ∀ E x (ϕ (x) ≡ ϕ & ¬ ϕ (x)) ⊃ (P (ϕ) ≡ P (ϕ & ¬ ϕ))) .$

See fn 16. ⮭

And, like before, we only make use of the left-to-right direction of the definition—that is, we can replace definition (V3) with the following axiom:

(V3*)
$G (x) ⊃ (∀ ϕ (P (ϕ) ⊃ □ ϕ (x))) .$

See fn 19. ⮭

Hájek (2002: 160). ⮭

Anderson and Gettings (1996: 171), van Inwagen (2007: 144), and Gustafsson (2020: 238). Apart from the well-known worries about the compatibility of traditional divine properties such as omniscience, omnipotence, and omnibenevolence, there is also the worry that some “purely good”-making properties may only be possessed by objects of different kinds. For example, the property of being a pleasure cannot be possessed by people whereas the property of being benevolent can only be possessed by people. To get around this problem, we can restrict

P

to properties that apply to a specific kind of object. (I thank Wlodek Rabinowicz for this point.) ⮭

The proof up to (19) follows Gustafsson (2020: 235–236). ⮭

Acknowledgements

I wish to thank Krister Bykvist, Wlodek Rabinowicz, and Roy Whelden for valuable comments.

References

Anderson, C. Anthony (1990). Some Emendations of Gödel’s Ontological Proof. Faith and Philosophy, 7(3), 291–303.

Anderson, C. Anthony (2015). Gödel’s ‘Proof’ for the Existence of God. In Snezana Lawrence and Mark McCartney (Eds.), Mathematicians and Their Gods: Interactions Between Mathematics and Religious Beliefs (279–289). Oxford University Press.

Anderson, C. Anthony and Michael Gettings (1996). Gödel’s Ontological Proof Revisited. In Petr Hájek (Ed.), Gödel ‘96: Logical Foundations of Mathematics, Computer Science and Physics—Kurt Gödel’s Legacy (167–172). Springer.

Åqvist, Lennart (1968). Chisholm-Sosa Logics of Intrinsic Betterness and Value. Noûs, 2(3), 253–270.

Aristotle (2025). Complete Works (Vol. 1), C. D. C. Reeve and Pavlos Kontos (Eds.). Hackett.

Benzmüller, Christoph (2020). A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel’s Ontological Argument. In Diego Calvanese, Esra Erdem, and Michael Thielscher (Eds.), Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020 (779–789). IJCAI.

Benzmüller, Christoph (2022). Symbolic AI and Gödel’s Ontological Argument. Zygon, 57(4), 953–962.

Bjørdal, Frode (1999). Understanding Gödel’s Ontological Argument. In Timothy Childers (Ed.), The Logica Yearbook 1998 (214–217). Filosofia.

Carnap, Rudolf (1947). Meaning and Necessity: A Study in Semantics and Modal Logic. University of Chicago Press.

Chellas, Brian F. (1980). Modal Logic: An Introduction. Cambridge University Press.

Chisholm, Roderick M. and Ernest Sosa (1966). On the Logic of “Intrinsically Better”. American Philosophical Quarterly, 3(3), 244–249.

Cook, Roy T. (2004). God, the Devil, and Gödel’s Other Proof. In Libor Behounek (Ed.), The Logica Yearbook 2003 (97–109). Filosofia.

Cresswell, M. J. (1975). Hyperintensional Logic. Studia Logica, 34(1), 25–38.

Cresswell, M. J. (1991). In Defence of the Barcan Formula. Logique & Analyse, 34(135–136), 271–282.

Feys, R. (1950). Les systèmes formalisés des modalités aristotéliciennes. Revue philosophique de Louvain, 48(20), 478–509.

Fitting, Melvin (2002). Types, Tableaus, and Gödel’s God. Kluwer.

Fitting, Melvin and Richard L. Mendelsohn (1998). First-Order Modal Logic. Kluwer.

Gödel, Kurt (1987). Ontologischer Beweis. In Judith Jarvis Thomson (Ed.), On Being and Saying: Essays for Richard Cartwright (256–257). MIT Press.

Gödel, Kurt (1995a). Ontological Proof. In John W. Dawson Jr. (Trans.), Collected Works Volume III: Unpublished Essays and Lectures (403–404). Oxford University Press.

Gödel, Kurt (1995b). Texts Relating to the Ontological Proof. In John W. Dawson Jr. (Trans.), Collected Works Volume III: Unpublished Essays and Lectures (429–437). Oxford University Press.

Gustafsson, Johan E. (2020). A Patch to the Possibility Part of Gödel’s Ontological Proof. Analysis, 80(2), 229–240.

Halldén, Sören (1957). On the Logic of ‘Better’. Gleerup.

Hansson, Sven Ove (2001). The Structure of Values and Norms. Cambridge University Press.

Hartshorne, Charles (1962). The Logic of Perfection and Other Essays in Neoclassical Metaphysics. Open Court.

Hazen, A. P. (1998). On Gödel’s Ontological Proof. Australasian Journal of Philosophy, 76(3), 361–377.

Hájek, Petr (2002). A New Small Emendation of Gödel’s Ontological Proof. Studia Logica, 71(2), 149–164.

Johnson, David (1999). Hume, Holism, and Miracles. Cornell University Press.

Johnson, David (2004). Truth without Paradox. Rowman & Littlefield.

Kanckos, Annika and Tim Lethen (2021). The Development of Gödel’s Ontological Proof. The Review of Symbolic Logic, 14(4), 1011–1029.

Kanckos, Annika and Tim Lethen (2022). Kurt Gödel’s Reception of Charles Hartshorne’s Ontological Proof. In Esther Ramharter (Ed.), The Vienna Circle and Religion (183–196). Springer.

Koons, Robert (2006). Sobel on Gödel’s Ontological Proof. Philosophia Christi, 8(2), 235–248.

Kovač, Srećko (2003). Some Weakened Gödelian Ontological Systems. Journal of Philosophical Logic, 32(6), 565–588.

Leibniz, Gottfried Wilhelm (1676/1969). Two Notations for Discussion with Spinoza. In Leroy E. Loemker (Trans.), 2nd ed., Philosophical Papers and Letters (167–169). Reidel.

Lewis, Clarence I. and Cooper H. Langford (1932). Symbolic Logic. Century Company.

Magari, Roberto (1988). Logica e Teofilia: Osservazioni su una dimostrazione attribuita a Kurt Gödel. Notizie di Logica, 7(4), 11–20.

Maydole, Robert (2003). The Modal Perfection Argument for the Existence of a Supreme Being. Philo, 6(2), 299–313.

Plantinga, Alvin (1974a). God, Freedom, and Evil. Harper & Row.

Plantinga, Alvin (1974b). The Nature of Necessity. Clarendon Press.

Pruss, Alexander R. (2009). A Gödelian Ontological Argument Improved. Religious Studies, 45(3), 347–353.

Pruss, Alexander R. (2012). A Gödelian Ontological Argument Improved Even More. In Miroslaw Szatkowski (Ed.), Ontological Proofs Today (203–211). Ontos Verlag.

Rescher, Nicholas (1966). Semantic Foundations for the Logic of Preference. In Nicholas Rescher (Ed.), The Logic of Decision and Action (37–62). University of Pittsburgh Press.

Scott, Dana (1987). Gödel’s Ontological Proof. In Judith Jarvis Thomson (Ed.), On Being and Saying: Essays for Richard Cartwright (257–258). MIT Press.

Smullyan, Raymond (2002). Some Interesting Memories: A Paradoxical Life. Thinkers’ Press.

Sobel, Jordan Howard (2004). Logic and Theism: Arguments for and against Beliefs in God. Cambridge University Press.

Sobel, Jordan Howard (2006a). On Gödel’s Ontological Proof. In Henrik Lagerlund, Sten Lindström, and Rysiek Sliwinski (Eds.), Modality Matters: Twenty-Five Essays in Honour of Krister Segerberg (397–421). Uppsala Universitet.

Sobel, Jordan Howard (2006b). To My Critics with Appreciation: Responses to Taliaferro, Swinburne, and Koons. Philosophia Christi, 8 (2), 249–292.

van Inwagen, Peter (2007). Some Remarks on the Modal Ontological Argument. In Matthias Lutz-Bachmann and Thomas M. Schmidt (Eds.), Metaphysik heute: Probleme und Perspektiven der Ontologie / Metaphysics Today: Problems and Prospects of Ontology (132–145). Alber.

von Wright, Georg Henrik (1972). The Logic of Preference Reconsidered. Theory and Decision, 3(2), 140–169.

Wang, Hao (1996). A Logical Journey: From Gödel to Philosophy. MIT Press.

Appendices

A. Proof of Theorem 1

Theorem 1: Given axioms and definitions

(C1)
$∀ ϕ ∀ ψ (□ ∀ x (ϕ (x) ≡ ψ (x)) ⊃ (P (ϕ) ≡ P (ψ)))$ ,
(C2)
$∀ ϕ ¬ P (ϕ & ¬ ϕ)$ ,
(C3)
$G (x) = df ∀ ϕ (P (ϕ) ⊃ □ ϕ (x))$ , and
(C4)
$P (G)$ ,

we can derive, in second-order system KB,

(C5)
$□ ∃ x G (x) .$

Proof.³⁷ Assume, for proof by contradiction,

(6)
$¬ ∀ ϕ (P (ϕ) ⊃ ◇ ∃ x ϕ (x)) .$ [Assumption]

From (6), we have

(7)
$∃ ϕ ¬ (P (ϕ) ⊃ ◇ ∃ x ϕ (x)) .$ [(6)]

From (7), we have, by existential instantiation,

(8)
$¬ (P (ϕ ′) ⊃ ◇ ∃ x ϕ ′ (x)) .$ [(6)]

From (8), we have

(9)
$P (ϕ ′)$ [(6)]

and

(10)
$¬ ◇ ∃ x ϕ ′ (x) .$ [(6)]

From (10), we have, by the definition of possibility,

(11)
$□ ¬ ∃ x ϕ ′ (x) .$ [(6)]

From (11), we have, by necessitation and the K axiom,

(12)
$□ ∀ x ¬ ϕ ′ (x) .$ [(6)]

From (12), we have, by necessitation and the K axiom,

(13)
$□ ∀ x (ϕ ′ (x) ⊃ ϕ ′ & ¬ ϕ ′ (x)) .$ [(6)]

We have, by necessitation,

(14)
$□ ∀ x (ϕ ′ & ¬ ϕ ′ (x) ⊃ ϕ ′ (x)) .$ []

From (13) and (14), we have, by necessitation and the K axiom,

(15)
$□ ∀ x (ϕ ′ (x) ≡ ϕ ′ & ¬ ϕ ′ (x)) .$ [(6)]

From (C1) and (15), we have

(16)
$P (ϕ ′) ≡ P (ϕ ′ & ¬ ϕ ′) .$ [(C1), (6)]

From (C2) and (16), we have

(17)
$¬ P (ϕ ′) .$ [(C1), (C2), (6)]

From (9) and (17), we have

(18)
$P (ϕ ′) & ¬ P (ϕ ′) .$ [(C1), (C2), (6)]

Having derived a contradiction from (6), we can conclude, not depending on (6),

(19)
$∀ ϕ (P (ϕ) ⊃ ◇ ∃ x ϕ (x)) .$ [(C1), (C2)]

From (C4) and (19), we have

(20)
$◇ ∃ x G (x) .$ [(C1), (C2), (C4)]

Assume, for conditional proof,

(21)
$G (a) .$ [Assumption]

From (C3) and (21), we have

(22)
$∀ ϕ (P (ϕ) ⊃ □ ϕ (a)) .$ [(C3), (21)]

From (22), we have

(23)
$P (G) ⊃ □ G (a) .$ [(C3), (21)]

From (C4) and (23), we have

(24)
$□ G (a) .$ [(C3), (C4), (21)]

From (24), we have, not depending on (21),

(25)
$G (a) ⊃ □ G (a) .$ [(C3), (C4)]

From (25), we have

(26)
$∀ x (G (x) ⊃ □ G (x)) .$ [(C3), (C4)]

From (26), we have,

(27)
$∃ x G (x) ⊃ ∃ x □ G (x) .$ [(C3), (C4)]

Assume, for conditional proof,

(28)
$∃ x □ G (x) .$ [Assumption]

From (28), we have, by existential instantiation,

(29)
$□ G (a) .$ [(28)]

We have, by necessitation,

(30)
$□ (G (a) ⊃ ∃ x G (x)) .$ []

From (30), we have, by the K axiom,

(31)
$□ G (a) ⊃ □ ∃ x G (x) .$ []

From (29) and (31), we have

(32)
$□ ∃ x G (x) .$ [(28)]

From (32), we have, not depending on (28),

(33)
$∃ x □ G (x) ⊃ □ ∃ x G (x) .$ []

From (27) and (33), we have

(34)
$∃ x G (x) ⊃ □ ∃ x G (x) .$ [(C3), (C4)]

From (34), we have,

(35)
$¬ □ ∃ x G (x) ⊃ ¬ ∃ x G (x) .$ [(C3), (C4)]

From (35), we have, by necessitation,

(36)
$□ (¬ □ ∃ x G (x) ⊃ ¬ ∃ x G (x)) .$ [(C3), (C4)]

Assume, for proof by contradiction,

(37)
$¬ □ ∃ x G (x) .$ [Assumption]

From (35) and (37), we have

(38)
$¬ ∃ x G (x) .$ [(C3), (C4), (37)]

From (38), we have, by the B axiom,

(39)
$□ ◇ ¬ ∃ x G (x) .$ [(C3), (C4), (37)]

From (39), we have, by the definition of possibility,

(40)
$□ ¬ □ ¬ ¬ ∃ x G (x) .$ [(C3), (C4), (37)]

From (40), we have, by necessitation and the K axiom,

(41)
$□ ¬ □ ∃ x G (x) .$ [(C3), (C4), (37)]

From (36) and (41), we have, by the K axiom,

(42)
$□ ¬ ∃ x G (x) .$ [(C3), (C4), (37)]

From (20), we have, by the definition of possibility,

(43)
$¬ □ ¬ ∃ x G (x) .$ [(C1), (C2), (C4)]

From (42) and (43), we have

(44)
$□ ¬ ∃ x G (x) & ¬ □ ¬ ∃ x G (x) .$ [(C1), (C2), (C3), (C4), (37)]

Having derived a contradiction from (37), we can conclude, not depending on (37),

(C5)
$□ ∃ x G (x) .$ [(C1), (C2), (C3), (C4)]

□

B. Proof of Corollary 1

Corollary 1: Given axioms and definitions (C1), (C2), (C3), and (C4), we can derive, in second-order system KB,

(C6)
$∃ x G (x) .$

Proof. Assume, for proof by contradiction,

(45)
$¬ ∃ x G (x) .$ [Assumption]

From (45), we have, by the B axiom,

(46)
$□ ◇ ¬ ∃ x G (x) .$ [(45)]

From (46), we have, by the definition of possibility,

(47)
$□ ¬ □ ¬ ¬ ∃ x G (x) .$ [(45)]

From (47), we have, by necessitation and the K axiom,

(48)
$□ ¬ □ ∃ x G (x) .$ [(45)]

From (48), we have, by necessitation and the K axiom,

(49)
$□ (□ ∃ x G (x) ⊃ ¬ ∃ x G (x)) .$ [(45)]

From (C5), we have, by necessitation,

(50)
$□ □ ∃ x G (x) .$ [(C1), (C2), (C3), (C4)]

From (49) and (50), we have, by the K axiom,

(51)
$□ ¬ ∃ x G (x) .$ [(C1), (C2), (C3), (C4), (45)]

From (43) and (51), we have

(52)
$□ ¬ ∃ x G (x) & ¬ □ ¬ ∃ x G (x) .$ [(C1), (C2), (C3), (C4), (45)]

Having derived a contradiction from (45), we can conclude, not depending on (45),

(C6)
$∃ x G (x) .$ [(C1), (C2), (C3), (C4)]

□

C. Proof of Theorem 2

Theorem 2: Given axioms and definitions

(V1)
$∀ ϕ ∀ ψ (□ ∀ E x (ϕ (x) ≡ ψ (x)) ⊃ (P (ϕ) ≡ P (ψ)))$ ,
(V2)
$∀ ϕ ¬ P (ϕ & ¬ ϕ)$ ,
(V3)
$G (x) = df ∀ ϕ (P (ϕ) ⊃ □ ϕ (x))$ , and
(V4)
$P (G & E)$ ,

we can derive, in second-order system KB,

(V5)
$□ ∃ E x G (x) .$

Proof. Assume, for proof by contradiction,

(53)
$¬ ∀ ϕ (P (ϕ) ⊃ ◇ ∃ E x ϕ (x)) .$ [Assumption]

From (53), we have

(54)
$∃ ϕ ¬ (P (ϕ) ⊃ ◇ ∃ E x ϕ (x)) .$ [(53)]

From (54), we have, by existential instantiation,

(55)
$¬ (P (ϕ ′) ⊃ ◇ ∃ E x ϕ ′ (x)) .$ [(53)]

From (55), we have

(56)
$P (ϕ ′)$ [(53)]

and

(57)
$¬ ◇ ∃ E x ϕ ′ (x) .$ [(53)]

From (57), we have, by the definition of possibility,

(58)
$□ ¬ ∃ E x ϕ ′ (x) .$ [(53)]

From (58), we have, by necessitation and the K axiom,

(59)
$□ ∀ E x ¬ ϕ ′ (x) .$ [(53)]

From (59), we have, by necessitation and the K axiom,

(60)
$□ ∀ E x (ϕ ′ (x) ⊃ ϕ ′ & ¬ ϕ ′ (x)) .$ [(53)]

We have, by necessitation,

(61)
$□ ∀ E x (ϕ ′ & ¬ ϕ ′ (x) ⊃ ϕ ′ (x)) .$ []

From (60) and (61), we have, by necessitation and the K axiom,

(62)
$□ ∀ E x (ϕ ′ (x) ≡ ϕ ′ & ¬ ϕ ′ (x)) .$ [(53)]

From (V1) and (62), we have

(63)
$P (ϕ ′) ≡ P (ϕ ′ & ¬ ϕ ′) .$ [(V1), (53)]

From (V2) and (63), we have

(64)
$¬ P (ϕ ′) .$ [(V1), (V2), (53)]

From (56) and (64), we have

(65)
$P (ϕ ′) & ¬ P (ϕ ′) .$ [(V1), (V2), (53)]

Having derived a contradiction from (53), we can conclude, not depending on (53),

(66)
$∀ ϕ (P (ϕ) ⊃ ◇ ∃ E x ϕ (x)) .$ [(V1), (V2)]

From (V4) and (66), we have

(67)
$◇ ∃ E x G (x) .$ [(V1), (V2), (V4)]

Assume, for conditional proof,

(68)
$G (a) .$ [Assumption]

From (V3) and (68), we have

(69)
$∀ ϕ (P (ϕ) ⊃ □ ϕ (a)) .$ [(V3), (68)]

From (69), we have

(70)
$P (G & E) ⊃ □ (G & E) (a) .$ [(V3), (68)]

From (V4) and (70), we have

(71)
$□ (G & E) (a) .$ [(V3), (V4), (68)]

From (71), we have, not depending on (68),

(72)
$G (a) ⊃ □ (G & E) (a) .$ [(V3), (V4)]

From (72), we have

(73)
$∀ E x (G (x) ⊃ □ (G & E) (x)) .$ [(V3), (V4)]

From (73), we have

(74)
$∃ E x G (x) ⊃ ∃ E x □ (G & E) (x) .$ [(V3), (V4)]

Assume, for conditional proof,

(75)
$∃ E x □ (G & E) (x) .$ [Assumption]

From (75), we have, by existential instantiation,

(76)
$□ (G & E) (a) .$ [(75)]

We have, by necessitation,

(77)
$□ ((G & E) (a) ⊃ ∃ E x G (x)) .$ []

From (76) and (77), we have, by the K axiom,

(78)
$□ ∃ E x G (x) .$ [(75)]

From (78), we have, not depending on (75),

(79)
$∃ E x □ (G & E) (x) ⊃ □ ∃ E x G (x) .$ []

From (74) and (79), we have,

(80)
$∃ E x G (x) ⊃ □ ∃ E x G (x) .$ [(V3), (V4)]

From (80), we have

(81)
$¬ □ ∃ E x G (x) ⊃ ¬ ∃ E x G (x) .$ [(V3), (V4)]

From (81), we have, by necessitation,

(82)
$□ (¬ □ ∃ E x G (x) ⊃ ¬ ∃ E x G (x)) .$ [(V3), (V4)]

Assume, for proof by contradiction,

(83)
$¬ □ ∃ E x G (x) .$ [Assumption]

From (81) and (83), we have

(84)
$¬ ∃ E x G (x) .$ [(V3), (V4), (83)]

From (84), we have, by the B axiom,

(85)
$□ ◇ ¬ ∃ E x G (x) .$ [(V3), (V4), (83)]

From (85), we have, by the definition of possibility,

(86)
$□ ¬ □ ¬ ¬ ∃ E x G (x) .$ [(V3), (V4), (83)]

From (86), we have, by necessitation and the K axiom,

(87)
$□ ¬ □ ∃ E x G (x) .$ [(V3), (V4), (83)]

From (82) and (87), we have, by the K axiom,

(88)
$□ ¬ ∃ E x G (x) .$ [(V3), (V4), (83)]

From (67), we have, by the definition of possibility,

(89)
$¬ □ ¬ ∃ E x G (x) .$ [(V1), (V2), (V4)]

From (88) and (89), we have

(90)
$□ ¬ ∃ E x G (x) & ¬ □ ¬ ∃ E x G (x) .$ [(V1), (V2), (V3), (V4), (83)]

Having derived a contradiction from (83), we can conclude, not depending on (83),

(V5)
$□ ∃ E x G (x) .$ [(V1), (V2), (V3), (V4)]

□

D. Proof of Corollary 2

Corollary 2: Given axioms and definitions (V1), (V2), (V3), and (V4), we can derive, in second-order system KB,

(V6)
$∃ E x G (x) .$

Proof. Assume, for proof by contradiction,

(91)
$¬ ∃ E x G (x) .$ [Assumption]

From (91), we have, by the B axiom,

(92)
$□ ◇ ¬ ∃ E x G (x) .$ [(91)]

From (92), we have, by the definition of possibility,

(93)
$□ ¬ □ ¬ ¬ ∃ E x G (x) .$ [(91)]

From (93), we have, by necessitation and the K axiom,

(94)
$□ ¬ □ ∃ E x G (x) .$ [(91)]

From (94), we have, by necessitation and the K axiom,

(95)
$□ (□ ∃ E x G (x) ⊃ ¬ ∃ E x G (x)) .$ [(91)]

From (V5), we have, by necessitation,

(96)
$□ □ ∃ E x G (x) .$ [(V1), (V2), (V3), (V4)]

From (95) and (96), we have, by the K axiom,

(97)
$□ ¬ ∃ E x G (x) .$ [(V1), (V2), (V3), (V4), (91)]

From (89) and (97), we have

(98)
$□ ¬ ∃ E x G (x) & ¬ □ ¬ ∃ E x G (x) .$ [(V1), (V2), (V3), (V4), (91)]

Having derived a contradiction from (91), we can conclude, not depending on (91),

(V6)
$∃ E x G (x) .$ [(V1), (V2), (V3), (V4)]

□