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.

When Classical Logic is not Enough: Nonclassical Logics and Theological Reasoning

This is the eleventh 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.

Classical logic is extraordinarily powerful, so powerful in fact that one can easily begin to speak simply of 'logic' as though the classical system exhausted the possibilities of valid inference. The propositional calculus gives us familiar principles governing negation, conjunction, disjunction, and implication; first-order logic adds quantification and identity; model theory then permits us to specify satisfaction, consequence, validity, and interpretation with great precision. Much of the preceding series has depended upon precisely this framework, and nothing in what follows should be taken as withdrawing the confidence we have repeatedly placed in it.

Yet the development of logic in the twentieth century made clear that one need not abandon rigor in order to ask whether every feature of classical consequence is appropriate to every domain of reasoning. One can instead ask which principles are being used, what assumptions support them, and what changes when one of those assumptions is altered. This is the setting within which the various nonclassical logics emerged, not as one unified rebellion against classical logic, but as a family of formally disciplined attempts to revise particular features of consequence for particular purposes.

The plurality is important. Intuitionistic logic alters what may count as sufficient warrant for assertion and consequently declines to validate some classical principles. Relevant logics require a stronger connection between antecedent and consequent than material implication ordinarily supplies. Paraconsistent logics deny that contradiction must entail everything whatsoever, while many-valued logics permit semantic values other than the classical pair of truth and falsity. These systems do not all solve the same problem, and theology gains nothing by treating them as though they were variations upon one general theme called 'nonclassical logic'.

The more fruitful question is why theology might care about any of them.

Intuitionistic Logic: What Warrants the Assertion?

Classical logic validates the law of excluded middle:

P ∨ ¬P.

Either P or not-P.

It also validates double-negation elimination:

¬¬P → P.

If it is not the case that P is false, then P.

For classical reasoning these principles are familiar enough that one may hardly notice when they are being used. Intuitionistic logic, arising from Brouwer's philosophy of mathematics and subsequently formalized especially by Heyting, does not accept them unrestrictedly, not because the intuitionist is somehow more tolerant of contradiction, but because the standards governing assertion have changed. Under the constructive interpretation, asserting P requires an appropriate construction or proof of P, while asserting P ∨ Q requires having grounds for one disjunct or the other; consequently, the impossibility of ¬P need not itself amount to a constructive establishment of P.

The theological temptation here is obvious, and it should be resisted. It would be careless to claim that theological propositions are intuitionistic simply because faith is not mathematical proof, or to suppose that intuitionistic logic somehow captures religious trust better than classical logic. The connection is much more modest, but also more interesting, because intuitionistic logic forces us to ask a question theological argument often leaves implicit: What exactly warrants the assertion being made?

Consider the difference between

¬¬P

and

P.

Classical logic permits the passage from the former to the latter, whereas intuitionistic logic does not generally permit that inference. The distinction is useful because it forces us to ask whether showing that the denial of a proposition is untenable amounts to positively establishing the proposition itself. A theologian may successfully argue that a particular denial of divine action produces contradiction, but it remains a further question whether this alone establishes the particular positive account of divine action that the theologian wishes to defend.

One need not become an intuitionist in order to profit from the distinction. The formal system is valuable here because it makes visible an inferential step that ordinary theological prose can conceal, namely, the transition from the failure of a denial to the warrant for an affirmation.

Relevant Logic: What Has the Premise to Do with the Conclusion?

Classical material implication produces results that can initially seem peculiar. Since

P → Q

is classically equivalent to

¬P ∨ Q,

the conditional is true whenever P is false or Q is true, and consequently classical logic validates forms such as

P → (Q → P)

and

¬P → (P → Q).

These are often called paradoxes of material implication, though they are not contradictions within classical logic; they follow directly from the truth-functional definition of the conditional.

Relevant logicians ask whether a genuine relation of implication should require more than this. If we say that one proposition follows from another, should there not be some appropriate connection between the content of premise and conclusion? Relevant logics attempt to build such a requirement into the consequence relation itself, so that implication is not secured merely by the falsity of an antecedent or the independent truth of a consequent.

For theology the question is hardly peripheral, because theological discourse is saturated with conditionals. We say:

If Christ is risen, then …

If God creates ex nihilo, then …

If justification is by faith, then …

If God is immutable, then …

In such cases the theological force of the conditional ordinarily depends upon some intelligible relation between what is asserted in the antecedent and what is claimed in the consequent. We do not usually mean merely that the conditional happens to receive the value true under the truth table for material implication.

This is not yet an argument for replacing classical implication. It may instead be an argument for recognizing that many theological uses of 'if … then …' express more than the material conditional was ever intended to capture. The important point is therefore methodological: before formalizing a theological conditional, one must determine what sort of inferential relation the natural-language formulation is attempting to express.

Relevant logic helps precisely because it refuses to allow us to ignore that question.

Paraconsistent Logic: What Follows from Contradiction?

Perhaps no family of nonclassical logics is more immediately attractive to theologians, and perhaps none is more easily abused, than paraconsistent logic. Classical logic validates the principle commonly called explosion:

P, ¬P ⊢ Q.

From a contradiction, anything follows.

The principle does not mean that Q bears some hidden relation to P. Rather, once both P and ¬P have been admitted into a classical theory, every sentence becomes derivable, and the theory consequently loses its ability to discriminate among conclusions. In that technical sense, contradiction produces triviality.

Paraconsistent logics reject explosion. In a paraconsistent consequence relation, it is not generally the case that

P, ¬P ⊨ Q

for arbitrary Q, and therefore inconsistent information can be reasoned from without permitting every proposition to follow. What must be emphasized, however, is that paraconsistency does not by itself entail that contradictions are true; it entails only that contradiction need not produce inferential collapse.

This distinction is especially important in theology, where doctrines are often said loosely to be 'paradoxical' or even 'contradictory'. Christ is divine and human; God is one and three; the believer is righteous and sinful; God acts while creatures genuinely act. Yet none of these formulations has the form

P ∧ ¬P

unless one has first identified 'human' with 'not divine', 'three' with 'not one', or otherwise made the predicates contradictory in the same respect and under the same description.

Indeed, much of the history of Christian doctrine can be read as sustained resistance to exactly such conflations. Chalcedonian Christology does not say that Christ is finite and not finite in the same respect; Trinitarian doctrine distinguishes essence from person; the Lutheran formula simul iustus et peccator does not require that righteousness and sin be predicated univocally in the same respect. The logical discipline here lies not in invoking paraconsistency too quickly, but in determining first whether a genuine contradiction exists.

Paraconsistent logic becomes genuinely interesting when we confront a theological corpus, a historical tradition, or a developing theory that actually contains inconsistent commitments. Must everything then follow? A paraconsistent framework says no, and that can be useful when analyzing historically layered materials, competing doctrinal formulations, or theories under revision, because one can study the consequences of inconsistency without first pretending that the inconsistency is absent and without allowing the system to become trivial.

It is therefore essential to distinguish paraconsistency from dialetheism. The former concerns the behavior of consequence in the presence of contradiction; the latter is the metaphysical thesis that some contradictions are in fact true. One may use paraconsistent logic as a formal tool without thereby committing oneself to the reality of true contradictions, and theology should preserve that distinction with some care.

Many-Valued Logic: Must Every Proposition Be Simply True or False?

Classical propositional logic operates with two truth values, true and false. Many-valued logics generalize this architecture by permitting additional semantic values, though the significance of those additional values varies considerably from system to system. Some contain three values, others finitely many, and still others infinitely many; moreover, the extra values need not always be understood as degrees of truth, since they may instead represent indeterminacy, lack of information, semantic defect, or some other feature of the evaluation.

The theological temptation must again be controlled. The existence of many-valued logics does not establish that theological truth itself comes in degrees, nor does it show that mystery or doctrinal controversy requires intermediate truth values. What these logics do show is that bivalence is a semantic choice that can be examined rather than silently presupposed in every domain.

Suppose, for example, that we consider a predicate such as

x is mature in faith.

At what precise point does this predicate become true? If there is no sharp boundary, the issue may concern vagueness rather than either contradiction or theological confusion. Similar difficulties arise with predicates such as 'orthodox', 'responsible', 'culpable', 'spiritually mature', and even, in some contexts, 'alive' and 'dead', where biological or conceptual boundaries may be difficult to draw sharply.

A many-valued semantics offers one family of ways of representing such cases. It is not the only family, since supervaluationism, epistemicism, contextualism, and other theories compete with it, but the formal possibility is philosophically useful because it prevents us from assuming without argument that every semantically difficult case must still admit a sharp classical assignment of exactly one of two values.

The lesson for theology is therefore not that truth is fuzzy. It is that the semantics appropriate to a theological predicate must be investigated rather than assumed.

Which Logic for Theology?

At this point one might ask which logic theology should use, but the question is too coarse if it is understood as demanding one system for every theological task. There is no reason to suppose that theology needs a single nonclassical logic to replace classical logic across the board, and there is every reason to retain classical first-order logic for the enormous range of theological reasoning for which its proof theory, semantics, and inferential behavior are entirely adequate.

The existence of nonclassical logics does not overthrow classical logic. What it does overthrow is the assumption that every feature of classical consequence lies beyond philosophical examination. Intuitionistic logic asks what licenses assertion; relevant logic asks what connection implication should require between premise and conclusion; paraconsistent logic asks whether inconsistency must entail triviality; many-valued logic asks whether every semantic domain is adequately represented by exactly two truth values.

What has happened, accordingly, is not an abandonment of logic but a deepening of the philosophy of logic, because logical consequence itself has become an object of investigation. Earlier in this series we asked what follows from a theory, what structures satisfy it, whether the intended structure can be characterized, whether truth can be defined within the relevant language, whether consequences can be mechanically decided, and whether possible-world semantics supplies a sufficiently fine-grained account of content. Nonclassical logic now asks a question prior to many of those questions: Which relation of consequence are we employing when we say that one proposition follows from another?

The answer cannot simply be read off from the theological subject matter. The doctrine of the Trinity does not announce that its proper formal reconstruction must be classical, relevant, paraconsistent, or intuitionistic, nor does the Incarnation tell us in advance what sort of logical system best represents the relations among its propositions. One must first determine what the doctrine actually asserts, whether its apparent tensions are genuine contradictions or merely differences of respect, what kinds of conditionals occur within the argument, and what semantic distinctions the doctrine itself requires.

Only after that work has been done does the choice of formal machinery become philosophically responsible.

There is a danger in both directions. One can force every theological claim into classical form and conclude that whatever does not fit must be confused, or one can invoke a nonclassical logic whenever a doctrine appears difficult and thereby protect a defective formulation from criticism by simply changing the consequence relation. Neither procedure is satisfactory, because in both cases logic is being selected before the theological and semantic work has been done.

The choice of logic should instead follow from an analysis of the inferential phenomena one is attempting to represent. If the problem is vagueness, paraconsistency may be beside the point; if the problem is inconsistent information, many-valuedness may not address it; if the issue concerns the relation between antecedent and consequent, intuitionistic logic does not automatically solve it. Different logics revise different structures, and therefore there is no generic escape hatch labeled 'nonclassical'.

Why It Matters for Theology

Nonclassical logic matters for theology because it reveals that our conception of consequence already contains philosophical commitments. Classical logic gives powerful and often entirely appropriate accounts of theological reasoning, but its principles are better understood when we know what alternatives would look like and which features of inference those alternatives modify.

The discipline imposed by nonclassical logic is therefore double. We must specify exactly which classical principle appears inadequate for the task before us, and we must also identify what is gained and what is lost when that principle is revised. Merely changing the logic does not settle the theological question, since every alteration in consequence brings with it new semantic and proof-theoretic commitments of its own.

For theology this discipline can be salutary, because it forces distinctions that theological rhetoric too easily obscures. Apparent contradiction must be distinguished from genuine contradiction; material implication from explanatory or relevant connection; lack of proof from falsity; vagueness from inconsistency; mystery from contradiction; and formal tolerance of inconsistency from the metaphysical claim that some contradiction is actually true.

These are not logical niceties added after the theological work is complete. They belong to the conditions under which theology can say clearly what it means to say.

The most important lesson, therefore, is not that theology needs another logic, but that theology should know what its logic is doing, what it permits, what it forbids, and why. Once that much has been learned, the existence of alternative logics becomes less threatening and more useful, because each can be treated not as a rival worldview but as an instrument for testing the assumptions built into a particular account of consequence.

This brings us naturally to the final installment of the series. We began with Frege, Peirce, and Cantor, where modern logic dramatically enlarged the resources available for formal expression; we moved through model theory, completeness, incompleteness, compactness, truth, computability, modality, second-order logic, and hyperintensionality; and we have now reached the point at which consequence itself can be formally varied.

It is therefore fitting to return at the end to Gödel. His ontological argument brings together much of the machinery accumulated along the way: quantified modal logic, higher-order resources, necessity, possibility, formal derivation, and the distinction between the validity of an argument and the truth or adequacy of the axioms from which it proceeds. The final question will not be whether logic can 'prove God', but something more precise and, I think, more interesting: what exactly has been established when a theological argument has been successfully formalized and proved valid?

Bibliographical Note

The modern study of intuitionistic logic grows from L. E. J. Brouwer's philosophy of mathematics and Arend Heyting's subsequent formalization of intuitionistic reasoning. Alan Ross Anderson and Nuel Belnap's work on entailment became foundational for relevance logic. Stanisław Jaśkowski and Newton da Costa were among the major pioneers of paraconsistent logic, while subsequent work by Graham Priest and others developed its philosophical implications. Jan Łukasiewicz's work on three-valued logic, initially associated especially with future contingents, helped initiate the systematic study of many-valued logics. These traditions should not be treated as a single alternative to classical logic, since each revises different features of classical consequence for different formal and philosophical purposes.

Beyond Possible Worlds: Hyperintensionality and the Grain of Theological Content

This is the tenth 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.

Kripke semantics gave modal logic an extraordinary conceptual advance. Once necessity and possibility could be interpreted relative to possible worlds and an accessibility relation, claims that had seemed resistant to rigorous semantic treatment became formally manageable. To say that φ is necessary at a world w is to say that φ is true at every world accessible from w; to say that φ is possible is to say that φ is true at at least one accessible world. With this apparatus, philosophers could distinguish actuality from necessity, possibility from actuality, and different systems of modal reasoning by imposing different conditions upon accessibility.

But a successful semantics can disclose its own limitations precisely by being successful. Possible-world semantics distinguishes propositions that differ in their modal profiles. What happens, however, when two propositions have exactly the same modal profile but nevertheless appear to differ in meaning, explanatory role, subject matter, or metaphysical ground? This is the problem of hyperintensionality.

To see the issue, we should first distinguish three levels. An extensional context is sensitive to extension—in the case of sentences, principally to truth value. An intensional context can distinguish expressions that have the same actual extension but differ across possible worlds. A hyperintensional context is finer-grained still: it may distinguish expressions even when they are necessarily equivalent, and therefore have the same truth value at every possible world. That is the central idea behind contemporary talk of hyperintensionality.

Suppose, for example, that φ and ψ are necessarily equivalent:

□(φ ↔ ψ).

On a coarse-grained possible-world account in which propositions are identified with the sets of worlds at which they are true, φ and ψ determine the same proposition. They are true at precisely the same worlds, and nothing in their possible-world extensions distinguishes them.

Now consider two necessary truths:

2 + 2 = 4.

and

If God is triune, then God is triune.

Assuming standard arithmetic and classical logic, both are true at every possible world under consideration. If propositions are simply sets of possible worlds, both consequently correspond to the same set: the set of all possible worlds. Yet one proposition concerns arithmetic, while the other concerns the logical consequence of a theological predication. Whatever account we finally give of propositional content, it seems difficult to maintain that they say the same thing merely because no possible world distinguishes their truth values. This is a standard pressure against identifying propositional content simply with sets of possible worlds: distinct necessary truths collapse into the same coarse-grained intension.

The corresponding problem arises for necessary falsehoods. If two propositions are impossible, each is true at no possible world. On the same coarse-grained account, both correspond to the empty set, even though they may express entirely different impossibilities. Possible worlds tell us where propositions are true; they do not always tell us finely enough what those propositions say.

The theological significance of this becomes apparent almost immediately.

Suppose a theologian maintains that God is triune is necessarily true. Suppose also that 7 + 5 = 12 is necessarily true.

The propositions then agree in modal profile: each is true at every possible world. But no theologian wishes to infer that the doctrine of the Trinity and an elementary proposition of arithmetic possess the same theological content. The former says something about God; the latter does not. Modal equivalence, even necessary equivalence, is therefore too coarse to capture every distinction theology needs to make.

The point becomes still clearer when we consider explanation. Assume that φ and ψ are necessarily equivalent. It does not follow that

φ because ψ

and

ψ because φ

are interchangeable. Explanation has direction. The existence of Socrates may explain the existence of Socrates' singleton, for example, even though, necessarily, Socrates exists if and only if the singleton of Socrates exists. Reversing the explanation does not thereby become equally satisfactory. Contemporary discussions of grounding therefore routinely treat grounding and explanation as hyperintensional: substitution of necessarily equivalent claims can change the truth or adequacy of a grounding or explanatory statement. Theology is filled with precisely such explanatory asymmetries.

Consider the difference between saying that something is true because God is what God is and saying merely that the proposition is necessarily true. If

□φ,

we know that φ holds throughout the relevant space of possible worlds. But from this alone we have learned nothing about why φ is true, whether φ belongs to the essence of something, or what metaphysically grounds φ.

Necessity and essence therefore come apart. An influential line of contemporary metaphysics, associated especially with Kit Fine, argues that although essential truths are necessary, not every necessary truth about an object states something belonging to its essence. One may have necessary connections to countless objects or mathematical truths that contribute nothing to what one is. The modern literature on grounding makes the same point: essence and metaphysical explanation seem to require distinctions finer than modal covariance across possible worlds.

That matters greatly for classical theology. When the theologian says that omnipotence, goodness, or triunity belongs to God essentially, the claim is not obviously exhausted by saying that God possesses the relevant property in every possible world in which God exists. The theologian is saying something about what God is, not merely plotting the distribution of a predicate across modal space.

Compare:

Necessarily, if God exists, then 2 + 2 = 4.

with:

Necessarily, if God exists, then God is God.

Both may be necessary. Yet the second appears connected to divine identity in a way the first plainly is not. Possible-world necessity by itself does not mark that difference.

Hyperintensionality therefore raises a question more fundamental than whether modal logic is adequate. The question is whether modal profile supplies a sufficiently fine grain of content for all the philosophical work theology asks propositions to perform. In many cases it does not.

Belief provides another familiar example. A person may believe φ without believing ψ even when φ and ψ are necessarily equivalent. Someone may believe a complicated mathematical theorem without recognizing an equivalent formulation of that theorem, or believe one description of an individual without believing another necessarily co-referring description. If belief were modeled entirely by the set of possible worlds compatible with what the believer believes, problems of logical omniscience quickly arise: the believer threatens to become committed to every logical consequence of everything believed. Hyperintensional approaches seek a semantic grain fine enough to distinguish contents that possible-world semantics treats alike.

The theological analogue is obvious. A fourth-century theologian might affirm everything needed for a doctrinal conclusion without possessing our later conceptual formulation of that conclusion. Two creedal formulations might agree extensionally, or even necessarily, while differing significantly in what they make explicit, what conceptual distinctions they employ, and what theological errors they exclude. If theological propositions are identified solely by their truth across possible worlds, some of these differences risk disappearing.

This is not merely a problem about wording. The distinction between homoousios and a formulation that happens to have the same truth conditions may matter precisely because doctrinal language intends to say something determinate about the relation of Father and Son. Likewise, two theories of justification might generate the same verdicts about every imagined case while differing concerning what grounds justification, what role faith plays, or what relation obtains between promise and reception. Agreement in extension—even necessary agreement—does not by itself establish sameness of theological account. How, then, should hyperintensionality be modeled?

There is no single accepted answer. Some approaches treat propositions as structured entities rather than merely sets of worlds, so that the internal semantic organization of a proposition contributes to its identity. Others employ impossible worlds: points of evaluation at which logical, mathematical, or metaphysical impossibilities may obtain. Two necessary truths that agree at every possible world can then differ because they behave differently at impossible worlds. Still other approaches use finer-grained notions of facts, states of affairs, subject matter, proof, grounds, or structured meaning.

Impossible-world semantics is particularly instructive. If φ and ψ are both necessary, no possible world distinguishes them. But an impossible world might be one at which φ holds while ψ does not. Extending the semantic space beyond the possible thereby gives us a way of separating contents that standard possible-world semantics collapses. This does not require believing that impossible worlds concretely exist somewhere; like possible worlds in formal semantics, they may be treated as representational devices within a semantic theory. Contemporary hyperintensional semantics employs precisely such strategies.

But once again, greater expressive discrimination brings philosophical costs. How fine-grained should propositions become? If every syntactically distinct sentence expresses a different proposition, we distinguish too much. If all necessary equivalents express the same proposition, we distinguish too little. Between these extremes lies the hard question of which differences matter for meaning, explanation, essence, grounding, belief, and subject matter.

The problem is therefore not merely to make semantic content finer-grained. It is to make it finer-grained in the right way.

This brings us back to a theme running through the entire series. Frege gave us quantification; model theory taught us how theories are interpreted in structures; Löwenheim–Skolem and Compactness exposed limits upon how tightly first-order theories control their models; Tarski distinguished truth from the semantic machinery by which truth is defined; Kripke showed how necessity and possibility can be treated through possible worlds; second-order logic showed that additional expressive power can be purchased, but only at a price.

Hyperintensionality now reveals another boundary. Even when we know the truth value of a proposition at every possible world, we may still not know enough about its content.

That is a remarkable result for philosophical theology, because theology is concerned not merely with which sentences come out true but with what is being said, what makes it true, how one truth explains another, what belongs to the essence of God or creature, and which conceptual distinctions are doctrinally significant. A semantics that records only distributions of truth across possible worlds may therefore be indispensable for modal reasoning while remaining insufficient for these further tasks.

Why It Matters for Theology

Hyperintensionality matters for theology because theological truth is not exhausted by modal extension. Two claims can agree at every possible world and nevertheless differ in subject matter, meaning, explanatory direction, essential content, or metaphysical ground.

This is particularly important when theology speaks of divine essence, Trinitarian relations, incarnation, justification, sacramental presence, or divine action. In such cases theologians ordinarily care not merely that certain propositions are necessarily connected but how they are connected and what accounts for the connection. To say that φ necessarily accompanies ψ is weaker than saying that ψ grounds φ, that φ belongs to the essence of some object, that ψ explains φ, or that φ and ψ express the same content.

Possible-world semantics therefore remains enormously valuable without being semantically exhaustive. Kripke taught us how to represent modal profile. Hyperintensional theories remind us that modal profile is not always identity of content.

For philosophical theology, the lesson is again one of discrimination rather than skepticism. The question is not whether formal semantics fails, but which semantic distinctions a particular formalism is capable of representing. Once theology begins asking not merely what could or must be true, but what a doctrine means, what grounds it, what explains it, and what belongs essentially to its subject matter, it has entered territory in which possible worlds alone may no longer be enough.

Bibliographical Note

The contemporary literature on hyperintensionality grows from problems concerning belief, meaning, logical omniscience, essence, grounding, and explanation. Kit Fine's work on essence was especially important in challenging the reduction of essence to necessity, while subsequent work on grounding and metaphysical explanation has reinforced the need for distinctions among necessarily equivalent contents. Mark Jago's The Impossible: An Essay on Hyperintensionality (Oxford University Press, 2014) and Francesco Berto and Mark Jago's Impossible Worlds (Oxford University Press, 2019) develop impossible-world approaches to hyperintensional semantics. Contemporary surveys treat structured propositions, impossible worlds, grounding, essence, content, and related approaches as different attempts to explain how semantic and metaphysical distinctions can be finer-grained than possible-world intensions.

Second-Order Logic: The Promise and Price of Saying More

This is the ninth 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.

First-order logic achieved something remarkable. It gave modern mathematics and philosophy a formal language expressive enough to represent enormously complicated structures while retaining a collection of equally remarkable metatheoretical properties. Gödel proved it complete. Compactness tells us that if every finite subset of a first-order theory has a model, the whole theory has a model. The Löwenheim–Skolem theorems tell us that theories with infinite models ordinarily have models of different infinite sizes. Church and Turing showed that validity is not decidable, but valid first-order sentences can nevertheless be effectively enumerated through formal proof.

By this point in our series, however, we have also discovered the price paid for these virtues. First-order theories frequently fail to determine uniquely the structures about which we intended to speak. The Löwenheim–Skolem theorem guarantees that a first-order theory with an infinite model cannot, under the usual conditions, uniquely characterize an infinite structure up to isomorphism. If our theory has the intended natural numbers as a model, it will also have nonstandard models. If we hoped that sufficiently careful first-order axiomatization would force interpretation back onto the one structure we originally intended, model theory tells us otherwise.

One response is to strengthen the language.

In first-order logic our quantifiers range over individuals:

∀x Px.

We read this:

Every individual is P.

Second-order logic allows us also to quantify over properties and relations themselves. Thus we may write

∀X φ,

where X is not an individual variable but a predicate variable. Under the standard, or full, semantics for second-order logic, a one-place predicate variable ranges over all subsets of the domain, a two-place relation variable ranges over all sets of ordered pairs from the domain, and similarly for relations of higher arity. The apparently small move from quantifying only over objects to quantifying also over properties and relations produces a dramatic increase in expressive power.

The natural numbers provide the classic example.

First-order arithmetic can express induction only by means of an axiom schema. For every formula φx of the appropriate kind, there is a corresponding induction axiom. What first-order logic cannot say in a single sentence is that induction holds for every property whatsoever of natural numbers, because the variables of first-order logic do not range over properties.

Second-order logic can say exactly this:

∀X[(X0 ∧ ∀x(Xx → Xx⁺)) → ∀xXx].

The formula says:

For every property X, if 0 has X and whenever a number has X its successor also has X, then every natural number has X.

Under full second-order semantics, X ranges over every subset of the domain. The second-order Peano axioms consequently characterize the natural-number structure up to isomorphism. Unlike first-order Peano arithmetic, they have no nonstandard models when interpreted under full semantics. Similar resources permit second-order characterizations of other important mathematical structures, including the real numbers as a complete ordered field.

Here, then, is the promise of second-order logic. It can sometimes say what first-order logic cannot say, and because it can say more, it can sometimes constrain its models far more tightly.

This point deserves emphasis because it returns us to the problem raised by Löwenheim–Skolem. Suppose our concern is not merely to construct some structure satisfying a theory, but to characterize the intended structure uniquely up to isomorphism. First-order logic may frustrate that aspiration for principled reasons. Second-order logic can sometimes accomplish precisely what first-order logic cannot.

But the gain is not free.

The very features that give full second-order logic its greater expressive power cost us several of the great metatheorems that made first-order logic so attractive. There is no effective sound and complete proof calculus for full second-order validity. Compactness fails. The ordinary Löwenheim–Skolem results fail as well. Indeed, these failures are closely related to second-order logic's capacity to characterize structures such as the natural numbers and the real numbers categorically.

This is not an accidental defect in a formalism awaiting technical repair. If full second-order arithmetic categorically characterizes the natural numbers, it cannot at the same time possess the first-order combination of expressive limitations, compactness, and Löwenheim–Skolem behavior that generated nonstandard models in the first place. We have gained one thing partly because we have surrendered another.

The trade becomes clearer if we return to Gödel's completeness theorem. For first-order logic,

T ⊨ φ if and only if T ⊢ φ.

Every semantic consequence of T is captured by formal derivation. No corresponding effective proof system captures all validities of second-order logic under full semantics. In fact, the validities of full second-order logic are not recursively enumerable. There can therefore be no mechanical procedure which simply generates all and only the valid second-order formulas by means of a complete formal calculus.

At precisely this point Leon Henkin discovered something illuminating. If we weaken the semantics so that second-order variables do not range over all subsets and relations on the domain, but only over a specified collection of them, a completeness theorem can be recovered. These are now called Henkin or general models. Under Henkin semantics, second-order logic behaves in important respects like many-sorted first-order logic and regains familiar completeness and model-theoretic properties.

But once again the gain has a price. The categorical power associated with full second-order semantics is no longer generally available.

The resulting choice is philosophically fascinating. If we demand that the second-order quantifiers really range over all subsets and relations of the appropriate kind, we obtain the expressive strength responsible for categoricity, but lose an effective complete proof system and other first-order metatheoretical properties. If instead we restrict the ranges of those quantifiers sufficiently to recover a Henkin-style completeness theorem, much of the distinctive model-theoretic strength that attracted us to second-order logic disappears.

This raises an even deeper question: Where did the additional expressive power come from?

Under full semantics, when we say that X ranges over every property of objects in a domain D, the usual set-theoretical semantics understands this as quantification over the entire power set of D. But if the semantic apparatus must already determine what all the subsets of D are, then a great deal has been placed into the metalanguage before the object language begins its work. The categoricity achieved by full second-order logic therefore depends upon a very strong semantic interpretation of its quantifiers.

This is why some philosophers have questioned whether full second-order logic should be regarded simply as “logic” in the same sense as first-order logic. Others have argued that the additional expressive power is precisely what makes second-order logic indispensable. The dispute need not be settled here. What matters for our purposes is that stronger formal expressiveness may transfer some of the burden from axioms inside the formal theory to semantic assumptions governing the range of the quantifiers.

For theology, that observation should sound familiar.

Theologians regularly speak in ways that appear to quantify not merely over individuals but over properties and relations. Claims about identity offer a simple example. A Leibnizian principle can be represented as

∀x∀y[(∀X(Xx ↔ Xy)) → x = y].

This says:

For any objects x and y, if x and y have exactly the same properties, then x is identical with y.

Whatever one finally thinks about the metaphysics of properties or the adequacy of the principle, the logical point is clear. “Every property” is not ordinary first-order quantification. If the phrase is meant literally, we have crossed into second-order territory.

Such territory appears quickly in philosophical theology. Discussions of divine attributes, personal identity, Christology, the Trinity, essence, necessity, and the relation between nature and properties can require us to speak not merely about objects but about what may truly be predicated of objects. Second-order resources can therefore make explicit distinctions that a purely first-order language either cannot make or can reproduce only indirectly.

There is another theological attraction, however, that may be even more important. Throughout this series we have repeatedly distinguished a formal theory from its intended interpretation. Theology ordinarily does not mean to say merely that there is some model in which its sentences come out true. When it speaks about God, creation, incarnation, justification, or resurrection, it intends its assertions to concern a determinate reality.

This can make categoricity look enormously attractive.

Suppose a theological theory T admits a large family of non-isomorphic models. We might ask whether this plurality reflects genuine theological alternatives, harmless differences in representation, or simply the expressive weakness of the language in which T has been stated. Second-order resources may sometimes allow us to constrain the intended structure more sharply than first-order resources permit.

But nothing follows merely from the fact that we have moved to second-order logic. Second-order logic does not magically identify the intended theological structure. Nor does increased expressive power guarantee theological truth. We must still determine whether the predicates have been interpreted properly, whether the axioms say what the doctrine intends, and whether the semantic resources introduced by the formalism correspond to anything we are prepared to accept metaphysically.

Indeed, second-order logic sharpens rather than eliminates the problem of interpretation. With first-order logic, we worried that the axioms did not control their models tightly enough. With full second-order logic, we must additionally ask what licenses our claim to quantify over all the relevant properties and relations.

This yields an important lesson for model-theoretic theology. There are at least two ways in which a formal theory can fail to capture what we intend. Its language may be too weak to characterize the intended structure, or its semantics may achieve the desired characterization only because the intended structure has effectively been built into the semantic apparatus. The first danger is underdetermination; the second is concealed determination from the metalanguage.

Neither is solved by formalism alone.

Second-order logic therefore places philosophical theology before a genuine methodological choice. Sometimes the expressive poverty of first-order logic is a virtue. Its weakness makes possible completeness, compactness, and powerful general model theory. At other times that same weakness prevents us from saying what we actually want to say, particularly when we want to quantify over properties, characterize structures categorically, or distinguish intended from unintended interpretations more sharply.

The proper question is therefore not whether second-order logic is better than first-order logic. The question is what theological work we need the logic to do and what semantic price we are prepared to pay for allowing it to do that work.

Why It Matters for Theology

Second-order logic teaches theology that expressive power and formal tractability do not necessarily increase together. A stronger language can distinguish more, characterize more, and sometimes eliminate unintended models, while at the same time surrendering completeness, compactness, effective axiomatizability, and other properties available to first-order logic under its standard semantics.

That tradeoff matters whenever theology attempts formal reconstruction. If we restrict ourselves to first-order resources, we must accept limits upon what our theories can characterize. If we invoke full second-order resources, we must be explicit about the semantics that gives those resources their power and about the assumptions entering through the metalanguage.

The deepest lesson may therefore concern something we have encountered repeatedly throughout this series. Formal precision does not remove philosophical decisions; it makes their location clearer. Sometimes the decisive commitment lies in an axiom. Sometimes it lies in a rule of inference. Sometimes it lies in the structure selected as a model. And sometimes, as second-order logic shows with unusual clarity, it lies in what we have allowed our quantifiers to range over before the argument has even begun.

Theology should want that clarity.

Bibliographical Note

Leon Henkin's “Completeness in the Theory of Types,” Journal of Symbolic Logic 15 (1950): 81–91, established the completeness result associated with what are now called Henkin or general semantics. Stewart Shapiro's Foundations without Foundationalism: A Case for Second-Order Logic (Oxford University Press, 1991) provides an influential philosophical defense of second-order logic. Jouko Väänänen's work on second-order and higher-order logic gives a particularly useful account of full and general semantics, categoricity, and the failures of first-order compactness and Löwenheim–Skolem properties when full second-order semantics is adopted.

Kripke: Possible Worlds, Necessity, and the Semantics of Modal Logic

This is the eighth 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.

For much of the first half of the twentieth century, modal logic occupied an uncertain position. Philosophers and logicians had long wanted to reason formally about necessity and possibility, but the semantic status of modal expressions remained obscure. What does it mean to say that something is necessarily true rather than merely true? What makes a proposition possible rather than actual? And how are we to understand the inferential behavior of expressions such as “it is necessary that” and “it is possible that” without treating them merely as unexplained operators added to ordinary logic?

The difficulty was real because modal contexts do not behave extensionally in the straightforward way familiar from classical first-order logic. If two names designate the same object, substitution of one for the other ordinarily preserves truth in extensional contexts. Yet in modal or other intensional contexts, substitution may fail. One may know that Cicero is Cicero without knowing that Cicero is Tully, although Cicero and Tully designate the same man. The logical problem was therefore not merely how to invent symbols for necessity and possibility, but how to give those symbols a semantics capable of explaining their inferential structure.

Saul Kripke's work around 1959 and 1960 supplied the decisive breakthrough. Building upon earlier developments by Rudolf Carnap, Stig Kanger, Jaakko Hintikka, and others, Kripke gave modal logic a relational semantics in which modal operators are interpreted through what are commonly called possible worlds.

Let us suppose that we have a collection of worlds and a relation of accessibility among them. We write

wRv

to mean:

world v is accessible from world w.

The accessibility relation does not ordinarily mean that one world physically travels to another, nor need possible worlds be understood as concrete universes. Within the semantics, they function first of all as points of evaluation. The relation R specifies which worlds are relevant when the modal status of a proposition is evaluated at a given world.

We can then define necessity and possibility.

□φ

is read:

It is necessary that φ.

And

◇φ

is read:

It is possible that φ.

The crucial semantic clauses are these:

w ⊨ □φ

if and only if

for every v such that wRv, v ⊨ φ.

In words: φ is necessary at world w exactly when φ is true at every world accessible from w.

Likewise,

w ⊨ ◇φ

if and only if

there is some v such that wRv and v ⊨ φ.

In words: φ is possible at world w exactly when φ is true at at least one world accessible from w.

What had previously looked like an elusive intensional distinction now received a mathematically precise semantic treatment. Necessity becomes truth throughout an appropriate range of accessible worlds; possibility becomes truth at at least one such world.

The importance of the accessibility relation appears when we notice that different modal logics correspond to different structural properties of R. If every world is accessible from itself, then R is reflexive. If accessibility is symmetric, then whenever wRv, we also have vRw. If it is transitive, then whenever wRv and vRu, we have wRu.

These apparently technical properties correspond to familiar modal principles.

For example, the system T validates

□φ → φ.

The principle says that whatever is necessary is true. Semantically, this follows when accessibility is reflexive, since if every world is accessible from itself, then anything true at all worlds accessible from w must be true at w itself.

The system S4 adds, among other things, the principle

□φ → □□φ.

If something is necessary, then it is necessarily necessary. This corresponds naturally to transitivity of accessibility.

S5 validates still stronger principles, including

◇φ → □◇φ.

If something is possible, then it is necessarily possible. In standard Kripke semantics, S5 may be modeled by treating accessibility as an equivalence relation, or more simply in many presentations by allowing every relevant world to be accessible from every other.

The achievement here was not merely that several modal calculi could now be given models. Kripke semantics showed why different systems validate different modal principles. Instead of treating modal axioms as isolated formal stipulations, one could correlate them with structural features of frames.

A Kripke frame consists of a set W of worlds together with an accessibility relation R:

F = ⟨W, R⟩.

A Kripke model adds a valuation V telling us where atomic propositions are true:

M = ⟨W, R, V⟩.

The semantics therefore mirrors a pattern already familiar from first-order model theory. A formal language receives interpretation relative to a structure, and truth is defined recursively relative to that structure. Kripke's innovation was to extend this model-theoretic strategy to modal discourse.

This has enormous consequences for philosophical theology because so much theological reasoning is modal whether or not theologians explicitly acknowledge it. Theology repeatedly distinguishes what God does from what God could have done, what creatures happen to be from what they must be, what follows necessarily from the divine nature from what results contingently from divine willing, and what is possible given certain theological commitments from what is impossible.

Consider a simple theological sentence:

□(God is God).

Whatever else may be said about the example, the modal operator tells us that the assertion is not merely that the proposition happens to be true. It is represented as true at every relevant accessible world.

Or consider:

◇(God creates no world).

This would express the claim that there is at least one accessible world in which God does not create. Whether the claim is theologically acceptable is a further question, but the semantics makes clear what kind of claim it is.

The value of the apparatus lies precisely in separating formal structure from theological judgment. Kripke semantics does not tell us which propositions are necessary, which worlds are genuinely possible, or which accessibility relation theology ought to adopt. Rather, it gives us a disciplined framework within which those further questions can be stated with precision.

This point matters because “possible world” language can easily become metaphysically inflated. One sometimes speaks as though Kripke semantics had established the existence of a vast plurality of concrete worlds. It did no such thing. The semantics requires mathematical structures containing points of evaluation and an accessibility relation. What metaphysical interpretation, if any, should be given to those points is a further philosophical issue.

That distinction is especially important in theology, where possible-world language is often used in discussions of divine necessity, freedom, providence, incarnation, atonement, and the problem of evil. One may employ Kripke semantics to regiment modal relations without committing oneself to David Lewis's later modal realism, according to which possible worlds are concrete realities. The formal semantics and the ontology of possible worlds are distinct questions.

There is another important lesson here. Modal claims are not merely ordinary claims with decorative prefixes. If

φ

is true, it does not follow that

□φ

is true.

Likewise, if

◇φ

is true, we cannot infer

φ.

The operators alter the conditions under which a proposition is evaluated. Much theological confusion arises precisely when claims of actuality, possibility, and necessity are allowed to slide into one another without argument.

Suppose, for example, one argues:

God creates the world.

Therefore,

God necessarily creates the world.

Nothing in ordinary logic licenses this inference. To move from actuality to necessity requires an additional modal premise.

Or suppose one reasons:

It is possible that God creates a world containing rational creatures.

Therefore,

God creates such a world.

Again, the inference fails. Possibility does not entail actuality.

These distinctions are elementary once formalized, but they become extremely important when theological arguments move among divine attributes, divine actions, and creaturely possibilities. Modal logic permits one to see precisely where the transition occurs and to ask what principle licenses it.

Kripke's work also transformed the treatment of quantified modal logic. Once individuals, quantifiers, and modal operators are combined, further questions arise. Does the domain of objects remain fixed across worlds, or may different worlds contain different objects? If an object exists in more than one world, how is it identified across worlds? Can an object possess some properties essentially and others accidentally?

These questions helped lead directly into Kripke's later work on naming, necessity, and essential properties. If a name such as “Aristotle” rigidly designates the same individual in every possible world in which that individual exists, then modal claims about Aristotle differ importantly from claims expressed merely through descriptions such as “the teacher of Alexander.” The distinction between rigid designation and descriptive reference would become one of the major developments in late twentieth-century philosophy.

For theology, the implications are immediate. Claims about God, Christ, divine attributes, personal identity, incarnation, and resurrection often depend upon questions of transworld identity and essential predication. To say that Christ could have acted otherwise is not merely to describe another individual satisfying a similar description. It is to make a modal claim about the same individual.

Kripke's semantics therefore gives philosophical theology something more valuable than an additional notation. It provides a framework for distinguishing necessity from actuality, possibility from consistency, essential from accidental predication, and semantic evaluation from metaphysical interpretation.

The framework also fits naturally with the larger trajectory of the results considered in this series. Tarski taught us to distinguish object language from metalanguage and truth from satisfaction. Church and Turing showed that formal specification does not guarantee universal mechanical decidability. Kripke now demonstrates that even intensional notions such as necessity and possibility can be treated with considerable formal rigor once their semantics is properly specified.

The lesson is not that metaphysics has been reduced to set theory. Rather, the logical structure of modal discourse can be made explicit without pretending that the formalism itself settles every metaphysical question.

Why It Matters for Theology

Kripke semantics matters for theology because theological reasoning is saturated with modal distinctions. God is said to exist necessarily, creation is usually said to be contingent, certain divine attributes are treated as essential, creaturely states as possible or impossible, and doctrines are often tested by asking whether a specified set of claims can be jointly true. Modal logic enables these claims to be distinguished rather than merely asserted.

It also teaches an important methodological discipline. A formal modal model tells us what follows once we have fixed a set of worlds, an accessibility relation, and a valuation. It does not itself tell us what counts as a genuinely possible world for theology, whether divine possibilities should be modeled by S4 or S5, whether domains should vary across worlds, or whether possible worlds should be given any robust metaphysical status. Those are theological and philosophical questions that arise after the semantics has done its work.

Kripke's achievement was therefore not to settle the metaphysics of possibility, but to provide a semantics within which modal reasoning could finally be treated with the same kind of rigor that model theory had already brought to extensional logic. For philosophical theology, that was a decisive gain.

Bibliographical Note

Saul A. Kripke's early modal-semantic work appeared in “A Completeness Theorem in Modal Logic,” Journal of Symbolic Logic 24 (1959): 1–14, and “Semantical Considerations on Modal Logic,” Acta Philosophica Fennica 16 (1963): 83–94. His later lectures, published as Naming and Necessity, developed the influential notions of rigid designation, necessary a posteriori truths, and essential properties. For theological applications, the most important background lies in the semantics of modal systems T, S4, and S5, quantified modal logic, rigid designation, and the distinction between formal possible-world semantics and substantive metaphysical theories of possible worlds.