Issue proving that a formula is valid using semantic tableau

Question

I have to prove that a formula in propositional logic is valid. I created a truth table which shows that the formula is valid (a tautology); however I am doing something wrong when trying to prove this using a semantic tableau by creating a semantic tableau of the formula's complement. All leaf nodes should be closed with X as a result of a complementary pair of atoms, but in my attempt all leaf nodes are open as there are no complementary pairs of atoms in any leaf nodes... Any idea what I'm doing wrong here?

My semantic tableau:

https://imgur.com/a/4P2OQbc

The alpha and beta rules I used to construct this semantic tableau:

https://imgur.com/a/tMdTjfi

Answer 1

The $\alpha$ rules are different from the $\beta$ rules. For the $\alpha$ rules, you create a new branch for each of $\alpha_1$ and $\alpha_2$. But for the $\beta$ rules, you don't branch. Rather, you put both $\beta_1$ and $\beta_2$ in the same branch.

If you think about the rules conceptually, and what you are trying to do with this tableaux method this should all makes sense. That is, in general, in a semantic tableaux method you exolore all possible options to make some statement true. Thus, for example, there are two ways to make a statement like $P \lor Q$ true: either $P$ is true, or $Q$ is true. Hence, you create a branch for each of those ways. n the other hand, there is only one way to make $\neg (P \lor Q)$ true, and that is by setting both $p$ and $Q$ to false. This is why you get both $\neg P$ and $\neg Q$ still in the same branch.

Below is a pic of the tree as it should look like:

Answer 2

You are using the rules in the wrong way.

$\lnot (A \to B)$ is TRUE exactly when $(A \to B)$ is FALSE.

And $(A \to B)$ is FALSE exactly when $A$ is TRUE and $B$ is FALSE, i.e. $\lnot B$ is TRUE.

Thus, the rule for $\lnot (A \to B)$ is :

on the same path add $A$ and $\lnot B$; you have not to branch.

See e.g. : Raymond Smullyan, First-order Logic (1961) and similar example in Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer (3rd ed 2012), page 53.