The tree tables are testing for satisfiability, and in this case we are testing if two formulas α and β are equivalent. The negated biconditional ¬(α ↔ β) represents a contradiction if the two formulas are equivalent, therefore all paths will close on the tree.

However, if the two formulas are equivalent, would doing a tree beginning with α and ¬β, one on top of the other, not also be a contradiction?

Why would this not work as a test for equivalence?

  • $\begingroup$ Maybe you have to start the tree with a pair of formulas that are equivalent, like e.g. $p \to q$ and $\lnot p \lor q$... $\endgroup$ May 30 at 5:36


You must log in to answer this question.

Browse other questions tagged .