Editing Kripke semantics (section)

===Basic definitions===
 
A '''Kripke frame''' or '''modal frame''' is a pair <math>\langle W,R\rangle</math>, where ''W'' is a (possibly empty) set, and ''R'' is a [[binary relation]] on ''W''. Elements
of ''W'' are called ''nodes'' or ''worlds'', and ''R'' is known as the [[accessibility relation]].{{sfn|Gasquet|Herzig|Said|Schwarzentruber|2013|pages=14–16}}

A '''Kripke model''' is a triple <math>\langle W,R,\Vdash\rangle</math>,<ref>Note that the ''notion'' of 'model' in the Kripke semantics of modal logic ''differs'' from the notion of 'model' in classical non-modal logics: In classical logics we say that some formula ''F'' ''has'' a 'model' if there exists some 'interpretation' of the variables of ''F'' which makes the formula ''F'' true; this specific interpretation is then ''a model of'' the ''formula F''. In the Kripke semantics of modal logic, by contrast, a 'model' is ''not'' a specific 'something' that makes a specific modal formula true; in Kripke semantics a 'model' must rather be understood as a larger ''universe of discourse'' within which ''any'' modal formulae can be meaningfully 'understood'. Thus: whereas the notion of 'has a model' in classical non-modal logic refers to some individual formula ''within'' that logic, the notion of 'has a model' in modal logic refers to the logic itself ''as a whole'' (i.e.: the entire system of its axioms and deduction rules).</ref> where
<math>\langle W,R\rangle</math> is a Kripke frame, and <math>\Vdash</math> is a relation between nodes of ''W'' and modal formulas, such that for all ''w''&nbsp;∈&nbsp;''W'' and modal formulas ''A'' and ''B'':

* <math>w\Vdash\neg A</math> if and only if <math>w\nVdash A</math>,
* <math>w\Vdash A\to B</math> if and only if <math>w\nVdash A</math> or <math>w\Vdash B</math>,
* <math>w\Vdash\Box A</math> if and only if <math>u\Vdash A</math> for all <math>u</math> such that <math>w\; R\; u</math>.
We read <math>w\Vdash A</math> as “''w'' satisfies
''A''”, “''A'' is satisfied in ''w''”, or
“''w'' forces ''A''”. The relation <math>\Vdash</math> is called the
''satisfaction relation'', ''evaluation'', or ''[[Forcing (mathematics)|forcing]] relation''.
The satisfaction relation is uniquely determined by its
value on propositional variables.

A formula ''A'' is '''valid''' in:
* a model <math>\langle W,R,\Vdash\rangle</math>, if <math>w\Vdash A</math> for all <math>w \in W</math>,
* a frame <math>\langle W,R\rangle</math>, if it is valid in <math>\langle W,R,\Vdash\rangle</math> for all possible choices of <math>\Vdash</math>,
* a class ''C'' of frames or models, if it is valid in every member of ''C''.
We define Thm(''C'') to be the set of all formulas that are valid in
''C''.  Conversely, if ''X'' is a set of formulas, let Mod(''X'') be the
class of all frames which validate every formula from ''X''.

A modal logic (i.e., a set of formulas) ''L'' is '''[[Soundness|sound]]''' with
respect to a class of frames ''C'', if ''L''&nbsp;⊆&nbsp;Thm(''C''). ''L'' is
'''[[Completeness (logic)|complete]]''' wrt ''C'' if ''L''&nbsp;⊇&nbsp;Thm(''C'').