Existential Quantifier (First-Order Tableaux)

first-order-logic tableaux

Definition

Existential Quantifier (First-Order Tableaux)

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

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

Examples

$t:\exists xP(x)$

Replace with $t:P(c)$ where $c$ is a new parameter not yet on the branch. This captures the idea: to satisfy an existential claim, we introduce a witness. The parameter $c$ names that witness.

$f:\exists xP(x)$

If the branch contains $f:\exists xP(x)$ and the ground term $a$ is available, we may add $f:P(a)$. As with $t:\forall$, the rule can be applied repeatedly for different terms.