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}$.