Editing Kripke semantics (section)

===Intuitionistic first-order logic===

Let ''L'' be a [[first-order logic|first-order]] language. A Kripke
model of ''L'' is a triple
<math>\langle W,\le,\{M_w\}_{w\in W}\rangle</math>, where
<math>\langle W,\le\rangle</math> is an intuitionistic Kripke frame, ''M<sub>w</sub>'' is a
(classical) ''L''-structure for each node ''w''&nbsp;∈&nbsp;''W'', and
the following compatibility conditions hold whenever ''u''&nbsp;≤&nbsp;''v'':
* the domain of ''M<sub>u</sub>'' is included in the domain of ''M<sub>v</sub>'',
* realizations of function symbols in ''M<sub>u</sub>'' and ''M<sub>v</sub>'' agree on elements of ''M<sub>u</sub>'',
* for each ''n''-ary predicate ''P'' and elements ''a''<sub>1</sub>,...,''a<sub>n</sub>''&nbsp;∈&nbsp;''M<sub>u</sub>'': if ''P''(''a''<sub>1</sub>,...,''a<sub>n</sub>'') holds in ''M<sub>u</sub>'', then it holds in ''M<sub>v</sub>''.
Given an evaluation ''e'' of variables by elements of ''M<sub>w</sub>'', we
define the satisfaction relation <math>w\Vdash A[e]</math>:
* <math>w\Vdash P(t_1,\dots,t_n)[e]</math> if and only if <math>P(t_1[e],\dots,t_n[e])</math> holds in ''M<sub>w</sub>'',
* <math>w\Vdash(A\land B)[e]</math> if and only if <math>w\Vdash A[e]</math> and <math>w\Vdash B[e]</math>,
* <math>w\Vdash(A\lor B)[e]</math> if and only if <math>w\Vdash A[e]</math> or <math>w\Vdash B[e]</math>,
* <math>w\Vdash(A\to B)[e]</math> if and only if for all <math>u\ge w</math>, <math>u\Vdash A[e]</math> implies <math>u\Vdash B[e]</math>,
* not <math>w\Vdash\bot[e]</math>,
* <math>w\Vdash(\exists x\,A)[e]</math> if and only if there exists an <math>a\in M_w</math> such that <math>w\Vdash A[e(x\to a)]</math>,
* <math>w\Vdash(\forall x\,A)[e]</math> if and only if for every <math>u\ge w</math> and every <math>a\in M_u</math> , <math>u\Vdash A[e(x\to a)]</math>.
Here ''e''(''x''→''a'') is the evaluation which gives ''x'' the
value ''a'', and otherwise agrees with ''e''.{{refn|See a slightly different formalization in {{harvtxt|Moschovakis|2022}}}}