1

I have recently been reading Raymond Smullyan's wonderful book titled Logical Labyrinths. I'm having trouble understanding the completeness proof of the Tableaux method for Propositional Calculus. In order to show that a sentence $X$ is a tautology, we show that $F X$ results in a closed tableau, i.e., every branch of the completed tableaux is closed. Why can't we equivalently say that $X$ is a tautology if every branch of a completed tableau for $T X$ is open? Is it because different branches could assign different values to the same atom to satisfy that branch? And how do we show that any completion of the tableaux results in a closed tableaux?

Because every branch is a conjunction (atleast in my understanding), is it fair to say that a completed tableaux expresses a sentence $X$ in disjunctive normal form?

Any pointers would be very helpful. Thanks a lot.

user2374991
  • 13
  • The issue is that a closed tableaux means that the top formula is unsatisfiable and the method exploit the property that $X$ is a tautology iff $\lnot X$ is unsatisfiable. – Mauro ALLEGRANZA Oct 13 '22 at 06:46
  • To start with $X$ and prove that one or many branches are open proves that $X$ is satisfiable, not that it is a tautology. – Mauro ALLEGRANZA Oct 13 '22 at 06:48

1 Answers1

0

Your first suggestion is not true. Take an atomic sentence $P$. Set it to True. OK, that's the end of the tableaux: it's an open and finished branch. And it's the only one, so every branch in the tableaux is open and finished. But clearly $P$ is not a tautology.

But yes, there is a connection of a completed tableaux $TX$ and a DNF for that sentence $X$: you can conjunct together all the atomic statements in each branch (where you use $P$ for $TP$ and $\neg P$ for $FP$), and if you then disjunct together all those conjunctions, you get a DNF for that sentence. Not necessarily a canonical DNF, where each conjunction refers to each variable, but it is a DNF of $X$, yes.

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • Ok, thanks. I see that. But what about the other part. Is the tableaux expansion related in any way to the original formula, perhaps as its DNF or something else? – user2374991 Oct 12 '22 at 17:38
  • @user2374991 Sorry, I didn't see that second part. Just added that to my answer – Bram28 Oct 12 '22 at 17:55
  • This has been very useful to me - thanks a lot. Just to summarize my understanding then, if a tableaux is a DNF representation of formula X, then it only helps answer satisfiability. But it does not imply that X is true everywhere. For assignments not conforming to the conjunctions in the branches, X would be false.

    But when we use the tableaux for $\neg X$, and if all the branches are closed, then its DNF is false. IOW then, the formula is identically false. Which implies that X is a tautology.

     – user2374991 Oct 12 '22 at 20:10
  • @user2374991 Yes, that's all correct! :) – Bram28 Oct 14 '22 at 12:52