Kripke Semantics

Definition

Kripke semantics provides a model-theoretic interpretation of intuitionistic logic using ordered “worlds” representing states of knowledge or constructive phases. Unlike classical models which assign static truth values, Kripke models assign truth relative to an information state, enforcing monotonicity.

Structure

A Kripke frame is a tuple $F = (W, \leq)$ where:

$W$ is a non-empty set of worlds (or nodes, states).
$\leq$ is a preorder (reflexive and transitive) on $W$ .

A Kripke model for First-Order Logic is a tuple $M = (W, \leq, D, ⊩)$ where:

$(W, \leq)$ is a frame.
$D$ is a domain function assigning a non-empty set $D (w)$ to each $w \in W$ .
Monotonicity of Domains: $w \leq v ⟹ D (w) \subseteq D (v)$ .
$⊩$ is the forcing relation defined between worlds and atomic formulas, satisfying Persistency: $w ⊩ P (t_{1}, \dots, t_{n}) \land w \leq v ⟹ v ⊩ P (t_{1}, \dots, t_{n})$

Forcing Relation

The relation $w ⊩ ϕ$ is defined inductively. Let $a \in D (w)$ denote elements of the domain at world $w$ .

Connectives

$w ⊩ ϕ \land ψ ⟺ w ⊩ ϕ and w ⊩ ψ$
$w ⊩ ϕ \lor ψ ⟺ w ⊩ ϕ or w ⊩ ψ$
$w ⊩ ϕ \to ψ ⟺ \forall v \geq w, (v ⊩ ϕ ⟹ v ⊩ ψ)$
$w ⊩ \neg ϕ ⟺ \forall v \geq w, v \neq ⊩ ϕ$
$w \neq ⊩ ⊥$

Quantifiers

$w ⊩ \exists x . ϕ (x) ⟺ \exists d \in D (w), w ⊩ ϕ (d)$
$w ⊩ \forall x . ϕ (x) ⟺ \forall v \geq w, \forall d \in D (v), v ⊩ ϕ (d)$

Note on Universal Quantification

The clause for $\forall$ must quantify over future worlds and future domains. This ensures that $\forall x . ϕ (x)$ implies that $ϕ$ holds for all objects constructed now and all objects that may be constructed later.

Properties

Monotonicity (Persistency)

For any formula $ϕ$ (not just atomic), if $w ⊩ ϕ$ and $w \leq v$ , then $v ⊩ ϕ$ . This reflects the constructive principle that established truth is not lost as knowledge grows.

Soundness and Completeness

Intuitionistic logic is sound and complete with respect to Kripke semantics.

$Γ ⊢_{I} ϕ ⟺ Γ ⊨_{Kr i p k e} ϕ$ .
Strong Completeness: Requires the Prime Ideal Theorem (weaker than full AC).

The Law of Excluded Middle

LEM ( $A \lor \neg A$ ) fails in Kripke semantics because it requires $w ⊩ A$ or $w ⊩ \neg A$ at the current world.

Counter-model: Let $W = {w_{0}, w_{1}}$ with $w_{0} \leq w_{1}$ . Let $w_{1} ⊩ A$ but $w_{0} \neq ⊩ A$ .
$w_{0} \neq ⊩ A$ (by definition).
$w_{0} \neq ⊩ \neg A$ because there exists a future world ( $w_{1}$ ) where $A$ holds.
Therefore, $w_{0} \neq ⊩ A \lor \neg A$ .

Relation to Other Semantics

Algebraic: The set of upper-closed subsets of $W$ forms a Heyting Algebra.
Beth Semantics: A generalization where truth is determined by “bars” (covering sets of chains), useful for proving properties of choice sequences.
Topological Semantics: Kripke frames correspond to topological spaces where the open sets are the upper-closed sets (Alexandrov topology).

Quartz 4

Explorer