A model for Modal Logic, which is specified as a tuple of sets (W, R, P).
- W is the set of all possible worlds.
- R is a set of binary relations on W, the accessibility relations.
- P is a set of functions, mapping propositional variables to subsets of W.
The set of worlds, W, is normally notated (α, β, γ, ....).
R specifies for each world whether each other world can be reached from it. αRβ =
true means β can be reached from α. αRα is not necessarily true.
There are several classes of R such as K, KT, K4, KB, D, S4, B, and
S5, which are defined by general rules on accessibility.
P contains functions such as ||p|| = {β, γ}, meaning p is true in world β and
γ.
- ||□(q)|| = {α} means q is true in every world accessible from α.
- ||◊(q)|| = {β} means q is true in some worlds accessible from β.
All the normal
propositional logic operations such as
implies,
two-way
implication,
and,
or,
negation etc can also be specified in this way.
-
K is that class of relations for which the K axiom is true. The K
axiom is □(p→q)→(□(p)→□(q)), or, if in all accessible worlds P implies Q,
then if P is true in all possible worlds, so is Q. A subset of KT, K4, KB, D, S4, B and S5.
-
KT is that class of relations for which the K axiom and the T
axiom are true. Such relations are reflexive. For all worlds a, aRa = true. The T axiom
is □(p)→p, or, if in all accessible worlds P is true, then P is true in the current
world. A subset of S4, B and S5.
-
K4 is that class of relations for which the K axiom and the 4
axiom are true. Such relations are transitive. For all worlds a,b and c, (aRb)^(bRc)→(aRc) is true.
The 4 axiom is □(p)→□(□(p)), or, if in all accessible worlds P is true, P is true in all
worlds accessible from all accessibile worlds. A subset of S4, B and S5.
-
KB is that class of relations for which the K axiom and the B
axiom are true. Such relations are symmetric. For all worlds a,c aRc→cRa. The B
axiom is p→□(◊(p)), or, if in all accessible worlds P is true, then from every
accessible world, there is at least one accessible world in which P is true. A subset of B and S5. (yes, KB is
a subset of B. Whilest K is a subset of KB. I
didn't name these things dagnamit!)
-
D is that class of relations for which the K axiom and the D
axiom are true. Such relations posses seriality. For all worlds a, there exists b,
such that aRb. The D axiom is □(p)→◊(p), or, if in all accessible worlds P is true,
then if P is true in least one accessible world.
-
S4 is that class of relations for which the
axioms of KT and K4 are true; namely the K axiom, the 4 axiom and the T axiom. Such
relations are reflexive and transitive. A superset of KT and K4.
-
B is that class of relations for which the
axioms of KT and KB are true. Such relations are reflexive and
symmetric. A superset of KT and KB.
-
S5 is the big one. It is that class of relations for which the
axioms of KT, KB and K4 are true. Such relations are reflexive, symmetric and
transitive, or euclidean. Basically, you can get everywhere from anywhere.
This encodes the concept that if something is not known, then it is known that it is not
known. eg. ◊(p)→□(◊(P)), or, if P is true in at least one accessible world, then
it is true in at least one world accessible from every accessible world. Draw a diagram,
it's easier that way. A superset of KT, KB and K4.