A Kripke frame is a set of possible worlds together with an accessibility relation. The relation specifies which worlds must be considered when evaluating a logical formula. A Kripke model adds an interpretation of the propositional variables at each world.
For propositional intuitionistic logic, a Kripke frame is a partially ordered set 
. If a propositional variable
is true at 
and 
, it must remain true at 
. Writing 
to mean that 
is true at 
, the rule for implication is
 |
Conjunction and disjunction are evaluated at the current world, while falsity is true at no world. Negation
of 
means implication
from 
to falsity. A formula
is valid on a Kripke frame if it is true at every world under every permissible interpretation
(Moschovakis 2022).
For example, let 
with 
,
and let a propositional variable 
become true only at 
. At 
, neither 
nor its negation is true, since
holds at the accessible world 
. Consequently, 
is not valid on this Kripke frame. This illustrates
why the law of the excluded middle need
not hold in intuitionistic logic.
Medvedev logic and Skvortsov logic use Kripke frames consisting of nonempty subsets
of a set, with a world 
accessible from 
exactly when 
is a subset of 
.
