Lemma 1.4.19. Assuming that:

$H$ a Heyting algebra
$v$ a $H$ -valuation

Then there is a Kripke model

(S, \leq, ⊩)

such that

v ⊨_{H} φ

if and only if

S ⊩ φ

, for every proposition

φ

.