modal logic B
The modal logic B (for Brouwerian) is the smallest normal modal logic containing the following schemas:
-
•
(T) , and
-
•
(B) .
In this entry (http://planetmath.org/ModalLogicT), we show that T is valid in a frame iff the frame is reflexive![]()
.
Proposition 1.
B is valid in a frame iff is symmetric.
Proof.
First, suppose B is valid in a frame , and . Let be a model based on , with , a propositional variable. Since , , and by assumption, for all such that . In particular, , which means there is a such that and . But this means that , so , whence , and is symmetric.
Conversely, let be a symmetric frame, a model based on , and a world in . Suppose . If , then there is a such that , with . This mean for no with , we have . Since is symmetric, , so , a contradiction![]()
. Therefore, , and as a result.
∎
As a result,
Proposition 2.
B is sound in the class of symmetric frames.
Proof.
Since any theorem![]()
in B is deducible from a finite sequence
consisting of tautologies
![]()
, which are valid in any frame, instances of B, which are valid in symmetric frames by the proposition
above, and applications of modus ponens
![]()
and necessitation, both of which preserve validity in any frame, whence the result.
∎
In addition, using the canonical model of B, we have
Proposition 3.
B is complete 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 . We want to show that , or that . It is then enough to show that if , then . If , because is maximal, or by modus ponens on B, or by the substitution theorem on , or by the definition of , or since , or , since is maximal, or by the definition of . So is symmetric, and 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 |