Definition
Existential Quantifier (First-Order Tableaux)
: instantiate with a fresh parameter that does not yet appear on the branch. : instantiate with any ground term (may be applied repeatedly).
Examples
Replace with
where is a new parameter not yet on the branch. This captures the idea: to satisfy an existential claim, we introduce a witness. The parameter names that witness.
If the branch contains
and the ground term is available, we may add . As with , the rule can be applied repeatedly for different terms.