1
$\begingroup$

I'm trying to understand the chapter (13) on algebraic semantics for intuitionistic predictate logic in Constructivism in Mathematics by Troelstra and van Dalen and I'm having trouble verifying soundness.

The models we are discussing are so-called $\Omega$-models which take truth values in some complete Heyting algebra $\Omega$.

Proving soundness can be, according to the authors, done in a routine way. If I'm correct that means by induction on the structure of derivations. If the final rule application of a derivation is of the form

$$ \begin{align} \Gamma_1 \vdash A_1, \ldots, \Gamma_n \vdash A_n \\ \hline \Gamma \vdash A \end{align} $$ then our induction hypothesis is: in each $\Omega$-model we have that if for some $i$ it holds that $[\![B]\!] = \top$ for all $B \in \Gamma_i$, then $[\![A_i]\!] = \top$.

Now consider for instance the case of disjunction elimination. We have a derivation of the form $$ \begin{align} \Gamma_1 \vdash A \lor B & & \Gamma_2, A \vdash C & & \Gamma_3, B \vdash C \\ \hline \Gamma_1 \cup \Gamma_2 \cup \Gamma_3 \vdash C \end{align} $$ Now suppose that in some $\Omega$-model we have that for each sentence $B$ in $\Gamma_1 \cup \Gamma_2 \cup \Gamma_3$, it holds that $[\![B]\!] = \top$. Then by the induction hypothesis we have $[\![A \lor B]\!] = [\![A]\!] \lor [\![B]\!]= \top$. The result would follow easily if that would imply that in the same model we have either $[\![A]\!] = \top$ or $[\![B]\!] = \top$, but I don't think that holds for every complete Heyting algebra. Because of this I don't know how to proceed.

I feel like my trouble is caused by some fundamental misunderstanding of either $\Omega$-models or Heyting algebra's, but I don't know exactly what I'm missing.

Could anybody point me in the right direction? If more definitions or explanation is needed I'd be happy to provide it.

$\endgroup$

1 Answer 1

1
$\begingroup$

If $\Gamma = A_1,\ldots,A_n$, then define $[\![ \Gamma ]\!]$ to be $[\![ A_1 ]\!] \wedge \ldots \wedge [\![ A_n ]\!]$, and in particular take the empty sequent to $\top$. Then show that if $\Gamma \vdash A$, then $[\![ \Gamma ]\!] \leq [\![A ]\!]$. This can be done by induction on derivation. Once you've done that you can deduce that if $\Gamma \vdash A$ and $[\![ \Gamma ]\!] = \top$ then $[\![ A ]\!] = \top$, but as you've noticed this is too weak to do directly by induction. Eg for a non trivial topological space $T$ there will be open sets $U$ and $V$ such that $U \cup V = T$ but $U \neq T$ and $V \neq T$.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .