4
$\begingroup$

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]

$\endgroup$
3
  • $\begingroup$ I'm not quite following the proof as given (it would be much clearer with an indication of what proof rule each case corresponds to). But what I've usually seen proven by induction is: if $\Gamma \vdash \phi$, then there is a finite subset $\Gamma' \subseteq \Gamma$ such that $[\bigwedge_{\psi \in \Gamma'} i(\psi)] \le i(\phi)$. So then, for example, the step for $\rightarrow I$ just reduces to the adjunction property $p \le (q \rightarrow r)$ if and only if $(p \wedge q) \le r$. And the statement $\Gamma \vdash \phi \implies \Gamma \models \phi$ falls out as a corollary. $\endgroup$ Feb 6, 2020 at 20:50
  • $\begingroup$ Now that I think about it, I guess another approach would be: first show that for $x \in \mathcal{H}$, there exists another Heyting algebra $\mathcal{H}'$ and a Heyting algebra homomorphism $\Phi : \mathcal{H} \to \mathcal{H}'$ such that $\Phi^{-1}(\{ 1 \}) = \{ y \in \mathcal{H} \mid x \le y \}$. Then, applying this with $v(x)$ in place of $x$, if $\mathcal{H}, v \models \Gamma$, then $\mathcal{H}', \Phi \circ v \models \Gamma \cup \{ x \}$ so by induction $\Phi \circ v(p) = 1$, so $v(x) \le v(p)$, so $v(x \rightarrow p) = 1$. $\endgroup$ Feb 7, 2020 at 1:55
  • $\begingroup$ And then for ${\vee}E$, you could reuse the same proof to show $v(x) \le v(\phi)$, $v(y) \le v(\phi)$, so $v(x) \vee v(y) \le v(\phi)$. $\endgroup$ Feb 7, 2020 at 1:58

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.