E–S5 congruential lattice
loading…
Each node is a logic, E extended by some of the schemata M, C, N, K, D, T, B, 4, 5 and P (◇⊤), with the class of neighborhood frames satisfying their conditions (lowercase). An edge rises to a stronger logic with no node between.
view
color nodes by
The keystone (Q1) is open: must a frame with k, d and b have c? If so, the orange edge's ends, and , are one class of frames; as logics, exactly when ⊢ C.
How to read this map
Nodes. Each node is a set of the ten conditions m, c, n, k, d, t, b, 4, 5, p, closed under the entailments proved among them; it defines a class of neighborhood frames and a logic, E extended by the matching schemata, in capitals. P is ◇⊤; p says no world has ∅ as a neighborhood. Conditions are joined by ⊗; an entailment among conditions is written ⟹, a derivation of a schema ⊢.
Names. A name is E, or K when the logic has M, C and N, then a smallest set of schemata generating it, P only if needed; D, T, B, S4, S5 and ES5 keep their usual names. A node's panel lists its conditions, its name's generators in green.
Edges. An edge joins a logic to a stronger one with no logic of the map between, so a logic sits above all it extends. Each row holds the logics of one rank, E at the bottom and S5 at the top. In the 3-D view left, right and depth only spread the nodes; in the layered view the order within a row only reduces crossings. Drag to turn or move; scroll or pinch to zoom.
Colors. Color the nodes by rank, the number of conditions, or by completeness, whether n-cube proves the logic determined by its class. Rank runs from 0 for E to for S5. Determined: yes, through the proper canonical frame (Chellas' smallest canonical model) or, for logics, its k-closure, the least canonical frame satisfying k. Not yet built: n-cube builds no canonical frame in its class; several, the normal ones among them, are determined in the literature. Open: , the keystone's logic.
The keystone (Q1): does every frame with k, d and b have c? The nodes are classes of frames if not and if so, the orange edge's ends, and , becoming one; as logics they are one exactly when proves C. Assume Q1 to see .
Clicking a node opens its panel and isolates its cone: extensions above, sublogics below; in the completeness coloring the cone keeps its colors and dims the rest. Click the background, or press Escape, to clear.