modal logic B


The modal logic B (for Brouwerian) is the smallest normal modal logic containing the following schemas:

  • (T) AA, and

  • (B) AA.

In this entry (http://planetmath.org/ModalLogicT), we show that T is valid in a frame iff the frame is reflexiveMathworldPlanetmathPlanetmath.

Proposition 1.

B is valid in a frame F iff F is symmetric.

Proof.

First, suppose B is valid in a frame , and wRu. Let M be a model based on , with V(p)={w}, p a propositional variable. Since wV(p), wp, and wpp by assumptionPlanetmathPlanetmath, vp for all v such that wRv. In particular, up, which means there is a t such that uRt and tp. But this means that tV(p), so t=w, whence uRw, and R is symmetric.

Conversely, let be a symmetric frame, M a model based on , and w a world in M. Suppose wA. If ⊧̸wA, then there is a u such that wRu, with ⊧̸uA. This mean for no t with uRt, we have tA. Since R is symmetric, uRw, so ⊧̸wA, a contradictionMathworldPlanetmathPlanetmath. Therefore, wA, and wAA as a result. ∎

As a result,

Proposition 2.

B is sound in the class of symmetric frames.

Proof.

Since any theoremMathworldPlanetmath in B is deducible from a finite sequencePlanetmathPlanetmath consisting of tautologiesMathworldPlanetmath, which are valid in any frame, instances of B, which are valid in symmetric frames by the propositionPlanetmathPlanetmath above, and applications of modus ponensMathworldPlanetmath and necessitation, both of which preserve validity in any frame, whence the result. ∎

In additionPlanetmathPlanetmath, using the canonical model of B, we have

Proposition 3.

B is completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath in the class of reflexive, symmetric frames.

Proof.

Since B contains T, its canonical frame 𝐁 is reflexive. We next show that any consistent normal logic Λ containing the schema B is symmetric. Suppose wRΛu. We want to show that uRΛw, or that Δu:={BBu}w. It is then enough to show that if Aw, then AΔu. If Aw, ¬Aw because w is maximal, or ¬Aw by modus ponens on B, or ¬Aw by the substitution theorem on A¬¬A, or ¬AΔw by the definition of Δw, or ¬Au since wRΛu, or Au, since u is maximal, or AΔu by the definition of Δu. So RΛ is symmetric, and R𝐁 is both reflexive and symmetric. ∎

Title modal logic B
Canonical name ModalLogicB
Date of creation 2013-03-22 19:34:11
Last modified on 2013-03-22 19:34:11
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 8
Author CWoo (3771)
Entry type Definition
Classification msc 03B45
Defines B