# Proof of the disjunction property

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$?

• Your proof works; you have only to specify that the two countermodels must have disjoint frames $W_1$ and $W_2$. The new model will have $W= \{ w_0 \} \cup W_1 \cup W_2$ and the "extended" accessibility relation will be : $xRy$ iff $x=w_0$ or $xR_1y$ or $xR_2y$. Nov 6, 2016 at 16:38

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?

• Yes, I think I get it now. As for the problem with a potential overlap between $W$ and $V$, I think using copies of the worlds would work. For example by using $W'\cup V'\cup \{u\}$, where $W'=W\times \{0\}$ and $V'=V\times\{1\}$, then $W'$ and $V'$ are disjoint, and we can define $R$ and $f$ appropriately
– Kaj
Nov 6, 2016 at 19:44

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$.

• I suppose I can make sure the two frames are disjoint using $W_1'\cup W_2'\cup \{w_0\}$, where $W_1'=W_1\times \{1\}$ and $W_2'=W_2\times\{2\}$, then $W_1'$ and $W_2'$ are disjoint, and we can define $R$ and $f$ appropriately
– Kaj
Nov 6, 2016 at 19:46

\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.

• Thanks, but this is more or less a more worked out version of what I had already described, and didn't really answer the doubt I had... Also, why do you use latex markup for anything other than the formulas? That doesn't work on stackexchange
– Kaj
Nov 6, 2016 at 19:39