Definition 1.4.6 (Valuation in Heyting algebras). Let $H$ be a Heyting algebra and $L$ be a propositional language with a set $P$ of primitive propositions. An $H$-valuation is a function $v:P\to H$, extended to the whole of $L$ recursively by setting:

• $v(\perp )=\perp$,

• $v(A\wedge B)=v(A)\wedge v(B)$,

• $v(A\vee B)=v(A)\vee v(B)$,

• $v(A\to B)=v(A)\Rightarrow v(B)$.

A proposition $A$ is $H$-valid if $v(A)=\top$ for all $H$-valuations $v$, and is an $H$-consequence of a (finite) set of propositions $\mathrm{\Gamma }$ if $v(\wedge \mathrm{\Gamma })\le v(A)$ for all $H$-valuations $v$ (written $\mathrm{\Gamma }{\models }_{H}A$).