modal logic T


The modal logic T is the smallest normal modal logic containing the schema T:

AA

A Kripke frame (W,R) is reflexiveMathworldPlanetmathPlanetmath if R is reflexive on W.

Proposition 1.

T is valid in a frame F iff F is reflexive.

Proof.

First, suppose is not reflexive, say, (w,w)R. Let M be a model based on such that V(p)={uwRu}, where p is a propositional variable. By the construction of V(p), we see that for all u such that wRu, we have up, so wp. But since wV(p), ⊧̸wp. This means that ⊧̸wpp.

Conversely, let be a reflexive frame, and M any model based on , with w a world in M. Suppose wA. Then for all u such that wRu, uA. Since wRw, we get wA. Therefore, wAA. ∎

As a result,

Proposition 2.

T is sound in the class of reflexive frames.

Proof.

Since any theoremMathworldPlanetmath in T is deducibleMathworldPlanetmath from a finite sequencePlanetmathPlanetmath consisting of tautologiesMathworldPlanetmath, which are valid in any frame, instances of T, which are valid in reflexive 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 T, we have

Proposition 3.

T is completePlanetmathPlanetmathPlanetmathPlanetmath in the class of reflexive frames.

Proof.

We show that the canonical frame 𝐓 is reflexive. For any maximally consistent set w, if AΔw:={BBw}, then Aw. Since T contains AA, we get that Aw by modus ponens and the fact that w is closed under modus ponens. Therefore wR𝐓w, or R𝐓 is reflexive. ∎

T properly extends the modal system D, for AA is not valid in any non-reflexive serial frame, such as the one (W,R), where W={u,w} and R={(u,u),(w,u)}: just let V(p)={w}. So wp and ⊧̸up, or ⊧̸wp. This means ⊧̸wpp.

Title modal logic T
Canonical name ModalLogicT
Date of creation 2013-03-22 19:33:58
Last modified on 2013-03-22 19:33:58
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 9
Author CWoo (3771)
Entry type Definition
Classification msc 03B45
Related topic ModalLogicD
Defines T