Proof of the disjunction property

Question

I am trying to prove the disjunction property "if $\,\vdash\phi\lor\psi$ then $\,\vdash\phi$ or $\,\vdash\psi$" for intuitionistic propositional logic.

So far I thought about choosing two non-tautologies $\phi$ and $\psi$ with two Kripke countermodels: $$(W, R_W, f_W)~~\mbox{such that}~~\exists (w\in W)(w\not\Vdash\phi)$$ $$(V, R_V, f_V)~~\mbox{such that}~~\exists (v\in V)(v\not\Vdash\psi)$$ Then create a new Kripke model $(W\cup V\cup\{u\}, R, f)$ with $R(u,w)$ and $R(u,v)$.

My reasoning is that $w\not\Vdash\phi\implies u\not\Vdash\phi$ and $v\not\Vdash\psi\implies u\not\Vdash\psi$, and therefore $u\not\Vdash\phi\lor\psi$, which provides a countermodel for $\phi\lor\psi$ being a tautology and $\phi$ and $\psi$ not being tautologies.

Is this sufficient to be a proof? For me it's unclear whether adding a world $u$ changes which sentences $w$ forces. So if I add a world $u$, can I be certain that still $w\not\Vdash\phi$?

Answer 1

I think your proof idea is good.

For adding the world u, I think if we set f(u) = \emptyset, then it will not change the fact that w \nVdash \phi, since f has to be monotone, but since no propositional variable holds in u, everything can happen in its successor.

I think we also need to add a relation from u to all of the successors of w and v, since it should be transitive right?

I'm now trying it by myself, some other issues I ran into: - What if the domains W,V are (partly) the same? (but the valuations could be different) How do we set the valuations in the merged model? Is it an idea to merge isomorphic disjoint copies so we do not have this problem?

Answer 2

Yes, your proof works; you have only to specify that the two countermodels must have disjoint frames $\langle W_1, R_1 \rangle$ and $\langle W_2, R_2 \rangle$.

The new model will have $W = \{ w_0 \} ∪ W_1 ∪ W_2$ and the "extended" accessibility relation will be :

$xRy$ iff $x=w_0$ or $xR_1y$ or $xR_2y$.

Answer 3

\noindent \textbf{Claim:} if $\varphi \vee \psi$ is an intuitionistic tautology, then so is at least one of $\varphi$ and $\psi$.

\begin{proof} Suppose, for contradiction, that $\varphi \vee \psi$ is an intuitionistic tautology, but neither $\varphi$ nor $\psi$ is. Then, by definition, there exist Kripke models $(W_1,R_1,f_1)$, $(W_2,R_2,f_2)$ and states $w_1 \in W, w_2 \in W_2$ such that $(W_1,R_1,f_1),w_1 \nVdash \varphi$ and $(W_2,R_2,f_2),w_2 \nVdash \psi$. Now take the disjoint union of their isomorphic labeled copies. That is, consider $(W,R,f)$ with \begin{itemize} \item $W = W_1 \times {1} \cup W_2 \times {2}$, \item $R = {\langle (w,1),(v,1) \rangle | (w,v) \in R_1 } \cup {\langle (w,2),(v,2) \rangle | (w,v) \in R_2 }$, \item $f((w,i)) = f_i(w)$ for all $i \in {1,2}$ and $w \in W_i$. \end{itemize}

\noindent Furthermore, we add a common root $u$ of $(w_1,1),(w_2,2)$ to the model, so we get $(W' = W \cup \{u\},R' = R \cup \{(u,u)\} \cup \{\langle u,(v_1,1) \rangle | R(w_1,1)(v_1,1)\} \cup \\ \{\langle u,(v_2,2) \rangle | R(w_2,2)(v_2,2)\}, f')$ with $f'(w) = f(w)$ for $w \neq u$, and $f'(u)= \emptyset$. \end{proof}

\noindent It is straightforward to check that $(W',R',f')$ is still an intuitionistic Kripke model. $R$ is clearly still reflexive and transitive, and by adding $u$, we also added a reflexive arrow and all the transitive arrows to the successors of $(w_1,1)$ and $(w_2,2)$. Furthermore, monotonicity of $f$ still holds since $f(u) = \emptyset$. Thus, if $u R' (v,i)$, then we must have that $f(u) \subseteq f((v,i))$. Finally, since the successors of $w_1$, $w_2$ are unchanged, we have $(w,1) \nVdash \varphi$ and $(w,2) \nVdash \psi$.

\vspace{0.3cm} \noindent Then it follows that $u \nVdash \varphi$ since $Ru(w_1,1)$ and $(w_1,1) \nVdash \varphi$ and $u \nVdash \psi$ since $Ru(w_2,2)$ and $(w_2,2) \nVdash \psi$. But then we have $u \nVdash \varphi \vee \psi$, which contradicts our assumption that $\varphi \vee \psi$ is an intuitionistic tautology.