I have been reading Raymond Smullyan's wonderful book titled Logical Labyrinths. I'm having trouble understanding the completeness proof of the Tableaux method. 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 the branch?
Because every branch is a conjunction (atleast in my understanding), is it fair to say that a completed tableaux expresses a sentence X in a disjunctive normal form?
Any pointers would be very helpful. Thanks a lot.
