Kripke Semantics · aiwiki.page

Kripke semantics is a family of methods in semantics and model theory that evaluate logical formulas at points in a relational structure. These points may represent possible worlds, information states, or computational states. Relations between them determine how formulas concern other points. Its principal forms interpret modal logic and intuitionistic logic, with different rules for evaluating their logical connectives. (ai.stanford.edu)

Historical development

Saul A. Kripke developed influential modal completeness results in 1959 and presented a systematic treatment of normal modal propositional calculi in Semantical Analysis of Modal Logic I (1963). His Semantical Analysis of Intuitionistic Logic I (1965) introduced relational models for intuitionistic predicate logic and proved completeness for that interpretation. These developments made relational structures a central tool for studying nonclassical logics. (onlinelibrary.wiley.com)

Frames, models, and modal truth

A Kripke frame is a pair

F=(W,R),

where $W$ is a nonempty set and $R\subseteq W\times W$ is a binary relation, called the accessibility relation. The notation $wRv$ means that $v$ is accessible from $w$ . A Kripke model adds a valuation:

M=(W,R,V).

For every propositional letter $p$ , $V(p)\subseteq W$ specifies the points where $p$ is true. (filosoficas.unam.mx)

The satisfaction notation $M,w\models\varphi$ means that $\varphi$ is true at $w$ in $M$ . In classical modal logic, the connectives of propositional logic retain their ordinary local meanings:

\begin{aligned} M,w\models p &\iff w\in V(p),\\ M,w\models\neg\varphi &\iff M,w\not\models\varphi,\\ M,w\models\varphi\land\psi &\iff M,w\models\varphi\text{ and }M,w\models\psi. \end{aligned}

Necessity and possibility receive relational clauses:

\begin{aligned} M,w\models\Box\varphi &\iff \forall v\,(wRv\Rightarrow M,v\models\varphi),\\ M,w\models\Diamond\varphi &\iff \exists v\,(wRv\land M,v\models\varphi). \end{aligned}

Thus $\Box\varphi$ concerns every accessible point, whereas $\Diamond\varphi$ concerns at least one. They are dual: $\Diamond\varphi$ is equivalent to $\neg\Box\neg\varphi$ . (filosoficas.unam.mx)

For example, let $w$ access exactly $u$ and $v$ , with $p$ true at $u$ but false at $v$ . The clauses give

M,w\models\Diamond p, \qquad M,w\not\models\Box p.

The value of $p$ at $w$ itself is irrelevant unless $wRw$ . At a point with no accessible successors, every box formula is vacuously true and every diamond formula is false. These are direct consequences of the universal and existential clauses.

Validity and frame correspondence

Validity involves several distinct levels. A formula is valid in a model if it holds at every point; it is valid on a frame if it holds at every point under every valuation. Validity over a class of frames requires validity on every frame in that class. Consequently, checking one valuation cannot establish frame validity. (ai.stanford.edu)

Modal axiom schemata often correspond exactly to structural conditions on accessibility:

Schema	Formula	Corresponding frame condition
T	$\Box p\to p$	Reflexivity: $wRw$
D	$\Box p\to\Diamond p$	Seriality: every point has a successor
4	$\Box p\to\Box\Box p$	Transitivity: $wRv\land vRu\Rightarrow wRu$
B	$p\to\Box\Diamond p$	Symmetry: $wRv\Rightarrow vRw$
5	$\Diamond p\to\Box\Diamond p$	Right Euclideanness: $wRv\land wRu\Rightarrow vRu$

These correspondences quantify over all valuations, not merely the valuation of a particular model. (ai.stanford.edu)

For instance, reflexivity guarantees T because $w$ is among its own accessible points. Conversely, if $wRw$ fails, assign $p$ to all successors of $w$ but not to $w$ . Then $\Box p$ holds at $w$ while $p$ does not, refuting T.

Soundness and completeness

A deductive system is sound for a frame class when every theorem is valid there; it is complete when every formula valid there is a theorem. Standard examples include T over reflexive frames, S4 over reflexive transitive frames, and S5 over frames whose accessibility relation is an equivalence relation. (filosoficas.unam.mx)

Completeness is not automatic. Some normal modal logics are Kripke incomplete: no class of ordinary Kripke frames has exactly their theorems as its valid formulas. Such failures concern the match between a proof system and ordinary frame semantics, rather than an inability to evaluate formulas in relational models. (arxiv.org)

Intuitionistic forcing

Intuitionistic models usually employ a partially ordered set $(W,\leq)$ , interpreted as stages of increasing information. Atomic valuations are persistent:

w\leq v,\quad w\Vdash p \quad\Rightarrow\quad v\Vdash p.

Here $\Vdash$ denotes forcing. Conjunction and disjunction are evaluated locally, but implication considers all extensions:

w\Vdash\varphi\to\psi \iff \forall v\geq w\, (v\Vdash\varphi\Rightarrow v\Vdash\psi).

No point forces falsity $\bot$ , and negation is defined by $\neg\varphi=\varphi\to\bot$ . Thus

w\Vdash\neg\varphi \iff \text{no }v\geq w\text{ forces }\varphi.

Persistence extends from atoms to every formula. Crucially, not forcing a proposition differs from forcing its negation. (princeton.edu)

For a concrete countermodel to the law of excluded middle, take two points $w<v$ , with $p$ forced only at $v$ . At $w$ , neither $p$ nor $\neg p$ is forced: $p$ is not yet established, but the extension $v$ establishes it. Therefore

w\not\Vdash p\lor\neg p.

The model represents incomplete information, not a contradiction.

For intuitionistic first-order logic, points additionally carry nonempty domains $D(w)$ , with $D(w)\subseteq D(v)$ whenever $w\leq v$ . Existential forcing requires a witness in the current domain. Universal forcing ranges over every later point and every element of its domain. (princeton.edu)

Applications and limits

In computer science, Kripke structures represent state-transition systems. They commonly include initial states and a labeling function recording which atomic propositions hold at each state. Model checking evaluates specifications against these structures; temporal logics additionally describe behavior along paths, such as whether a request is eventually followed by a response. This supports formal verification, although state-space explosion and inaccurate system models remain important limitations. (cs.cmu.edu)

Accessibility need not represent physical possibility. It may encode computational transitions or alternatives relevant to an agent’s information. Accordingly, selecting a frame condition is part of selecting a mathematical model, not a universal claim about all interpretations of necessity or knowledge. (ai.stanford.edu)

A further expressive limit is captured by bisimulation: points whose atomic facts and transitions match back and forth satisfy the same basic modal formulas. Alternative frameworks, including algebraic, topological, and neighborhood semantics, provide other ways to interpret modal languages. (ai.stanford.edu)

References

Semantical Analysis of Modal Logic I Normal Modal Propositional Calculifilosoficas.unam.mx
Semantical Analysis of Intuitionistic Logic Iprinceton.edu
Modal Logic: A Semantic Perspectiveai.stanford.edu
A new version of an old modal incompleteness theoremarxiv.org
Introduction to Model Checkingcs.cmu.edu