Gödel’s Ontological Argument: What Formal Proof Can—and Cannot—Establish

This is the twelfth and final part of a series developed through the Department of Philosophical Theology at the Institute of Lutheran Theology’s Christ School of Theology, exploring major results and developments in modern logic and their significance for philosophical and systematic theology.

It is fitting to end this series by returning to Gödel. We encountered him earlier because the completeness theorem showed an extraordinary correspondence between syntactic derivability and semantic consequence in first-order logic, while the incompleteness theorems exposed principled limits upon sufficiently strong formal theories. We return to him now in a rather different role, for Gödel also worked for many years upon a formal reconstruction of the ontological argument, bringing together higher-order quantification, modal logic, properties, essences, and necessary existence in an attempt to show that the existence of a Godlike being follows from a small set of explicitly stated axioms.

The argument is sometimes reported under the breathless heading that Gödel “proved that God exists,” which is almost exactly the wrong way to understand its philosophical importance. What Gödel produced was a formal argument within a specified logical framework; consequently, the interesting question is not whether the symbols somehow compel belief in God, but what has been established once the derivation is valid. To answer that question requires distinctions we have accumulated throughout this series: between syntax and semantics, proof and truth, axioms and interpretations, necessity and actuality, object language and metalanguage, and finally between a formally successful model and the reality that the model is intended to represent.

There is also a historical complication worth keeping in view. What is usually called 'Gödel’s ontological proof' is now better regarded as a family of closely related arguments. Gödel left a compact manuscript dated 1970; Dana Scott, after discussing the argument with Gödel, produced a slightly modified formulation that became especially influential, while C. Anthony Anderson, Melvin Fitting, and others later proposed further emendations. Recent formal work has made the distinctions among these versions increasingly precise.

Positive Properties and a Godlike Being

The argument begins not with existence but with properties. Let

PF

mean:

F is a positive property.

Gödel did not reduce positivity to some more elementary formal notion. 'Positive' functions as a primitive predicate upon properties, and axioms specify how positive properties behave. This point is crucial, because the proof does not manufacture substantive content from logic alone; it begins with substantive assumptions governing a class of properties and then investigates what follows from those assumptions.

Using a Scott-style presentation, one central principle says, roughly, that a property and its negation cannot both be positive and that one of them must fall on the positive side. Another principle says that if a positive property necessarily entails another property, the entailed property is also positive. We may represent the latter as

[PF ∧ □∀x(Fx → Hx)] → PH.

The reading is straightforward: if F is positive, and necessarily everything possessing F possesses H, then H is positive as well.

Gödel then defines a Godlike individual as one possessing every positive property:

Gx ↔ ∀F(PF → Fx).

Thus:

x is Godlike if and only if x possesses every positive property.

Notice what has happened. 'Godlike' has not been introduced as an unanalyzed name for the Christian God, nor has divine existence been inserted explicitly into the definition. The predicate G is constructed from the prior notion of positivity, and the burden of the argument consequently begins shifting toward the axioms governing positive properties.

One of the most important axioms then says that being Godlike is itself positive:

PG.

Together with the principles governing positive properties, one can prove that every positive property is possibly exemplified. Since being Godlike is positive, it follows that

◇∃xGx.

That is:

Possibly, there exists a Godlike being.

The move deserves attention because modal ontological arguments are often caricatured as simply assuming that God possibly exists and then exploiting S5 to obtain necessary existence. In the Gödel-Scott construction, the possibility claim appears as a theorem derived from more fundamental assumptions about positivity. Whether those assumptions are plausible is another question, but formally the distinction matters. In the familiar Scott presentation, positive properties are shown to be possibly exemplified, and Godlikeness is stipulated to be positive; hence the possible exemplification of Godlikeness follows.

Essence and Necessary Existence

Possibility alone does not give Gödel what he wants, however, and the next steps introduce the concepts of essence and necessary existence. Let

F Ess x

mean:

F is an essence of x.

In the Scott-style formulation, this can be represented schematically as

F Ess x ↔ Fx ∧ ∀H[Hx → □∀y(Fy → Hy)].

Thus F is an essence of x when x actually possesses F and F necessarily entails every property H that x possesses. The definition is extremely strong. An essence does not merely belong importantly or characteristically to an individual; it necessarily carries with it every property possessed by that individual under the conditions specified by the formalism. Scott's addition of the requirement Fx—the requirement that x actually exemplify the alleged essence—turns out to be technically significant, since recent formal analysis shows that a strict rendering of Gödel's own 1970 definition without this condition produces inconsistency, whereas the Scott modification avoids that particular problem.

Necessary existence is then defined through essences:

NEx ↔ ∀F(F Ess x → □∃yFy).

In words:

x exists necessarily if and only if every essence of x is necessarily exemplified.

Gödel then adds another crucial axiom:

PNE.

Necessary existence is a positive property.

Since a Godlike being possesses every positive property, any Godlike being possesses necessary existence. Moreover, the argument establishes that Godlikeness itself is an essence of anything Godlike. Once these pieces are assembled, the conclusion follows:

□∃xGx.

Necessarily, there exists a Godlike being.

This is a genuine formal result. The familiar Scott variant has been formally checked using contemporary higher-order theorem provers and proof assistants, and the derivation of the necessary existence conclusion from the stipulated axioms and definitions can be verified mechanically. Indeed, the computer-assisted work is philosophically interesting precisely because it removes much uncertainty about whether some unnoticed inferential gap lies hidden inside the argument.

But now the philosophical work begins rather than ends.

What Exactly Has Been Proved?

Three questions must be distinguished. First, does the conclusion follow from the axioms and definitions in the specified logic? Second, are those axioms themselves true or otherwise rationally warranted? Third, do 'positive property', 'Godlike', 'essence', and 'necessary existence' adequately represent the theological and metaphysical concepts to which we intend them to refer?

The first question is formal. The latter two are not settled merely by answering the first.

Suppose T is the theory consisting of the relevant axioms and definitions, while φ is the claim that necessarily a Godlike being exists. We may establish

T ⊢ φ.

Given the proof system, φ is derivable from T. If the semantics is appropriate and the formal system sound, we may correspondingly have

T ⊨ φ.

Every model satisfying T satisfies φ.

Neither statement, however, contains the further premise that T is true of reality. That claim must come from somewhere else. A valid derivation tells us what follows if the axioms hold; it does not transform the axioms into metaphysical truths merely because their consequences have been derived without error.

This is especially important because 'positive property' remains primitive. The axioms tell us how positivity behaves: positive properties must satisfy certain closure conditions, Godlikeness is positive, necessary existence is positive, and so forth. But the formal system does not independently establish that the relevant theological understanding of perfection, goodness, or divine reality corresponds to precisely this class of formally positive properties.

We can now see why merely announcing that the proof has been computer-verified misses the point. A proof assistant can establish that the conclusion follows from the formalized premises, and model finders can test consistency or produce countermodels to candidate claims. They cannot, merely by executing those procedures, determine whether 'positive' has captured what a theologian means by divine perfection or whether Gödel's definition of 'essence' captures what belongs to the essence of God. Modern automated work on the argument has been valuable precisely because it separates these questions instead of collapsing them.

The Problem of Modal Collapse

The most striking illustration is the phenomenon known as modal collapse. In the Gödel-Scott family of formulations under discussion, the axioms are strong enough to derive

φ → □φ.

Whatever is true is necessarily true.

If this principle holds generally, then the distinction between contingent and necessary truth collapses. What actually happens could not have been otherwise, at least within the modal structure represented by the theory. Automated analysis has confirmed that modal collapse follows in the familiar Scott-style formulation and in closely related corrected forms of Gödel's argument.

For theology this is hardly an insignificant consequence. Classical Christian theology ordinarily distinguishes the necessity of God's being from the contingency of creation. God does not create because God lacks the ability not to create, and the created order is not ordinarily regarded as following from the divine essence with the same necessity with which God is God. If every actuality is necessary, the formal system threatens precisely this distinction between Creator and creature, necessity and freedom, which means that the theologian has good reason to inspect the assumptions producing the collapse.

Yet the right response is not to say that modal collapse proves Gödel's argument invalid. If the collapse is derivable from the axioms, then it is one of their consequences, and a formally valid proof cannot be refuted by disliking another theorem of the same system. Rather, modal collapse gives us evidence relevant to the independent assessment of the axioms: if those axioms entail a consequence we have strong theological or metaphysical reason to reject, then we have reason to reconsider the axioms, their definitions, or the logical framework within which they operate.

Later variants make this point particularly clear. Anderson and Fitting alter Gödelian assumptions in ways that preserve versions of the necessary-existence argument while avoiding modal collapse. The existence of such variants shows that the collapse is not simply an unavoidable consequence of any modal ontological argument; it depends upon how the relevant notions have been formalized and which axioms govern them.

When Formalization Discovers Something

Here the argument becomes a fitting conclusion to our series, because formalization is doing more than decorating an old philosophical argument with symbols. By making definitions and inferential commitments explicit, it can reveal consequences that ordinary prose leaves hidden. Modal collapse is one example; the recently identified difficulty with the unmodified 1970 definition of essence is another. What looked informally close enough can turn out formally to matter greatly.

This is one of the genuine promises of formal methods for theology. A formal reconstruction may show that a conclusion does not follow unless some additional premise is introduced, that two formulations previously regarded as equivalent actually behave differently, that an apparently harmless definition generates an unwanted theorem, or that weakening an axiom preserves the desired result while avoiding an objection. In such cases logic is not replacing theological judgment but giving theological judgment a more exact object upon which to work.

The same point applies to models. If there is a model of T in which some candidate theological conclusion fails, then the conclusion does not follow merely from T. If every model of T satisfies the conclusion, we have established semantic consequence. If T possesses models with structures substantially different from the one theology intended, the Löwenheim–Skolem considerations encountered earlier in this series return. If the intended structure can be isolated only by moving to stronger higher-order resources, the costs examined in our discussion of second-order logic arise. If necessarily equivalent formulations nevertheless differ in theological content, the problem of hyperintensionality returns as well.

Gödel's little argument thus sits at the intersection of nearly everything we have been discussing.

Why It Matters for Theology

The great theological lesson of Gödel's ontological argument is therefore neither that formal logic has proved God nor that formal logic is incapable of speaking meaningfully about God. Both conclusions are too easy. The argument shows instead what becomes possible when theological and metaphysical commitments are made explicit enough to enter a rigorous formal system.

Once the axioms have been stated, logic can be relentless. It can determine consequences that the original author may not have noticed, expose hidden dependence upon modal principles, distinguish definitions that initially appeared equivalent, and even allow computers to verify derivations whose details would otherwise be extraordinarily difficult to survey. What logic cannot do merely by being logic is certify that the primitive predicates have been interpreted correctly or that the axioms from which the derivation begins are true of God.

This distinction is not a weakness of formalization. It is the condition under which formalization becomes intellectually useful.

The theologian therefore ought neither fear formal logic nor ask it to do work it cannot do. When a formal argument establishes

T ⊢ φ,

the achievement can be considerable. We now know that φ follows from T according to the stated rules. The next questions concern T itself: what its terms mean, what its axioms assert, what models satisfy it, whether those models correspond to the intended subject matter, and whether we have independent reason to believe that the world—or God—is as the theory represents.

Those questions cannot be evaded by pointing again to the proof.

The Series in Retrospect

We began this series with Frege, Peirce, and Cantor because modern logic enormously expanded what could be formally expressed. Russell and the development of axiomatic methods showed why disciplined formal construction was necessary; Gödel showed both the extraordinary reach and the principled limitations of proof; Löwenheim–Skolem and Compactness taught us that theories may have structures we never intended; Tarski taught us to distinguish truth from satisfaction and object language from metalanguage; Church and Turing placed limits upon mechanical decision; Kripke gave necessity and possibility a model-theoretic semantics; second-order logic showed how additional expressive strength can be purchased at metatheoretical cost; hyperintensionality showed that even complete modal agreement may fail to capture sameness of content; and nonclassical logics taught us that the relation of consequence itself may become an object of philosophical investigation.

Gödel's ontological argument draws these threads together because it forces us to ask, all at once, what language we are using, over what its variables range, which modal semantics we have chosen, which properties our higher-order quantifiers admit, what our definitions mean, which axioms are assumed, what follows from them, and whether the formal structures thereby generated correspond to the theological reality about which we intend to speak.

After twelve installments, that may be the most important lesson modern logic can offer theology. Formalization does not abolish interpretation, metaphysics, or theological judgment; neither does it leave them where it found them. It disciplines them by forcing us to locate exactly where our commitments enter and exactly what those commitments entail.

Logic does not relieve theology of the obligation to speak truthfully about its subject matter. It makes it considerably harder for theology to conceal from itself what it has actually said.

Bibliographical Note

Gödel's ontological argument appears in the posthumously published third volume of his Collected Works, with an introduction by Robert Merrihew Adams. Dana Scott's closely related formulation became one of the principal versions discussed in the subsequent literature. C. Anthony Anderson's “Some Emendations of Gödel's Ontological Proof,” Faith and Philosophy 7 (1990): 291–303, develops an influential revision, while Melvin Fitting's Types, Tableaus, and Gödel's God (Kluwer, 2002) provides an extensive logical treatment. Christoph Benzmüller and Bruno Woltzenlogel Paleo inaugurated detailed computer-supported verification of the argument using contemporary higher-order theorem provers and proof assistants, while later work by Benzmüller, David Fuenmayor, Annika Kanckos, Scott, and others has clarified the relations among different Gödelian variants, modal collapse, positivity, and the exact logical strength required by the argument. Recent work with Scott also distinguishes more sharply Gödel's 1970 manuscript from Scott's modified version and shows the importance of the precise definition of essence.

Church and Turing: Computability, Decision, and the Limits of Mechanical Reasoning

This is the seventh part of a series developed through the Department of Philosophical Theology at the Institute of Lutheran Theology’s Christ School of Theology, exploring major results in modern logic and their significance for philosophical and systematic theology.

Once logic had become sufficiently exact to distinguish formal derivation from semantic consequence, and once Gödel had shown both the completeness of first-order logic and the incompleteness of sufficiently strong formal theories, another question became unavoidable: Which logical and mathematical problems can, in principle, be solved by a completely mechanical procedure? The question was not merely whether human beings happen to know an efficient method, nor whether some proof might be extremely difficult to discover. It concerned something considerably more fundamental. Is there, for a given class of problems, an effective procedure which, if followed correctly and for a finite number of steps, will always yield the right answer?

During the 1930s Alonzo Church and Alan Turing, working independently and by strikingly different routes, gave mathematically precise accounts of what such an effective procedure would amount to. Church employed the lambda calculus and the notion of recursive functions; Turing imagined what are now called Turing machines, highly idealized devices capable of manipulating symbols according to finitely specified rules. Although the formalisms differed, they identified the same class of functions. This convergence was sufficiently remarkable that the resulting conception came to be expressed in the Church–Turing thesis: everything that can be calculated by an effective mechanical procedure is computable by a Turing machine, or equivalently by one of the other standard formal models of computation.

The thesis is important partly because it is not itself a theorem in the ordinary sense. The informal notion of an effective procedure is not independently given as a mathematically defined object against which one can simply prove that Turing computability is extensionally equivalent. Rather, the thesis proposes that the mathematically exact notion captures the pretheoretical notion of mechanical calculability. Its strength arises from the convergence of many independently developed formal characterizations—Turing machines, recursive functions, lambda definability, register machines, and others—which all identify the same class of computable functions.

This matters because, once effective calculability had been formalized, one could ask with precision whether important logical problems were decidable. A decision procedure for a class of statements is an effective method which, for any statement in the class, eventually terminates and answers correctly either yes or no. Thus, if there were a decision procedure for first-order validity, one could feed any first-order sentence φ into the procedure and eventually receive the correct verdict:

φ is logically valid,

or

φ is not logically valid.

At first this hope did not appear unreasonable. After all, Gödel had proved first-order logic complete. If

⊨ φ,

then

⊢ φ.

Every logically valid first-order sentence therefore has a formal proof. One might consequently suppose that validity is mechanically decidable: enumerate possible proofs until a proof of φ is found. But this establishes only half of what a decision procedure would require. If φ is valid, proof search will eventually succeed; if φ is not valid, however, a blind search for a proof need never terminate. We would then have no general means of knowing whether the sentence lacked a proof or whether its proof simply had not yet appeared.

This distinction is the difference between being recursively enumerable and being decidable. A proof system may provide a method that eventually recognizes all the positive cases without providing a method that always settles both positive and negative cases. First-order validity has precisely this character. Valid sentences can be effectively enumerated because formal proofs can be mechanically checked and systematically generated. What Church and Turing showed, however, is that there is no algorithm that decides, for every first-order sentence, whether that sentence is logically valid.

This result answers negatively the famous Entscheidungsproblem associated with Hilbert and Ackermann. The hope had been for a general mechanical procedure by which questions of logical validity could be settled. Church and Turing showed that no such procedure exists for full first-order logic. The limitation here is therefore not one imposed by insufficient ingenuity, inadequate computing power, or the practical difficulty of extremely large calculations. There can be no algorithm of the stipulated kind at all.

Turing's route to this conclusion is especially instructive because it turns upon the possibility of machines representing the behavior of other machines. A Turing machine is an idealized computing device consisting, in its simplest description, of a potentially unbounded tape divided into cells, a read-write head, and a finite set of instructions determining what the machine does according to the symbol it encounters and its current state. Despite the austerity of this arrangement, Turing showed that machines of this type can represent any effectively calculable procedure.

More remarkably, he showed that there can be a universal machine capable of simulating any other Turing machine when given an appropriate description of that machine and its input. Once machines and their inputs can themselves be represented symbolically, however, questions about computation can be transformed into questions about the behavior of encoded machines. This makes possible one of the central results in the theory of computation: the undecidability of the halting problem.

Suppose we ask whether there is a machine H which, when given the description of any machine M together with an input w, always correctly determines whether M eventually halts when run on w. Symbolically, we may represent the hoped-for procedure as follows:

H(M, w) = YES

if M halts on w,

and

H(M, w) = NO

if M does not halt on w.

Turing showed that no such general machine can exist. The proof proceeds by constructing, from the hypothetical halting-decider H, another machine whose behavior becomes contradictory when it is given its own description as input. The exact construction matters, but the deeper lesson is already visible: once sufficiently rich systems can encode descriptions of their own operations, diagonal forms of self-reference again appear, much as they had in Gödel's incompleteness argument and in the semantic paradoxes that motivated Tarski.

The family resemblance among these results should not obscure their differences. Gödel's first incompleteness theorem says that sufficiently strong, consistent, effectively axiomatized formal systems contain statements that cannot be proved within those systems. Tarski's undefinability result establishes limitations upon defining truth for sufficiently expressive languages within those same languages. Church and Turing establish limitations upon algorithmic decision. These are distinct theorems with distinct conclusions, even though each reveals, from a different direction, that formalization does not culminate in a universal procedure by which every relevant question can mechanically be settled.

That distinction is particularly important in theology, where the phrase “limits of reason” can become so elastic that nearly any formal result is made to support nearly any desired theological conclusion. Church and Turing do not show that human reason is intrinsically incapable of knowing God, that faith begins where logic fails, that mystery lies beyond computation, or that theological truth transcends all formal representation. None of those claims follows from the mathematics. What the results establish is much more exact: there are rigorously specified classes of formal problems for which no general algorithmic decision procedure exists.

This precision is itself theologically useful, because theology has often been tempted both to overestimate and to underestimate what formal reasoning can do. On the one hand, one may imagine that if theological propositions are stated with sufficient logical precision, doctrinal questions could eventually become matters of mechanical derivation. On the other hand, one may react against formalization by claiming that theology, because it concerns divine mystery, lies fundamentally beyond logical treatment. The Church–Turing results support neither conclusion. They tell us instead that formal procedures have determinate powers and determinate limitations, which should be investigated rather than rhetorically exaggerated.

Suppose, for example, that a theological theory T is formalized in some sufficiently expressive language and that we ask whether a sentence φ follows from T. If the language is first-order, then by completeness,

T ⊨ φ if and only if T ⊢ φ.

This tells us something profound: semantic consequence and formal derivability coincide. But it does not follow that there is a single algorithm which, for every T and every φ, will always terminate and decide whether T ⊨ φ. Completeness guarantees the existence of proofs for consequences; undecidability denies a universal terminating decision method for every case. The difference is easy to overlook but essential to an adequate philosophy of logic.

The theological significance becomes clearer if we distinguish deduction from decision. A deductive system provides rules by which conclusions may be derived from premises. A decision procedure provides an effective method which determines, for every candidate case, whether the relevant relation holds. Theology can therefore profit enormously from formal deduction without supposing that all questions internal to a sufficiently expressive theological system will thereby become algorithmically decidable.

Consider a simple doctrinal reconstruction. Suppose T contains axioms concerning divine attributes, creaturely dependence, incarnation, or sacramental presence. The formal system may permit us to derive consequences not immediately obvious in the ordinary-language formulations. It may expose hidden inconsistency, clarify the scope of quantifiers, distinguish competing interpretations, or show that certain propositions follow only when additional assumptions are introduced. None of this requires the theological theory to possess a complete mechanical decision procedure.

Indeed, the absence of such a procedure may help us understand why formal reasoning and conceptual judgment remain distinct. Algorithms operate on formally specified structures according to explicit rules. But the construction of the formal representation itself—deciding what counts as a primitive term, which distinctions are semantically important, how a doctrine is to be interpreted, and whether a formal consequence corresponds to the intended theological claim—already requires judgments that are not supplied by the algorithm simply because the algorithm is formally impeccable.

Here again the preceding results in this series converge. Löwenheim–Skolem taught us that a theory may possess many nonisomorphic models. Compactness showed that local satisfiability does not necessarily secure the global structure one had intended. Tarski distinguished truth, satisfaction, object language, and metalanguage. Church and Turing now show that even where the syntax and semantics have been specified with extraordinary exactness, one cannot assume that every resulting question falls under a universal mechanical method of decision.

There is, consequently, a modest but important lesson for theological method. Formalization can sharpen theological reasoning without converting theology into computation. The theologian who uses formal logic responsibly should therefore ask not merely whether an argument has been symbolized, but what class of formal problem has been produced, what can be mechanically determined within that class, what can only be semi-decided or recursively enumerated, and what interpretive judgments preceded the formalization in the first place.

The result is neither a triumphalist rationalism nor an invocation of mystery against reason. It is a more discriminating account of reason itself. Church and Turing teach us that a mechanical procedure is a precisely characterizable thing and that, once characterized, its limitations can themselves be proved. Logic therefore acquires one of its most striking forms of self-knowledge: it can determine not merely what follows from what, but something about what no general calculating procedure can decide.

Why It Matters for Theology

Church and Turing leave philosophical theology with several durable lessons. First, formal derivability must be distinguished from algorithmic decidability. A system may have precise proof rules even though no general procedure can decide every relevant consequence question. Second, the absence of a decision procedure is not an invitation to irrationalism; it is itself a formally demonstrable limitation within a precisely defined domain. Third, theological formalization remains useful even when it does not yield mechanical settlement of every question, since formal systems can still clarify consequence relations, reveal inconsistency, distinguish interpretations, and expose hidden assumptions.

Finally, these results remind theology that formal methods do not eliminate judgment. Before any algorithm can operate, a language must be chosen, symbols interpreted, axioms selected, and the intended relation between the formal structure and theological reality specified. Computation begins only after much of the most important conceptual work has already been done.

The deeper lesson, then, is not that reason fails, but that reason comes to understand the forms of its own effectiveness. Church and Turing showed that there are questions which no universal mechanical procedure can decide, and in doing so they transformed the meaning of logical limitation. The limitation is not a retreat from rigor. It is one of rigor's greatest achievements.

Bibliographical Note

Alonzo Church's 1936 paper “An Unsolvable Problem of Elementary Number Theory” gave one of the first precise demonstrations that certain effectively posed problems are undecidable. Alan Turing's “On Computable Numbers, with an Application to the Entscheidungsproblem,” published in 1936–1937, introduced the machine model now bearing his name and established the undecidability of central computational problems. For the historical background, Hilbert and Ackermann's formulation of the Entscheidungsproblem remains important, while modern introductions to computability theory ordinarily treat Turing machines, recursive functions, the Church–Turing thesis, the halting problem, and the undecidability of first-order validity together.