The semantics of modality. Kripke models (worlds + accessibility) are rigorous, complete for the standard modal systems, and the working foundation of modal, temporal, epistemic, and provability logic across philosophy and computer science.
A relay, honestly told. The quantified-modal systems and the Barcan formula are [[ruth-barcan-marcus]]'s (1946); Kripke supplied the possible-worlds interpretation (c. 1959–63). Two halves of one achievement — and a real, documented priority dispute between them.
Math first. The possible worlds are a precise mathematical device. Whether other worlds "really exist" is a separate philosophical question (Kripke himself was cautious; David Lewis went further). The semantics works regardless.
Three worlds; in each, a fact p is true or false (click a world to toggle p). The accessibility relation — which worlds each can "see" — is set by the buttons below, and its shape is everything. Evaluate □p and ◇p at the highlighted world, and watch the famous modal axioms switch on and off as you change the relation: a reflexive relation validates "□p → p" (system T); add transitivity for S4; make it an equivalence for S5.
"Possible worlds are stipulated, not discovered by powerful telescopes." — Saul Kripke, Naming and Necessity
Each modal axiom corresponds to a property of accessibility: reflexive ↔ T, transitive ↔ 4, symmetric ↔ B, equivalence ↔ S5. Soundness and completeness tie the syntax of necessity to the geometry of worlds — exactly.
His later work argued names are rigid designators — they pick the same thing in every possible world — overturning the dominant theory of meaning. (The "tags" idea [[ruth-barcan-marcus]] had voiced earlier.)
Possible-worlds semantics didn't just rescue modal logic from suspicion — it colonised half of logic and computer science. Read the worlds as moments in time and you have temporal logic, used to verify that a chip or protocol never reaches a bad state. Read accessibility as "compatible with what an agent knows" and you have epistemic logic, the logic of knowledge and belief in AI and economics. Read it as "provable" and you recover, in modal dress, [[kurt-godel]]'s incompleteness. The model checkers that prove safety properties of real hardware and software are walking Kripke structures. A picture invented by a teenager became the standard semantics for reasoning about what must, might, will, or is known to be — one of the most fruitful single ideas in modern logic.
Gate kept on. Kripke's contribution is real, rigorous, and enormous: the possible-worlds semantics for modal logic, with its soundness and completeness theorems linking frame conditions to modal systems, is the standard model used everywhere from philosophy to formal verification, and he produced the core of it as a teenager — a genuine prodigy who published the foundational papers around 1959–1963. The honest qualification is one of credit and sequence, and it ties directly to the sphere before this one: the quantified modal logics and the Barcan formula were [[ruth-barcan-marcus]]'s in 1946; the idea of names as world-spanning "tags" was also hers before it was his "rigid designators." Kripke supplied the semantics — the worlds-and-accessibility interpretation that made the systems intuitive — which is a major and largely independent achievement, but the popular tendency to credit him with the whole edifice is the error this lineage corrects: it is, properly, Barcan's syntax and Kripke's semantics, and there was a sharp, well-documented priority dispute (including a notorious seminar) between them. Finally, the "possible worlds" are a mathematical model, not a commitment that other universes literally exist — Kripke was careful on this; the device earns its keep by working, regardless of metaphysics. ⚑ With Kripke the modal thread that [[ruth-barcan-marcus]] opened is complete: the syntax, and the worlds that give it meaning. [[gerhard-gentzen]] ←.