Questions: Semantic Tableaux (First-Order)

Question 1

You are building a first-order tableau and encounter ∃x P(x) on a branch. Constants a and b already appear on the branch. How should you correctly apply the δ rule?

• A. Add P(a) and remove ∃x P(x) from the branch, since a is already present
• B. Add P(b) because b is the most recently introduced constant
• C. Introduce a fresh constant c (not appearing anywhere in the tableau) and add P(c)
• D. Add both P(a) and P(b) to cover all existing constants

Answer: (C)

The δ rule requires a *fresh* constant — one that does not appear anywhere in the tableau. This freshness condition enforces that c is an arbitrary, unnamed witness for the existential claim. If you reuse an existing constant like a, you are asserting that the thing satisfying P(x) is the same object as a, which is unjustified and could conflate distinct witnesses, invalidating the proof. The δ rule is applied once per existential formula on a branch; the formula can then be set aside (unlike the γ rule).

Question 2

You run a fair tableau procedure on a first-order formula φ. After many rule applications, the procedure has not terminated. What is the correct conclusion?

• A. φ is definitely invalid (satisfiable), because valid formulas always terminate quickly
• B. φ is definitely valid, because an infinite procedure indicates completeness searching
• C. Non-termination is expected for invalid formulas; the open branches accumulating on the tableau are building a countermodel, but we cannot yet conclude anything definitive
• D. The procedure has a bug — a correct fair tableau procedure always terminates

Answer: (C)

FOL validity is not decidable (Church's theorem), so no sound and complete procedure can always terminate. The fair tableau method is *semi-decidable*: if φ is valid, the tableau closes in finitely many steps; if φ is invalid, the procedure may run forever as the γ rule generates new terms requiring new instantiations. Non-termination does not prove invalidity — it only means we haven't yet found either a proof or a finite countermodel. The open branches are building toward a countermodel, but we cannot conclude invalidity without a completed open branch.

Question 3

After applying the γ rule to ∀x φ(x) on a branch, the formula ∀x φ(x) must remain on the branch for potential future instantiations.

• T. True
• F. False

Answer: True

This is the defining feature of the γ rule and what distinguishes it from the δ rule. A universal formula ∀x φ(x) says φ holds for *every* domain element — no single instantiation exhausts it. You may need to instantiate it with different terms as new constants are introduced by δ-rule applications. If you removed ∀x φ(x) after one instantiation, you would lose the ability to use it again, making the procedure incomplete. The δ rule, by contrast, is applied once — the fresh constant witnesses the existential claim, and the formula can be retired.

Question 4

A completed fair tableau with at least one open branch proves that the original formula (before negation) is not valid, because the open branch defines a countermodel.

• T. True
• F. False

Answer: True

Soundness of the tableau method guarantees this: if every branch were closable, the formula would be valid. An open completed fair branch contains no contradiction and has been fully developed — every universal formula has been instantiated with every relevant term. Reading off the branch: the domain is the set of constants appearing on the branch, and each predicate P is true of exactly the tuples for which P(c₁,...,cₙ) appears positively on the branch. This interpretation satisfies the negation of the original formula, meaning the original formula is false in that interpretation — a genuine countermodel.

Question 5

Why is the fairness condition necessary for the completeness of first-order tableaux? What could go wrong without it?

Model answer: Without fairness, the procedure might repeatedly instantiate one universal formula while ignoring another, or use only old constants and never the fresh ones introduced by δ applications. This could leave a branch open indefinitely even though it should close — the procedure would fail to find the required instantiation.

Concretely: suppose a branch has ∀x ∀y R(x,y) and an existential introduces fresh constant c. A strategy that only ever instantiates ∀x ∀y R(x,y) with the original constant a would never produce R(c, a) or R(a, c), which might be exactly what is needed to close the branch. Fairness requires that every universal formula be eventually instantiated with every term on the branch, including those introduced later by δ applications. Without this guarantee, the tableau is sound but not complete — it can prove valid formulas valid, but may fail to close branches that should close.