Modal Logic: Necessity, Time, Knowledge, and Provability

First-order model theory studies how formulas are interpreted in structures. Modal logic adds another question: how does the truth of a statement at one situation depend on its truth at other situations?

The situations might represent possible alternatives, later moments, states compatible with an agent's information, or stages in a mathematical interpretation. Their relationship matters as much as the truth values assigned within them.

This development overlaps chronologically with the foundational work in the preceding notes. It belongs here because the distinction between a language, a model, and a class of models now lets us explain what changed.

Lewis and the problem of implication

In classical propositional logic, the material conditional $A\to B$ is false exactly when $A$ is true and $B$ is false. Consequently, a false antecedent makes the conditional true, and a true consequent makes it true regardless of its antecedent.

This definition is useful for expressing truth-functional constraints. It does not by itself express every ordinary claim that one statement follows necessarily from another.

C. I. Lewis investigated this difference in work culminating in A Survey of Symbolic Logic in 1918 and, with C. H. Langford, Symbolic Logic in 1932. The resulting systems treated strict implication. In familiar modern notation, strict implication can be expressed as

Here $\Box$ means necessity. The formula says that the conditional holds throughout the relevant alternatives.

This must be distinguished from $A\to\Box B$. If a meeting happens to be on Tuesday, it can still be necessary that, if it is on Tuesday, it occurs on a weekday. The necessity concerns the relationship, not the particular scheduling decision.

Strict implication also retains limitations as an analysis of relevance: an impossible antecedent strictly implies every proposition in standard normal modal settings. That difficulty helped motivate a separate tradition discussed in the next note.

From calculi to relational semantics

The semantic history has several contributors. Carnap developed interpretations involving state descriptions. Jónsson and Tarski investigated Boolean algebras with operators. Kanger, Hintikka, and Kripke developed influential approaches to modal interpretation, with Kripke's work around 1959–1963 especially important for systematic relational semantics.

These were related contributions rather than a single invention made all at once. The historical survey in the Stanford account of modal logic provides a useful guide to their different roles.

A propositional modal frame consists of a nonempty set $W$ and a relation $R$ on that set. A model also specifies which propositional letters are true at each member of $W$.

The central clause is

Possibility, written $\Diamond A$, holds when at least one accessible situation satisfies $A$. In classical modal logic it is equivalent to $\neg\Box\neg A$.

The word “world” does not commit the mathematician to a particular metaphysics. A frame is a mathematical object. Its intended interpretation must be supplied separately.

A two-world example

Let the worlds be $w$ and $v$, with $wRv$ and no other accessibility pairs. Suppose $p$ is false at $w$ and true at $v$.

Then $\Box p$ is true at $w$: its only accessible world makes $p$ true. Nevertheless, $p$ is false at $w$. Thus

is not valid on arbitrary frames.

Now require every world to access itself. Whenever $\Box p$ holds at a world, $p$ must hold there too. Reflexivity validates this axiom, usually called T.

Similarly, transitivity validates

If every world accessible from an accessible world is already accessible from the starting world, necessity propagates through two steps.

These examples explain why there are different modal logics. K uses the normal modal rules without additional frame restrictions. T, S4, and S5 impose further principles, conventionally associated with reflexive, reflexive-transitive, and equivalence-relation frames respectively.

Choosing a system means choosing mathematical commitments about the intended relationship. It is not a ranking from an inferior logic to a universally correct one.

The next lab makes the frame and valuation independently editable. It extends the two-world example to three worlds so that a missing transitive edge can also be inspected.

What normality assumes

Normal modal logic includes the distribution principle

It also has necessitation: if $A$ is a theorem, then $\Box A$ is a theorem.

The qualification “theorem” is essential. From a contingent assumption $A$ one cannot simply infer $\Box A$. Otherwise every assumed fact would become necessary.

The distribution principle follows from the relational truth clause: at every accessible world, both $A\to B$ and $A$ entail $B$. This semantic explanation also identifies what must be reconsidered when constructing a non-normal modal system.

Quantification changes the problem

Ruth Barcan Marcus's 1946 work introduced a systematic quantified modal calculus. Once variables and quantifiers enter the language, a model must specify which objects are available at each world.

The Barcan formula is commonly written

Its converse reverses the implication. Whether these principles hold depends on the semantic treatment of domains and existence.

Consider an outer domain containing $a$ and $b$. Let the local domain at $w$ be $\{a\}$ and at its accessible world $v$ be $\{a,b\}$. Suppose $P(a)$ is true at $v$ but $P(b)$ is false there.

At $w$, every locally available object necessarily has $P$, because the only such object is $a$. Yet it is not necessary that every locally available object has $P$: at $v$, the new object $b$ fails the condition.

Under this expanding-domain interpretation, the displayed Barcan formula fails. The example makes the issue concrete: quantification at the starting world need not cover all objects quantified over at an accessible world. Constant-domain models remove this particular difference.

Marcus's contribution also belongs to debates about identity, naming, and essential properties. Those philosophical disputes should not be collapsed into a claim that one domain convention is compulsory for every application.

Time, information, and obligation

Arthur Prior developed tense logic in the 1950s and 1960s, giving formal expression to past and future. A future operator can quantify over moments later than the present. Whether the present is included determines whether its version of $\Box A\to A$ should hold.

Jaakko Hintikka's Knowledge and Belief of 1962 developed another interpretation: accessible worlds represent alternatives compatible with an agent's information. An epistemic operator then expresses what holds throughout those alternatives.

If the actual world is always among the alternatives, knowledge is factive: knowing $A$ entails $A$. A model of belief may omit that requirement. Idealized closure under logical consequence creates a further issue, usually called logical omniscience, when the intended agents have limited reasoning abilities.

Georg Henrik von Wright's work on deontic logic gave obligation and permission their own formal treatment. An obligation need not be fulfilled, so an unrestricted inference from “ought” to “is” would misdescribe that interpretation.

The same mathematical framework can therefore clarify different subjects, provided that the meaning of accessibility and the justification for each axiom remain explicit.

Provability as a modal interpretation

Gödel had already connected modal ideas with provability in 1933. Later work associated with Löb and Solovay gave this connection a precise metamathematical form.

Read $\Box A$ as “the chosen arithmetical theory proves $A$,” using a standard arithmetized provability predicate. Löb's theorem motivates

the characteristic axiom of provability logic GL.

This is not the unrestricted assertion that every theorem is true, available within the theory itself. The placement of the boxes records statements about proofs of statements about proofs.

Solovay's 1976 arithmetical completeness theorem identifies GL with the modal principles valid under all arithmetical substitutions in the standard provability interpretation for PA, with the usual metatheoretical soundness assumptions. Its scope is precise: it concerns this interpretation, not every possible notion of evidence.

Modal logic thus reconnects with the incompleteness theorems. Theorems limiting self-verification become principles in a language designed to reason about provability itself.

The next question

Modal logic enriches a language with operators while often retaining classical reasoning inside each world. Other traditions change the underlying account of truth, consequence, relevance, or the use of assumptions. Those changes require their own motivations and examples.

Sources and further reading

• C. I. Lewis, A Survey of Symbolic Logic (1918); Lewis and C. H. Langford, Symbolic Logic (1932).
• Ruth C. Barcan, “A Functional Calculus of First Order Based on Strict Implication” (1946), Journal of Symbolic Logic 11, 1–16. Publication record.
• Bjarni Jónsson and Alfred Tarski, “Boolean Algebras with Operators,” parts I and II (1951–1952).
• Arthur N. Prior, Time and Modality (1957); Jaakko Hintikka, Knowledge and Belief (1962).
• Saul A. Kripke, “Semantical Analysis of Modal Logic I: Normal Modal Propositional Calculi” (1963).
• Robert M. Solovay, “Provability Interpretations of Modal Logic” (1976).
• Modal Logic and Ruth Barcan Marcus, Stanford Encyclopedia of Philosophy, for historical context and bibliography.