Franklin's Notes

Kripke semantics

Kripke semantics provides a way of formalizing the idea of "knowledge through time". A partially ordered set $\mathbf{P}$, sometimes called a frame in this context, can be used to model different "timelines", with $a\leq b$ representing the idea that $a$ is a moment in time ocurring before $b$ along some timeline. A set $A\subset\mathbf P$ is called hereditary if it is "closed upwards", i.e. if it contains all points ocurring later than each of its points. A valuation $V:\Phi_0\to 2^{\mathbf P}$ is a function assigning to each sentence symbols in a set of symbols some subset of the frame, with $V(\varphi)$ representing the set of moments in time at which $\varphi$ is true. This intuition provides the motivation for the following restriction placed on the valuation $V$:

For all sentences $\varphi$, the subset $V(\varphi)\subset \mathbf{P}$ must be hereditary. That is, if $\varphi$ is true at some moment in time, then it is also true at all future moments.

The hereditary subsets of $\mathbf P$ comprise a Heyting algebra , which is denoted $\mathbf{P}^+$. The above requirement formalizes the constructivist idea that something becomes true when it is proven to be true, and only then, going against the nonconstructivist mode of thought suggesting that mathematical truth is absolute, existing in a perfect state at all moments of time.

One a valuation $V$ is defined on a set $\Phi_0$ of sentence symbols, we can use this to define satisfaction in a model, or a pair $\mathcal M = (\mathbf{P},V)$, similarly to how this is done in first-order logic . If $\varphi$ is a sentence symbol, we write $\mathcal M\vDash_p \varphi$, or "$\mathcal M$ satisfies $\varphi$ at $p$" or "$\varphi$ is true in $\mathcal M$ at $p$", iff $p\in V(\varphi)$, that is, if $p$ is among the moments in time at which $\varphi$ is present. Having defined satisfaction for sentence symbols, we may now define satisfaction for logical combinations as follows:

1. $\mathcal M\vDash_p \varphi \land \psi$ iff $\mathcal M\vDash_p\varphi$ and $\mathcal M\vDash_p \psi$
2. $\mathcal M\vDash_p \varphi \lor \psi$ iff $\mathcal M\vDash_p\varphi$ or $\mathcal M\vDash_p \psi$
3. $\mathcal M\vDash_p \neg\varphi$ iff $\mathcal M \not\vDash_q\varphi$ for all $q\geq p$
4. $\mathcal M\vDash_p \varphi\to\psi$ if for all $q$ with $q\geq p$, we have $\mathcal M\vDash_q \psi$ whenever $\mathcal M\vDash_q \varphi$

Notice that the interpretations of $\land$ and $\lor$ operate elementwise along moments in time, but the interpretations of $\neg$ and $\to$ produce expressions depending not only on a single moment in time, but also all future moments in time. The natural way to interpret $\neg\varphi$ is "$\varphi$ is not true now, nor can it ever be found to be true" and the way to interpret $\varphi\to\psi$ is "as soon as $\varphi$ is true, $\psi$ will become true as well".

Finally, if $\mathcal M\vDash_p\varphi$ for all $p$ in the frame, we may simply write $\mathcal M\vDash\varphi$, and write that "$\varphi$ is true in $\mathcal M$". Finally, if $\varphi$ is true in $\mathcal M$ for all models $\mathcal M$ based on the frame $\mathbf{P}$, we write $\mathbf{P}\vDash\varphi$ and say that $\varphi$ is valid in the frame $\mathbf{P}$.




back to home page