B Modal Logic

Origin. Oskar Becker, "Zur Logik der Modalitäten" (Jahrbuch für Philosophie und phänomenologische Forschung 11, 1930), introduced the axiom and its name: he called A → □◇A the Brouwersche Axiom because reading negation as impossibility turns the intuitionistically valid A → ¬¬A into it. The analogy is the whole of the association — Brouwer never worked in modal logic — and Becker's own aim was to cut down the number of non-equivalent modalities. The system — T plus the axiom — is the Brouwersche system of Kripke, "Semantical Analysis of Modal Logic I: Normal Modal Propositional Calculi" (1963), which proved it complete for reflexive symmetric frames and decidable; the Lemmon–Scott nomenclature writes it KTB.

Models. Kripke frames whose accessibility relation is reflexive and symmetric: every world sees itself and every step can be retraced, but steps do not compose. A reflexive symmetric frame is a graph with a loop at every vertex, so KTB stands to graphs as K4 and S4 stand to orderings. KTB = KB + T = KT + B. It is one of the two standard strengthenings of T, the other being S4; the two are incomparable, and their join is S5 = KTB + 4.

Formalism.

Axioms: K: □(A → B) → (□A → □B). T: □A → A. B: A → □◇A. KTB = K + T + B.

Rules: Modus ponens. Necessitation: from ⊢ A infer ⊢ □A.

Frame condition: Reflexivity: ∀w. wRw. Symmetry: ∀w∀v. wRv → vRw. T and B are Sahlqvist formulas: canonical, elementary.

Dual form: ◇□A → A. What is possibly necessary is true.

Not derivable: 4: □A → □□A (needs transitivity). 5: ◇A → □◇A (needs euclideanness). So ◇◇A does not reduce to ◇A, and □ⁿA are pairwise non-equivalent.

Modalities: Infinitely many pairwise non-equivalent modalities, as in T. Becker introduced B to reduce the modalities; in KTB they stay infinite.

Relations to neighbours: KB ⊊ KTB: add T. KT ⊊ KTB: add B. KTB ⊊ S5 = KTB + 4. KTB and S4: incomparable extensions of T — 4 fails on reflexive symmetric frames, B fails on preorders. The join of KTB and S4 is S5.

Symbols.

Symbol	Unicode	Name	Meaning
□	U+25A1	Box / Necessity	True at all accessible worlds
◇	U+25C7	Diamond / Possibility	True at some accessible world
⊨	U+22A8	Validity	Frame or model satisfaction
⊢	U+22A2	Derivability	Provable in the calculus
⊊	U+228A	Proper inclusion	Strictly weaker logic
∀	U+2200	Universal quantifier	Frame conditions on worlds
B	—	Brouwersche axiom	A → □◇A
T	—	Veridicality axiom	□A → A
K	—	Distribution axiom	□(A → B) → (□A → □B)
4	—	Transitivity axiom	□A → □□A; exactly what KTB lacks
KTB	—	Brouwerian system	K + T + B; the logic of reflexive symmetric frames
R	—	Accessibility relation	Reflexive symmetric binary relation on worlds

Metatheory. Sound and complete with respect to reflexive symmetric frames, proved by Kripke (1963) and automatic by canonicity, since T and B are Sahlqvist and the frame condition is elementary. The finite model property holds by filtration — the reflexive symmetric closure of a filtration stays inside the frame class — and is recorded, with the decidability that follows from it and finite axiomatizability, in Chagrov and Zakharyaschev, Modal Logic (1997). Satisfiability is PSPACE-complete, and the attribution needs care: Ladner (1977) proved PSPACE-hardness for every normal logic between K and S4, an interval that does not contain KTB because S4 lacks B, and the hardness for KTB and KB — already for their one-variable fragments — is Rybakov and Shkatov, "Complexity of finite-variable fragments of propositional modal logics of symmetric frames" (Logic Journal of the IGPL 27, 2019). The lattice of normal extensions is charted only at the top: the unique logics of codimension one and two are the logic of a single reflexive point and the logic of the two-element cluster, and at codimension three Koussas, Kowalski, Miyazaki, and Stevens (2021) constructed a continuum of extensions, built from an uncountable family of graphs. The canonical-formula machinery of the transitive logics has no comparably effective KTB counterpart, so the lattice is far less understood than that of K4, where Blok (1980) could already exhibit a continuum of pretabular varieties.

Applies to. The Brouwersche slot in the map of Lewis-era systems: the standard extension of T incomparable with S4. Frame correspondence for symmetry with reflexivity, between KB below and S5 above. Readings on which accessibility is a tolerance relation — similarity or indistinguishability within a margin — which is reflexive and symmetric but not transitive. Modal logic on graphs, since reflexive symmetric frames are graphs with loops.

Limitations. Without 4 there is no reduction of iterated modalities: ◇◇A does not collapse to ◇A, the modalities □, □□, □□□, … are pairwise non-equivalent, and the normal-form arguments available in S4 and S5 are unavailable here. Adding 4 overshoots: a reflexive symmetric transitive relation is an equivalence relation, so KTB + 4 = S5 and there is no logic of reflexive symmetric frames with transitivity short of the full collapse. Symmetry disqualifies most intended readings — temporal accessibility is not symmetric, deontic accessibility is not symmetric, and B is unsound for provability, since GL's frames are irreflexive and transitive. Under the epistemic reading B becomes A → K¬K¬A, requiring that no truth can be ruled out by the agent, which fails for any agent confidently mistaken about anything. And the theory of its extensions is underdeveloped beside that of the transitive logics: the continuum at codimension three puts even the almost-tabular layer of the lattice beyond finite description, and the canonical-formula methods that chart the extensions of K4 have no KTB counterpart.