Matpic
mathematics, in pictures
Concept

Modal logic

The logic of an operator meaning *necessarily*, evaluated over diagrams of worlds and arrows. Its axioms are not a matter of taste: each holds on exactly the diagrams whose arrows have a stated property.

Named by 5 essays across one field — each of them below, with the objects they name alongside it.

Which axioms hold on which frames. A table of frames against modal axioms, each cell decided by checking the axiom under every valuation.

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 · Modal logic Two models the modal language cannot separate, and two it can. Four Kripke models in two pairs: the upper pair joined by a bisimulation and agreeing on every formula, the lower pair separated by a formula found by search.

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 · Modal logic A model whose worlds are sets of sentences. Worlds labelled by which of a fixed finite set of formulas they accept, with an arrow wherever every boxed formula accepted by one has its inside accepted by the other.

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.

logic · Modal logic Axioms, the conditions on the arrows they answer to, and the one that answers to none. A table of modal axioms with the property of the accessibility relation each corresponds to, every row decided by sweeping all relations on up to four worlds.

The axiom with no property of the arrows

The first rung matched each axiom to a condition on the arrows by hand. 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 · Modal logic The frames on which provability makes sense, and the two that are refused. Six small frames marked by whether Löb's axiom is valid on them: transitive frames with no cycles accept it, and any frame in which a world can reach itself does not.

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 · Modal logic

Named alongside it

The objects these essays reach for when they reach for this one.

Kripke modelAccessibilityExhaustive searchFrameAxiomDecision procedureExpressive powerBisimulationCompletenessConsistencyDefinabilityEquivalence relation

All concepts