Is Resolution Intuitionistically Valid?

58 Views Asked by At

Specifically, is it intuitionistically valid to deduce $Q$ from $P\vee Q$ and $\neg P\vee Q$? The proof I could come up with uses the law of exclusive middle, and I feel that you can probably come up with a clever construction using this resolution principle to deduce LEM, but I haven't been able to do so.

1

There are 1 best solutions below

2
On BEST ANSWER

Given $A \lor B$, if you can prove $C$ from both $A$ and $B$, you can conclude that $C$ is true.

Applying that to our situation, if we can prove $Q$ in all four cases of $P$ and $\neg P$, $P$ and $Q$, $Q$ and $\neg P$, and $Q$ and $Q$, then we can conclude $Q$. The case of $P$ and $\neg P$ can't happen (or alternatively, you can conclude $Q$ from explosion). The remaining cases have $Q$ as a premise, so $Q$ follows.