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	Meaning
B	—	Brouwer axiom A → □◇A
KB	—	K + B
KTB	—	K + T + B
R⁻¹	—	symmetric relation

Metatheory. Symmetric frames. Brouwer axiom. Completeness. Decidable.

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

Limitations. Less common. Specific applications unclear. Not reflexive alone. Intermediate.