For JJ Smith's propositional logic trees, why is the negated biconditional used for equivalence instead of simply α and ¬β?

34 Views Asked by At

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?