[proofplan]
We prove the stronger soundness statement with assumptions: if a finite context $\Gamma$ derives $A$, then the meet of the values of all formulas in $\Gamma$ lies below $v(A)$. This is proved by induction on a standard natural-deduction derivation for intuitionistic propositional logic. Each inference rule is checked against the corresponding order-theoretic property of a Heyting algebra: meets model conjunction, joins model disjunction, $0$ models absurdity, and the adjunction $x \wedge a \leq b$ iff $x \leq a \to b$ models implication. Applying the stronger statement to the empty context gives $1 \leq v(A)$, hence $v(A) = 1$.
[/proofplan]
[step:Reduce closed soundness to soundness with finite assumptions]
We use a standard natural-deduction presentation of intuitionistic propositional logic for the connectives $\bot$, $\wedge$, $\vee$, and $\to$, with finite contexts and the usual structural rules of weakening, contraction, and exchange.
Let $\Gamma = (G_1,\dots,G_m)$ be a finite context of formulas. Define its semantic value under $v$ to be the element $M_v(\Gamma) \in H$ given by
\begin{align*}
M_v(\Gamma) = v(G_1) \wedge \cdots \wedge v(G_m)
\end{align*}
when $m \geq 1$, and by
\begin{align*}
M_v(\varnothing) = 1
\end{align*}
when $\Gamma$ is empty. We prove the following stronger assertion:
[claim:Context soundness]
For every finite context $\Gamma$ and every formula $A$, if $\Gamma \vdash A$ in intuitionistic propositional logic, then
\begin{align*}
M_v(\Gamma) \leq v(A).
\end{align*}
[/claim]
[proof]
The proof is by induction on the last inference in a derivation of $\Gamma \vdash A$. The induction hypothesis is that the displayed inequality holds for all immediate subderivations of the last inference.
[/proof]
Once the claim is proved, the theorem follows immediately. If $\vdash A$, then the claim applied to $\Gamma = \varnothing$ gives
\begin{align*}
1 = M_v(\varnothing) \leq v(A).
\end{align*}
Since $1$ is the greatest element of $H$, we also have $v(A) \leq 1$. By antisymmetry of the order on $H$, $v(A)=1$.
[/step]
[step:Verify assumptions and structural rules]
First suppose the last inference is an assumption, so $A$ occurs in $\Gamma$. Since $M_v(\Gamma)$ is the meet of the values of all formulas in $\Gamma$, the universal property of finite meets gives
\begin{align*}
M_v(\Gamma) \leq v(A).
\end{align*}
For weakening, suppose a subderivation proves $\Gamma \vdash A$ and the last step concludes $\Gamma,B \vdash A$ for some formula $B$. By the induction hypothesis,
\begin{align*}
M_v(\Gamma) \leq v(A).
\end{align*}
The meet defining $M_v(\Gamma,B)$ satisfies
\begin{align*}
M_v(\Gamma,B) \leq M_v(\Gamma).
\end{align*}
Transitivity gives
\begin{align*}
M_v(\Gamma,B) \leq v(A).
\end{align*}
Exchange and contraction do not change the meet value, because meet is commutative, associative, and idempotent. Hence those structural rules preserve the desired inequality.
[guided]
We first check the rules that do not involve logical connectives. If the derivation ends by using an assumption, then the formula $A$ is one of the formulas listed in the finite context $\Gamma$. The element $M_v(\Gamma)$ is defined as the meet of the values of all assumptions in $\Gamma$. A meet is below each of its factors, so
\begin{align*}
M_v(\Gamma) \leq v(A).
\end{align*}
Now consider weakening. The premise gives a derivation of $\Gamma \vdash A$, while the conclusion allows one extra unused assumption $B$, giving $\Gamma,B \vdash A$. By the induction hypothesis applied to the premise,
\begin{align*}
M_v(\Gamma) \leq v(A).
\end{align*}
Adding an assumption corresponds semantically to taking one more meet:
\begin{align*}
M_v(\Gamma,B) = M_v(\Gamma) \wedge v(B).
\end{align*}
The meet $M_v(\Gamma) \wedge v(B)$ is below $M_v(\Gamma)$, so
\begin{align*}
M_v(\Gamma,B) \leq M_v(\Gamma).
\end{align*}
Combining the two inequalities by transitivity yields
\begin{align*}
M_v(\Gamma,B) \leq v(A).
\end{align*}
Exchange only reorders the factors in the finite meet, and contraction replaces two equal factors by one equal factor. Since meet in a lattice is commutative, associative, and idempotent, these operations leave the semantic value of the context unchanged. Therefore exchange and contraction preserve the same inequality.
[/guided]
[/step]
[step:Check conjunction rules using the universal property of meet]
For conjunction introduction, suppose the last inference has premises $\Gamma \vdash A$ and $\Gamma \vdash B$, and conclusion $\Gamma \vdash A \wedge B$. By the induction hypothesis,
\begin{align*}
M_v(\Gamma) \leq v(A)
\end{align*}
and
\begin{align*}
M_v(\Gamma) \leq v(B).
\end{align*}
By the universal property of meet,
\begin{align*}
M_v(\Gamma) \leq v(A) \wedge v(B) = v(A \wedge B).
\end{align*}
For conjunction elimination, suppose the last inference has premise $\Gamma \vdash A \wedge B$ and conclusion $\Gamma \vdash A$. By the induction hypothesis,
\begin{align*}
M_v(\Gamma) \leq v(A \wedge B) = v(A) \wedge v(B).
\end{align*}
Since $v(A) \wedge v(B) \leq v(A)$, transitivity gives
\begin{align*}
M_v(\Gamma) \leq v(A).
\end{align*}
The elimination rule concluding $B$ is identical, using $v(A) \wedge v(B) \leq v(B)$.
[/step]
[step:Check disjunction rules using the universal property of join]
For disjunction introduction, suppose the last inference has premise $\Gamma \vdash A$ and conclusion $\Gamma \vdash A \vee B$. By the induction hypothesis,
\begin{align*}
M_v(\Gamma) \leq v(A).
\end{align*}
Since $v(A) \leq v(A) \vee v(B)$, transitivity gives
\begin{align*}
M_v(\Gamma) \leq v(A) \vee v(B) = v(A \vee B).
\end{align*}
The other disjunction introduction rule is identical, using $v(B) \leq v(A) \vee v(B)$.
For [disjunction elimination](/theorems/4625), suppose the last inference has premises $\Gamma \vdash A \vee B$, $\Gamma,A \vdash C$, and $\Gamma,B \vdash C$, and conclusion $\Gamma \vdash C$. Set
\begin{align*}
m = M_v(\Gamma), \quad a = v(A), \quad b = v(B), \quad c = v(C).
\end{align*}
The induction hypothesis gives
\begin{align*}
m \leq a \vee b
\end{align*}
and
\begin{align*}
m \wedge a \leq c
\end{align*}
and
\begin{align*}
m \wedge b \leq c.
\end{align*}
Since $m \leq a \vee b$, we have
\begin{align*}
m = m \wedge (a \vee b).
\end{align*}
By distributivity in a Heyting algebra,
\begin{align*}
m \wedge (a \vee b) = (m \wedge a) \vee (m \wedge b).
\end{align*}
The two inequalities $m \wedge a \leq c$ and $m \wedge b \leq c$ imply, by the universal property of join,
\begin{align*}
(m \wedge a) \vee (m \wedge b) \leq c.
\end{align*}
Therefore
\begin{align*}
M_v(\Gamma) = m \leq c = v(C).
\end{align*}
[guided]
The disjunction elimination rule is the semantic form of proof by cases. We assume the last inference has premises $\Gamma \vdash A \vee B$, $\Gamma,A \vdash C$, and $\Gamma,B \vdash C$, and conclusion $\Gamma \vdash C$. Define the four elements of the Heyting algebra
\begin{align*}
m = M_v(\Gamma), \quad a = v(A), \quad b = v(B), \quad c = v(C).
\end{align*}
The first premise says that, under the assumptions $\Gamma$, the disjunction $A \vee B$ has been derived. By the induction hypothesis,
\begin{align*}
m \leq v(A \vee B) = a \vee b.
\end{align*}
The second premise says that $C$ follows if, in addition to $\Gamma$, we assume $A$. Semantically, adding the assumption $A$ means meeting with $a$, so the induction hypothesis gives
\begin{align*}
m \wedge a \leq c.
\end{align*}
Likewise, the third premise gives
\begin{align*}
m \wedge b \leq c.
\end{align*}
We now combine the two cases. Since $m \leq a \vee b$, meeting both sides with $m$ gives
\begin{align*}
m = m \wedge (a \vee b).
\end{align*}
A Heyting algebra is a distributive lattice, so meet distributes over join:
\begin{align*}
m \wedge (a \vee b) = (m \wedge a) \vee (m \wedge b).
\end{align*}
Each of the two joined terms lies below $c$, namely
\begin{align*}
m \wedge a \leq c
\end{align*}
and
\begin{align*}
m \wedge b \leq c.
\end{align*}
By the universal property of join, their join also lies below $c$:
\begin{align*}
(m \wedge a) \vee (m \wedge b) \leq c.
\end{align*}
Substituting the previous equalities, we obtain
\begin{align*}
M_v(\Gamma) = m \leq c = v(C).
\end{align*}
Thus disjunction elimination is sound.
[/guided]
[/step]
[step:Check implication rules using the Heyting adjunction]
For implication introduction, suppose the last inference has premise $\Gamma,A \vdash B$ and conclusion $\Gamma \vdash A \to B$. Set
\begin{align*}
m = M_v(\Gamma), \quad a = v(A), \quad b = v(B).
\end{align*}
The induction hypothesis gives
\begin{align*}
m \wedge a \leq b.
\end{align*}
By the defining Heyting adjunction,
\begin{align*}
x \wedge a \leq b \quad \text{if and only if} \quad x \leq a \to b,
\end{align*}
applied with $x=m$, we get
\begin{align*}
m \leq a \to b = v(A \to B).
\end{align*}
For implication elimination, suppose the last inference has premises $\Gamma \vdash A \to B$ and $\Gamma \vdash A$, and conclusion $\Gamma \vdash B$. Set
\begin{align*}
m = M_v(\Gamma), \quad a = v(A), \quad b = v(B).
\end{align*}
The induction hypothesis gives
\begin{align*}
m \leq a \to b
\end{align*}
and
\begin{align*}
m \leq a.
\end{align*}
Hence
\begin{align*}
m = m \wedge m \leq a \wedge (a \to b).
\end{align*}
By the Heyting adjunction applied to $x = a \to b$, the inequality
\begin{align*}
a \to b \leq a \to b
\end{align*}
implies
\begin{align*}
(a \to b) \wedge a \leq b.
\end{align*}
Commutativity of meet gives
\begin{align*}
a \wedge (a \to b) \leq b.
\end{align*}
Therefore
\begin{align*}
M_v(\Gamma) = m \leq b = v(B).
\end{align*}
[/step]
[step:Check absurdity elimination using the least element]
Suppose the last inference has premise $\Gamma \vdash \bot$ and conclusion $\Gamma \vdash A$. By the induction hypothesis,
\begin{align*}
M_v(\Gamma) \leq v(\bot) = 0.
\end{align*}
Since $0$ is the least element of $H$, we have
\begin{align*}
0 \leq v(A).
\end{align*}
By transitivity,
\begin{align*}
M_v(\Gamma) \leq v(A).
\end{align*}
This proves the context soundness claim for every inference rule. Applying the claim to a closed derivation of $A$ gives $v(A)=1$, as shown in the first step.
[/step]
