nLab
validity

Validity

Idea

To judge whether a modal logic gives a good encoding of the properties of a particular relational structure, we need to put aside the valuations and to concentrate on the frames. A formula will be valid on a frame 𝔉\mathfrak{F} if it is true at every state in every model that can be built from 𝔉\mathfrak{F}. More formally:

Definition
  • A formula ϕ\phi is said to be valid at a state ww is a frame 𝔉=(W,R 1,,R n)\mathfrak{F}= (W,R_1,\ldots, R_n) (notation 𝔉,wϕ\mathfrak{F},w \models \phi) if ϕ\phi is true at ww in every model 𝔐=(𝔉,V)\mathfrak{M} = (\mathfrak{F},V), based ion 𝔉\mathfrak{F}.

  • A formula, ϕ\phi, is valid in a frame 𝔉\mathfrak{F} (notation 𝔉ϕ\mathfrak{F}\models \phi) if it is valid at every state of 𝔉\mathfrak{F}.

  • If 𝔽\mathbb{F} is a class of frames (all of the same relational signature), then we say ϕ\phi is valid in 𝔽\mathbb{F} (notation 𝔽ϕ\mathbb{F}\models \phi if 𝔉ϕ\mathfrak{F}\models \phi for all 𝔉𝔽\mathfrak{F}\in \mathbb{F}, and is valid, ϕ\models\phi, if it is valid on the class of all frames.

Fixing a given set PP of atomic formulae and the relational signature that we are considering:

Proposition

The set of formulae that are valid on a class,F\mathbf{F}, of frames of that signature forms a logic.

(We restrict to Kripke frames (i.e. to binary relations) for simplicity of exposition, and refer to the sources, such as Blackburn et al, for a fuller discussion.)

We denote the logic thus specified by Λ F\Lambda_\mathbf{F}.

References

Generally this entry is based on

  • P. Blackburn, M. de Rijke and Y. Venema, Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53, 2001,

(any mistakes or errors of interpretation are due to ….!)

Revised on December 24, 2010 07:44:47 by Toby Bartels (75.88.75.53)