Truth trees, countermodels, and argument validation
A truth tree tests a formula by assuming it and breaking it apart until every branch hits a contradiction or survives. Build a few and see.
Pick a formula and step through its tableau. ANDs extend a branch, ORs split it, and a branch closes when it holds both A and ¬A.
Testing satisfiability of: ¬(p → (q → p)) (tautology)
Semantic tableaux (truth trees) are a systematic method for testing satisfiability. Start by assuming the formula is true, then apply decomposition rules that break compound formulas into simpler ones. Some rules branch the tree (disjunctions), others extend linearly (conjunctions). A branch closes when it contains both A and ¬A. If all branches close, the formula is unsatisfiable.
Select a formula and build its tableau step by step. Conjunctions add both conjuncts to the same branch. Disjunctions split the branch in two. When a branch contains a contradiction (A and ¬A), mark it closed. If every branch closes, the negation is unsatisfiable -- the original formula is a tautology.
Key insight: Tableaux search for counterexamples. If none exist (all branches close), the formula must be valid. An open branch directly provides a satisfying truth assignment.
Pick a formula and look for an open branch in the tableau of its negation. The literals on that branch give a truth assignment that makes the formula false.
To find a countermodel, we negate the formula and look for a satisfying assignment.
Under this assignment, p → q evaluates to False. Therefore it is not a tautology.
Method: Negation gives p ∧ ¬q. Open branch: p=T, q=F makes the original false.
When a formula is not a tautology, its tableau has an open branch. Read off the truth assignment from that branch: if p appears, set p = true; if ¬p appears, set p = false. This gives a countermodel -- a truth assignment that makes the formula false.
Key insight: Tableaux are constructive: they either prove a formula is valid or produce an explicit counterexample. This dual output makes them more informative than truth tables for understanding why a formula fails.
Pick an argument and see whether its tableau closes. Try Affirming Consequent: its open branch shows exactly how the argument fails.
p → q forces q when p is true. Adding ¬q creates a contradiction. Unsatisfiable, so the argument is valid.
Method: An argument is valid iff the conjunction of premises with the negation of the conclusion is unsatisfiable. If satisfiable, the satisfying assignment is a counterexample.
To test whether premises P₁, P₂, ... logically entail a conclusion C, build a tableau for P₁ ∧ P₂ ∧ ... ∧ ¬C. If all branches close, the argument is valid -- there is no way the premises can be true while the conclusion is false. If a branch stays open, the counterexample shows exactly how the argument fails.
Key insight: Many common reasoning errors, like affirming the consequent (from p→q and q, concluding p), are exposed immediately by the tableau method -- the open branch shows the counterexample.
Spot a mistake or have an idea?