Truth trees, countermodels, and argument validation
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.
In this lesson, you will build tableaux, extract countermodels from open branches, and validate logical arguments.
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.
Testing satisfiability of: ¬(p → (q → p)) (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.
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.
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.
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.
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.
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.
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.