A student builds a tableau for formula φ and finds one branch still open. They say 'I just haven't finished expanding that branch yet.' When are they right, and when are they wrong?
AThey are always right — any open branch means more decomposition rules can still be applied
BThey are right only if unexpanded formulas remain on that branch; if it is fully expanded, the open branch is a counterexample showing φ is not a tautology
CThey are always wrong — an open branch always means the formula is a tautology
DThey are right — a tableau proves a tautology when at least one branch closes, not all of them
An open branch with unexpanded formulas does mean more work remains. But a *fully expanded* open branch — where every formula has been decomposed as far as the rules allow — is a genuine counterexample: the literals on it form a consistent partial assignment that satisfies ¬φ, proving φ is not a tautology. The key word is 'fully expanded.' Option D reverses the requirement: for a tautology, *every* branch must close — one open branch is enough to refute it.
Question 2 Multiple Choice
In a semantic tableau for the formula ¬(P ∨ Q), what is the correct next step after writing ¬(P ∨ Q) at the root?
AFork the tree into two branches: one with P and one with Q
BAdd both ¬P and ¬Q to the same branch, extending it without forking
CAdd P and Q to the same branch, since ∨ requires both to be considered
DClose the branch immediately, since a negated disjunction is always false
¬(P ∨ Q) is equivalent to ¬P ∧ ¬Q by De Morgan's law — it is a conjunctive form (alpha formula). Conjunctions add both conjuncts to the same branch without forking, because any satisfying assignment must satisfy both. So ¬P and ¬Q are both added to the current branch. Option A describes the rule for a disjunction (P ∨ Q), which would fork the tree. Recognizing whether a formula is conjunctive (alpha) or disjunctive (beta) determines whether to extend or branch.
Question 3 True / False
Semantic tableaux are a refutation procedure — they prove a formula is a tautology by assuming its negation and showing that assumption leads to contradictions on every branch.
TTrue
FFalse
Answer: True
This is the defining structure of the method. You place ¬φ at the root (assuming φ is false) and systematically decompose it to find any truth assignment that satisfies ¬φ. If every branch closes (contains both φ and ¬φ for some φ), then ¬φ is unsatisfiable — no assignment can make it true. Since ¬φ is unsatisfiable, φ must be true under all assignments — it is a tautology. The indirect proof structure (assume the negation, derive contradiction everywhere) is what makes tableaux a refutation system.
Question 4 True / False
In a semantic tableau, a disjunction P ∨ Q on a branch means you add both P and Q to that same branch without forking.
TTrue
FFalse
Answer: False
This confuses the rules for conjunctions and disjunctions. A conjunction P ∧ Q adds both P and Q to the same branch (conjunctive/alpha rule), because any satisfying assignment must satisfy both conjuncts. A disjunction P ∨ Q instead forks the tree into two branches — one containing P, one containing Q — because any satisfying assignment must satisfy at least one disjunct but not necessarily both (disjunctive/beta rule). Applying the conjunction rule to disjunctions is the most common tableau error and produces incorrect results.
Question 5 Short Answer
Why does a closed semantic tableau prove that the original formula φ is a tautology? Explain the logical chain.
Think about your answer, then reveal below.
Model answer: The tableau starts by assuming ¬φ. Each branch represents a possible way a truth assignment could satisfy ¬φ. A branch closes when it contains both some formula and its negation — a contradiction that no assignment can satisfy. If every branch closes, every possible way to satisfy ¬φ leads to contradiction, so ¬φ is unsatisfiable. A formula is unsatisfiable if and only if its negation is a tautology. Therefore ¬(¬φ) = φ is a tautology.
Three logical steps link the closed tableau to the tautology claim: (1) decomposition rules are truth-preserving — each branch faithfully represents a class of possible assignments; (2) branch closure means that class leads to contradiction and is thus empty; (3) all branches closing means no assignment satisfies ¬φ — ¬φ is unsatisfiable. By the classical equivalence 'φ is a tautology iff ¬φ is unsatisfiable,' the closed tableau proves φ is valid. Soundness of the rules is what justifies step (1); completeness guarantees that every tautology will eventually produce a closed tableau.