KB Modal Logic

Origin. The B axiom (p → □◇p) was named for Brouwer by Becker (1930), on an analogy with intuitionistic double negation that later commentators judged mistaken; Kripke's symmetric-frame semantics (1963) made KB a system rather than an axiom. KB = K + B. Symmetric frames. Brouwerian axiom. Possibility-necessity link.

Models. Symmetric accessibility. Dual direction. Brouwer axiom. Between K and S5.

Formalism.

Axioms: K: □(A → B) → (□A → □B). B: A → □◇A. Brouwer axiom.

Rules: Modus ponens. Necessitation.

B axiom reading: If A actual, necessarily possible. What is, could have been. From here, here is reachable.

Frame condition: Symmetry: wRv → vRw. Bidirectional accessibility. Can return.

Dual form: ◇□A → A. If possibly necessary, then true. Characteristic dual.

Not valid: □A → A (needs reflexivity). □A → □□A (needs transitivity). Neither T nor 4.

KTB (Brouwerian): K + T + B. Reflexive + symmetric. Stronger than KB alone. "System B" proper.

Relation to S5: S5 = KTB + 4 = KT5. KB lacks reflexivity and transitivity. Weaker than S5. Symmetric but not equivalence.

Philosophical: Brouwerian intuitionism connection (loose). Reversibility of possibility. Actuality special.

Symbols.

Symbol	Unicode	Name	Meaning
□	U+25A1	Box / Necessity	True at all accessible worlds
◇	U+25C7	Diamond / Possibility	True at some accessible world
⊢	U+22A2	Derivability	Provable in the calculus
⊨	U+22A8	Validity	Frame or model satisfaction
⁻¹	U+207B, U+00B9	Superscript minus one	Converse of a relation
⊊	U+228A	Proper inclusion	Strictly weaker logic
B	—	Brouwer axiom	A → □◇A
KB	—	System KB	K + B; the logic of symmetric frames
KTB	—	System B	K + T + B; reflexive symmetric frames
R	—	Accessibility relation	Symmetric binary relation on W
R⁻¹	—	Converse relation	Equal to R when R is symmetric

Metatheory. Sound and complete with respect to the class of symmetric Kripke frames. B, in the form p → □◇p, is a Sahlqvist formula, so KB is canonical and symmetry is first-order definable by ∀w∀v (wRv → vRw); completeness follows from the canonical model, whose accessibility relation is symmetric. KB has the finite model property and is decidable, and its satisfiability problem is PSPACE-complete, so symmetry alone yields none of the tractability that S5 gains from collapsing iterated modalities. Symmetric frames are closed under generated subframes, disjoint unions and bounded morphic images, as Sahlqvist elementarity predicts. Over symmetric frames 4 and 5 become interderivable, so KB4 = KB5, the logic of partial equivalence relations. KB is a proper sublogic of KTB and of KB4, and KTB4 = KT5 = S5. KTB is incomparable with S4: neither contains the other, since 4 fails on reflexive symmetric frames and B fails on preorders.

Applies to. Modal logic. Symmetry conditions. Between systems. Reversibility.

Limitations. KB fixes only the direction of accessibility and settles nothing else: □A → A fails, □A → ◇A fails, and □⊥ remains satisfiable at dead ends, so necessity in KB need not be veridical or even consistent. Symmetry is implausible for most intended readings — temporal accessibility is not symmetric, deontic accessibility is not symmetric, and under the epistemic reading B becomes A → K¬K¬A, requiring that every truth be one the agent cannot rule out, which fails whenever an agent is confidently mistaken. B is also unsound for provability, since a symmetric transitive frame validating T collapses to S5, and GL is irreflexive and transitive. Even with T added, KTB retains infinitely many pairwise non-equivalent modalities, so no normal form for iterated boxes is available; adding 4 collapses the system all the way to S5, leaving no intermediate logic of reflexive symmetric transitive-but-not-euclidean frames.