Necessarily Interactive

A playground for possible worlds, where the shape of a graph decides the laws of logic.

Philosophers love to say a thing is possible if it's true in some possible world, and necessary if it's true in every world you can reach from here. Kripke made that precise: a bunch of worlds, arrows saying which world can "see" which, and a verdict on what's true where. Below you can build such a universe by hand — drag worlds, draw arrows, flip facts on and off — and watch the modal operators □ ("necessarily") and ◇ ("possibly") sort themselves out. The punchline, in the right-hand panel, is a small miracle: the purely geometric shape of your arrow-graph secretly fixes which famous laws of modal logic come out true.

Move / connect Add / remove worlds

Load a shape

A formula to evaluate

Which atoms are true where (a valuation)

formula true here formula false here

What your frame's shape makes true — for every valuation

These verdicts ignore the valuation above: an axiom is valid on a frame when it holds at every world no matter how you assign the atoms. Each one is validated by exactly one geometric property of your arrows — and the app checks it two ways: the geometric test, and an honest brute-force sweep over all 2^{(worlds × atoms)} valuations.

Try this. Type □p → p ("what's necessary is actually true"). Now press Add all self-loops so every world can see itself — the T axiom turns green. Delete one self-loop and it fails. That's the whole content of the theorem: reflexive arrows ⟺ the axiom T. Then hunt for the shapes behind 4 (transitive), B (symmetric) and 5 (euclidean).

The rules the app is using

A model is a set of worlds W, an accessibility relation R (the arrows), and a valuation saying which atoms hold at each world. Truth at a world w is defined by:

□φ is true at w ⟺ φ is true at every world v with an arrow w → v (vacuously true if w has no outgoing arrows).
◇φ is true at w ⟺ φ is true at some world v with w → v.
The connectives ¬ ∧ ∨ → ↔ are the ordinary truth-tables.

The five correspondences the right panel reports are the standard ones:

T □p → p ⟺ reflexive (every world sees itself).
D □p → ◇p ⟺ serial (every world sees something).
4 □p → □□p ⟺ transitive (w→v→u forces w→u).
B p → □◇p ⟺ symmetric (w→v forces v→w).
5 ◇p → □◇p ⟺ euclidean (w→v and w→u forces v→u).

K □(p→q) → (□p→□q) is valid on every frame — it's the engine that makes all of this "normal" modal logic. Adding all five conditions at once (reflexive + symmetric + transitive) gives an equivalence relation: the logic S5, the modal logic of plain "true somewhere / true everywhere."

How to type formulas (ASCII shortcuts)

Use the buttons, or type: []→□, <>→◇, ~ or !→¬, &→∧, |→∨, ->→→, <->→↔. Atoms are p, q, r. Precedence, tightest first: ¬ □ ◇, then ∧, then ∨, then → (right-associative), then ↔.

A single self-contained page — no libraries, no network. The maths is finite Kripke semantics and the Sahlqvist frame correspondences; verdicts are computed live and cross-checked by exhaustive valuation sweep. Built as a mock-up widget for Enriched Jam Sham.