Matpic
mathematics, in pictures
Concept

Accessibility

The relation between worlds of a Kripke model saying which are visible from which, and the whole of what a modal operator quantifies over. Every classical modal axiom turns out to hold on exactly the frames whose accessibility relation has a stated property.

Named by 3 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 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

Named alongside it

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

Exhaustive searchKripke modelModal logicAxiomExpressive powerFrameBisimulationDecision procedureDefinabilityEquivalence relationNecessityReflexive

All concepts