I'm having issues proving that ((p ∨ q) → r) → (p → (q ∨ r)) is valid by means of a semantic tableau.
I know it is valid because I was able to prove it using the following Truth Table:
As far as I know, a semantic tableau is a test for satisfiability. And a formula is valid iff its negation unsatisfiable. Therefore I will need build a semantic tableau using the negation of the formula and prove that negation of the formula to be unsatisfiable, thus making the formula valid.
So this was my attempt to construct a semantic tableau for the formula:
My problem is, there is only one closed branch for this semantic tableau that I've constructed. And as far as I know, all branches need to be closed in order for that negation formula to be invalid.
Any idea where I've gone astray?
Best Answer
The error is when you pass from the second to the third line: from \begin{align} (p \lor q) \to r, \ \lnot (p \to (q \lor r)) \end{align} you can't derive (as you wrote) \begin{align} (p \lor q) \to r, \ p \to \lnot(q\lor r) \end{align} but you can derive \begin{align}\tag{1} (p \lor q) \to r, \ p, \ \lnot(q\lor r) \end{align}
Developing the tableau from $(1)$ leads to close all branches, as expected.
Remember that, as a general rule in a tableau, a formula of the form $\lnot (A \to B)$ decomposes into $A, \ \lnot B$.