Propositional logic problem : Tableau calculus

Question

Let there four buttons: A, B, C and D. You win by pressing the correct button. It is known that if button A is pressed then button B must be pressed, too. If button C is pressed then button D must be pressed, too. If button D is pressed then either button A or button B (or both) must be pressed, too. Moreover, pressing neither button A nor button B leads to immediate loss of your game.

So how do i translate the situation above into a formula in propositional logic?

Also how do i apply the tableau calculus so i can see if the formula is satisfiable?

Answer 1

This puzzle is a little unclear ... can't you just press all buttons to win? That would be too easy ... so I suppose they want you to press just one button. OK, but what if, say, $C$ is the correct button? Then by the rules, I would have to press $D$ as well, and I end up pressing more than one button after all. So, I suppose that for that very reason, $C$ is not to be the 'correct' button. That is, I interpret this puzzle as: find the correct button, where the 'correct' button is the button that you are able to press all by itself.

OK, so let's use:

$W$: you can win

$A$: you press $A$

$B$: you press $B$

$C$: you press $C$

$D$: you press $D$

Since you can win iff you can press exactly one button, we have:

$W \leftrightarrow [(A \land \neg B \land \neg C \land \neg D) \lor (\neg A \land B \land \neg C \land \neg D) \lor (\neg A \land \neg B \land C \land \neg D) \lor (\neg A \land \neg B \land \neg C \land D)] $

We also have:

$A \to B$

$C \to D$

$D \to (A \lor B)$

$\neg (A \lor B) \to \neg W$

Now, to use a tree to see if there is a way to win this game (and what the correct button is), you put all these statement in the root of the tree, together with the assumption $W$. Note that the $W$ combined with the one big biconditional will quickly lead to $4$ branches corresponding to each of the disjuncts of the RHS of the biconditional, and thus to the pressing of exactly one button. And then, if there is indeed a way to win the game, one of the branches will get finished, but will not close, and from that branch you can immediately tell what the 'correct' button is. Branches that correspond to the pressing of a button that in fact cannot be pressed by itself will all close. If it turns out that all branches close, then you cannot win this game.