E–S5 congruential lattice

loading…

Nodes are the logics of [E, S5+P] (each is also its neighborhood frame-class), colored by rank; edges are covering relations. Click a node, search, or pick a region.

One collapse is genuinely open — Q1: does adding k, d, b force c? It's undecided both as a condition on frames (k⊗d⊗b ⟹ c) and as a derivation in the logic (EKDB ⊢ C). Tick assume Q1 to merge the orange edge's two endpoints into one logic (147); leave it and they stay distinct (148).

assume Q1 (merge it)

controls

query — highlight logics by a condition expression

atoms m c n k d t b 4 5 p · words normal gold regular · ops & | - ( )

show:

highlight regions (stack several)

show all labels (else: selected / highlighted)

isolate cone on click (up/down-set)

landmark logics (the gold-labeled set · click to highlight)

click a node…

legend

rank = #conditions

open question:

k⊗d⊗b ⟹ c — Q1, merge (semantic)