Let $\tau$ be a closed tableau. Prove that $\tau$ is not satisfiable.

341 Views Asked by At

Let $\tau$ be a closed tableau. Prove that $\tau$ is not satisfiable.

Okay can prove this by contradiction.

So we say that a tableau $\tau$ is $\textit{satisfiable}$ iff there exists an interpretation $\nu$ and a branch $B \in \tau$, such that for any formula $\phi \in B$, it is the case that $\nu(\phi)=1$

Now suppose $\phi \rightarrow \psi$ is on a branch $B$. I f we apply a rule to it, then two branches eventuate, $\neg \phi$ and $\psi$. The definition above says that $\nu$ makes every formula on $B$ true. Hence $\nu(\phi \rightarrow \psi)=1$ So $\tau$ is satisfied and is a open tableau. It is open because there is a open branch.

Does this prove that $\tau$ is not satisfiable because it is closed tableau.

Am I correct?

1

There are 1 best solutions below

4
On

This is absolutely standard bookwork and is proved in any good textbook which does logic-by-trees.

You've tagged the question "propositional logic" so I'm assuming that you want to prove the theorem for propositional tableaux (rather than for tableaux in quantificational logic).

The standard route is to prove the contrapositive -- i.e. prove that if $\tau$ IS satisfiable, then it has an open branch.

So assume the wffs at the top of the tableau are satisfiable together (i.e. there is a valuation which makes them all true). Prove that every time you apply one of the tree-building rules then all the wffs on at least branch remain satisfiable. And then note that satisfiable branches can't contain both $P$ and $\neg P$ and hence must stay open. So the tree stays open.

OK, that's the headline news. You'll find a full-dress proof carefully done in Ch. 19 of my Introduction to Formal Logic (CUP, 2003 and man y reprints).