Generator

a chain — where p is necessary and where it is merely possible

A generator in the logic library, called 40 times across 7 essays. Below: what it draws with nothing chosen and at each mode an essay asks for, what it checks while drawing, and everywhere it is used.

kripke is one function. Everything below came out of it during this build, at parameters taken from the essays rather than invented for this page — so a figure here is the same figure a reader meets in an essay, and if the generator changes, this page changes with it.

With nothing chosen

a chain — where p is necessary and where it is merely possible. A directed graph of worlds with an assignment for p, and the box and diamond values computed at each world.

A chain of 18 worlds, and the 3 the formulas can tell apart

Two models the modal language cannot separate, and two it can

A model whose worlds are sets of sentences

Where the tower of boxes stops saying anything new

The frames on which provability makes sense, and the two that are refused

What it checks while it draws

Collected by running the family and recording what it asserted, not written here. The count is how many separate times the claim was put to the test while these drawings were made.

□□p → □p is valid exactly on the dense frames ×1
□p → □□p is valid exactly on the transitive frames ×1
□p → ◇p is valid exactly on the serial frames ×1
□p → p is valid exactly on the reflexive frames ×1
□p at a world is p at every world it can reach ×1
◇□p → □◇p is valid exactly on the confluent frames ×1
◇p → □◇p is valid exactly on the euclidean frames ×1
◇p at a world is p at some world it can reach ×1
4 is valid on a frame exactly when the frame is transitive ×1
5 is valid on a frame exactly when the frame is euclidean ×1
a formula separating the other pair exists among those searched ×1
a transitive model filters to a transitive quotient here, checked rather than assumed ×1
a world and a valuation were found at which the axiom fails ×1
a world that reaches nowhere makes every necessity true and every possibility false ×1
and fewer worlds than the model it came from ×1
and it is deeper than anything the closure could ask ×1
and no frame with any worlds in it validates both Löb's axiom and □p → p ×1
and on every one of them ¬□⊥ is a fixed point of ¬□p ×1
and some class of the quotient can — the collapse invents a way back that the model has none of ×1
and the other two starting worlds are not ×1
and two frames agreeing on all of them disagree about the axiom ×1
and validates what is valid ×1
B is valid on a frame exactly when the frame is symmetric ×1
between one and five axioms are tabulated ×1
between two and six frames are compared ×1
D is valid on a frame exactly when the frame is serial ×1
excluded middle at a stage is exactly p there or ¬p there ×1
formulas up to depth two to four are compared ×1
Löb's axiom is valid exactly on the transitive frames with no cycles ×1
no condition in the catalogue matches McKinsey's axiom ×1
no stage forces both p and its negation ×1
no world of the model can be returned to ×1
on a frame with the property the axiom holds everywhere, under every valuation ×1
on that frame every deeper modality agrees with the first, not only the second ×1
one of the two frames collapses the tower and the other does not ×1
p → □◇p is valid exactly on the symmetric frames ×1
so every frame of the logic is transitive, which Löb's axiom implies ×1
some depth of looking ahead separates the chain from its quotient ×1
some frame this family knows has the property ×1
some frames validate it ×1
some stage forces neither p nor its negation, so p ∨ ¬p fails there ×1
T is valid on a frame exactly when the frame is reflexive ×1
the axiom is one of the five ×1
the bisimilar worlds agree on every formula up to the drawn depth ×1
the chain runs between eight and twenty-four worlds ×1
the deeper closure is asked for or not ×1
the frame is one this figure knows ×1
the gallery's verdict for a branch, both ends dead is the sweep's ×1
the gallery's verdict for a single dead end is the sweep's ×1
the gallery's verdict for a transitive chain is the sweep's ×1
the gallery's verdict for a two-cycle is the sweep's ×1
the gallery's verdict for a world seeing itself is the sweep's ×1
the gallery's verdict for one step and stop is the sweep's ×1
the model is the chain or the strict order on its worlds ×1
the model refutes □p → p, which is not valid in this logic ×1
the quotient has at most one world for each way of answering the closure ×1
the sweep runs over frames on three or four worlds ×1
the tower is followed to between two and four boxes ×1
the truth lemma holds for □□p: it is true at a world exactly when it is true at that world's class ×1
the truth lemma holds for □p: it is true at a world exactly when it is true at that world's class ×1
the truth lemma holds for p: it is true at a world exactly when it is true at that world's class ×1
the truth lemma holds: □□p is true exactly where it is accepted ×1
the truth lemma holds: □p is true exactly where it is accepted ×1
the truth lemma holds: p is true exactly where it is accepted ×1
the two starting worlds are related by the bisimulation ×1
the view is one the family draws ×1
this frame is not reflexive, so the axiom has a chance of failing ×1
this frame is not symmetric, so the axiom has a chance of failing ×1
this frame is not transitive, so the axiom has a chance of failing ×1
two frames this family knows ×1
what is established at a stage stays established later ×1
worlds share a class exactly when no formula of the closure tells them apart ×1

Where it is called

Every figure on this list is drawn by the same rule, so a change to the rule changes all of them at once. That is why the list is published.

Logic

How many worlds a formula can need

A modal formula can be true in a model with infinitely many worlds. It can also be true in a small one — and the small one is built from the large one by throwing away every distinction the formula was never able to make.

Logic

Necessity that means provable

Read the box as "the theory proves" and one modal logic stops being a proposal about what necessity might mean. It becomes a complete description of what a formal system can prove about its own proofs — and its frames run forward, compose, and stop.

Logic

The axiom is the shape of the graph

Add one operator meaning necessarily and the choice of which axioms to accept stops being a matter of taste. Each candidate axiom is true of exactly those worlds-and-arrows diagrams whose arrows have a stated property, and a logic is a class of graphs.

Logic

The axiom with no property of the arrows

Each axiom of modal logic can be matched by hand to a condition on the arrows between worlds. There is a recipe that does it for a whole class of axioms, and there is an axiom the recipe cannot reach — not because nobody has looked, but because no condition on the arrows defines it at all.

Logic

The middle that is not excluded

Either it is raining or it is not. Drop that as an axiom and what is left is still a logic — one with models made of open sets and of stages of knowledge, in which a set and its negation between them miss the boundary.

Logic

Two diagrams the language cannot tell apart

A modal formula sees a diagram of worlds and arrows through a very narrow window. Exactly how narrow is settled by a game: where one player can answer every move, no formula whatever separates the two starting worlds, however different the diagrams look.

Logic

Worlds built out of sentences

A Kripke model needs worlds, and nothing so far has said where worlds come from. They can be made of the syntax: a world is a set of formulas it commits to, one world sees another when the boxed commitments line up, and in the model that results every formula is true exactly where it was assumed.

The whole library · What the figures prove