Universal Quantifier (First-Order Tableaux)

first-order-logic tableaux

Definition

Universal Quantifier (First-Order Tableaux)

$$\frac{t:\forall xF}{t:F[t/x]}\frac{f:\forall xF}{f:F[c/x]}$$

• $t$: instantiate with any ground term $t$ (may be applied repeatedly).
• $f$: instantiate with a fresh parameter $c$ that does not yet appear on the branch.

Examples

$t:\forall xP(x)$

If the branch contains $t:\forall xP(x)$ and the ground term $a$ is available, we may add $t:P(a)$. The rule can be applied again later with a different term, e.g. $t:P(f(a))$.

$f:\forall xP(x)$

Replace with $f:P(c)$ where $c$ is a new parameter not yet on the branch. This captures the idea: to falsify a universal claim, find a counterexample. The parameter $c$ names that counterexample.