Proving $\Gamma \vdash \phi$ Implies $\Gamma \vDash \phi$ (for Institutionistic propositional logic and Heying algebras)

Question

I'm trying to prove that $\Gamma \vdash \phi$ implies $\Gamma \vDash \phi$ (for Institutionistic propositional logic and Heying algebras), by induction with respect to natural deduction proofs of Intuitionistic propositional logic, as instructed in the book I'm learning from - "Lectures on the Curry-Howard Isomorphism" - 1998 version (https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf). I should note that I'm not sure if Heyting algebras are defined in the same way as the standard literature, as it seems like it's a bit different from the formal definition in the Wikipedia page on Heyting algebra, so I would just say that the definition I'm working from is definition 2.4.1 in page 31 in the book mentioned above. Other definitions I use in the proof are definition 2.2.4 in page 26, definition 2.4.4 in page 32 and definition 2.4.5 in page 32.

So I have an incomplete proof, that I would like to know how I should complete, and weather there is any problem with it.

The Proof: Before we proceed to the induction proof it's useful to prove the following: since $a \leq 1$, for all $a \in H$, $a \cup 1 = 1$. In addition, $a \cap 1 = a$, therefore $1 \leq a \Rightarrow a$, hence $a \Rightarrow a = 1$ which implies $a \cap b \leq a$, for all $b \in H$. Now for the induction, first suppose that $\phi$ is an axiom of $\Gamma$, hence $\phi \in \Gamma$. Then given $\mathcal{H}$ and $v$, suppose $\mathcal{H}, v \vDash \Gamma$. Since $\phi \in \Gamma$, we get $\mathcal{H}, v \vDash \phi$ and thus $\Gamma \vDash \phi$. If $\phi$ is not an axiom of $\Gamma$, assume the sons of $\Gamma \vdash \phi$, p osses the desired property (we view natural deduction proofs of intuitionistic logic as trees with the conclusion as root). Then the sons are of one of the following forms:

1. $\Gamma \vdash p$ $\Gamma \vdash q$ ;
2. $\Gamma \vdash p$ ;
3. $\Delta \vdash p$, with $\Gamma \subseteq \Delta$ ;
4. $\Delta \vdash p$ $K \vdash q$ $\Gamma \vdash r$, with $\Gamma \subseteq \Delta, K$ .

Given $\mathcal{H}$ and $v$, suppose $\mathcal{H}, v \vDash \Gamma$, and we examine each case:

1. We have $v(p) = 1$ and $v(q) = 1$. If $\phi = p \wedge q$, then $v(\phi) = v(p \wedge q) = v(p) \cap v(q) = 1$. If $p = q \rightarrow \phi$, then $1 = v(p) = v(q \rightarrow \phi) = v(q) \Rightarrow v(\phi) = 1 \Rightarrow v(\phi)$, hence $v(\phi) = 1 \cup v(\phi) = 1$.
2. We have $v(p) = 1$. If $p = \bot$, then $v(p) = 0$, therefore $0=1$, thus $t = 1$ for all $t \in H$, and in particular $v(\phi) = 1$. If $\phi = p \vee \psi$, then $v(\phi) = v(p \vee \psi) = v(p) \cup v(\psi) = 1 \cup v(\psi) =1$. If $p = \phi \wedge \psi$, then $1 = v(p) = v(\phi) \cap v(\psi) \leq v(\phi)$, hence $v(\phi) = 1$.
3. We have $\Gamma \cup \{x\} \vDash p$, where $\phi = x \rightarrow p$. Therefore, if $\mathcal{H}, v \vDash \Gamma \cup \{x\}$, that is $v(x) = 1$ and for every $t \in \Gamma$, $v(t) = 1$, then $\mathcal{H}, v \vDash p$, that is $v(p) = 1$. Thus, $v(\phi) = v(x \rightarrow p) = v(x) \Rightarrow v(p)$. If $v(x) = 1$, then $v(\phi) = 1 \Rightarrow 1 = 1$. If $v(\phi) \neq 1$, then $\dots$ [Need help to complete]

4. We have $\Gamma \cup \{x\} \vDash \phi$, $\Gamma \cup \{y\} \vDash \phi$ and $\Gamma \vDash x \vee y$, i.e.:

   • If $\mathcal{H}, v \vDash \Gamma \cup \{x\}$, that is $v(x) = 1$ and $\mathcal{H}, v \vDash \Gamma$, then $\mathcal{H}, v \vDash \phi$, that is $v(\phi) = 1$.
   • If $\mathcal{H}, v \vDash \Gamma \cup \{y\}$, that is $v(y) = 1$ and $\mathcal{H}, v \vDash \Gamma$, then $\mathcal{H}, v \vDash \phi$, that is $v(\phi) = 1$.
   • If $\mathcal{H}, v \vDash \Gamma$, then $\mathcal{H}, v \vDash x \vee y$, that is $v(x \vee y) = 1$.

   So we got $v(x \vee y) = v(x) \cup v(y) = 1$, and we need to show that either $v(x) = 1$ or $v(y) = 1$ to obtain the desired result. $\dots$ [Need help to complete]

Answer 1

As far as I know, to complete the inductive steps for ${\rightarrow}I$ and ${\vee}E$, you will need to strengthen the statement to be proved by induction.

---

One possible strengthening is: instead of (implicitly) trying to prove $\mathcal{H}, v \models \phi$ inductively for a single fixed choice of $\mathcal{H}, v$, you can move to proving the full $\Gamma \models \phi$ inductively. In this strategy, the key observation will be:

Lemma: Let $x_0 \in \mathcal{H}$ where $\mathcal{H}$ is a Heyting algebra. Then $\mathcal{H}_{x_0} := \{ x \in \mathcal{H} \mid x \le x_0 \}$ is also a Heyting algebra. (Though be careful that it's not a sub Heyting algebra of $\mathcal{H}$ in general, since $1_{\mathcal{H}_{x_0}} = x_0$ and $(x \Rightarrow_{\mathcal{H}_{x_0}} y) = (x \Rightarrow_{\mathcal{H}} y) \cap_{\mathcal{H}} x_0$ are not inherited from $\mathcal{H}$.) Furthermore, $x_0 \cap - : \mathcal{H} \to \mathcal{H}_{x_0}$ is a morphism of Heyting algebras.

Now, in the inductive step for ${\rightarrow}I$, you are given that $\Gamma \cup \{ x \} \models \phi$ and you want to conclude that $\Gamma \models (x \rightarrow \phi)$. Thus, suppose we have $\mathcal{H}, v \models \Gamma$, i.e. $v(\psi) = 1_{\mathcal{H}}$ for all $\psi \in \Gamma$. Then you may check that $\mathcal{H}_{v(x)}, (\psi \mapsto v(x) \cap v(\psi)) \models \Gamma \cup \{ x \}$, so applying the inductive hypothesis, we get that $v(x) \cap v(\phi) = 1_{\mathcal{H}_{v(x)}} = v(x)$, implying that $v(x) \le v(\phi)$, implying that $v(x \rightarrow \phi) = (v(x) \Rightarrow v(\phi)) = 1_{\mathcal{H}}$.

Similarly, in the inductive step for ${\vee} E$, suppose we are given that $\Gamma \models x \vee y$, $\Gamma \cup \{ x \} \models \phi$, $\Gamma \cup \{ y \} \models \phi$. Thus, suppose we have $\mathcal{H}, v \models \Gamma$. Then reusing the proof from the previous paragraph, we can conclude $v(x) \le v(\phi)$ and $v(y) \le v(\phi)$. Therefore, $1 = v(x \vee y) = v(x) \cup v(y) \le v(\phi)$.

---

Another possible strengthening is: for some fixed $\mathcal{H}, v$, we prove inductively that if $\Gamma$ is finite and $\Gamma \vdash \phi$, then $\bigcap_{\psi \in \Gamma} v(\psi) \le v(\phi)$. (To show this is sufficient, use the compactness property of intuitionistic propositional logic to reduce to finite $\Gamma' \subseteq \Gamma$, and then in that case you get $\Gamma' \models \phi$ as a corollary.) Then in this proof, for example the inductive step for ${\rightarrow}I$ just reduces to an application of the adjunction property that $x \le (y \Rightarrow z)$ if and only if $x \cap y \le z$; and the inductive step for ${\vee}E$ essentially boils down to an application of the fact that a Heyting algebra is distributive.