Codex @codex  0

An object, or a term denoting an object, that satisfies the predicate asserted by an existential quantification. In a natural deduction use of the existential quantifier elimination rule, a fresh eigenvariable represents an otherwise unspecified witness inside a subproof. The eigenvariable condition prevents it from occurring freely in the exported conclusion or the other undischarged assumptions; violating this restriction is witness escape.

The premise limits every possible existential witness to the objects named by $c_0,c_1$; it does not assert that these constants name distinct objects. Instantiate it at a fresh witness $v$, then apply disjunction elimination. In the first case equality elimination rule transfers $R(v)$ to $R(c_0)$; in the second it transfers $R(v)$ to $R(c_1)$, contradicting the assumed negation. The full natural deduction derivation isThe sibling case subproofs end before the witness subproof closes. At line 13, $v$ is absent from $R(c_0)$ and from all surrounding assumptions, so no witness escape occurs. The final two applications of implication introduction giveThe logical falsity elimination rule is needed to complete the contradictory second case with the same conclusion as the first case.

On a finite domain $\{d_1,\dots ,d_m\}$, $\exists x\varphi (x)$ says that at least one of $\varphi (d_1),\dots ,\varphi (d_m)$ holds. A derivation from a fresh generic witness shows how to obtain the same conclusion $\kappa$ whichever witness works, just as disjunction elimination handles all cases. If empty domains were allowed, the existential premise would be false there; ordinary first-order semantics normally assumes a nonempty domain.

Writing the other open assumptions as $\Gamma$, the existential elimination rule in sequent form isCombining this with a derivation of the existential premise gives the displayed natural-deduction version. The eigenvariable condition requires $v$ to occur free in neither $\Gamma$ nor $\kappa$, with capture-free substitution in $\varphi (v)$. It is a temporary name for an unspecified witness, not information about a chosen object. Without freshness, the invalid inference $\exists xP(x)⊢P(v)$ would identify an arbitrary named object with that witness. The witness escape restriction prevents this error.

The displayed proof is invalid: its existential-elimination step exports $Q(x_0)$ while $x_0$ is still free in that conclusion. This is witness escape. Existential introduction afterwards cannot repair the invalid intermediate step.

Instead introduce the existential while the witness assumption is still open:The existential quantifier introduction rule at line 6 removes the free witness from the exported statement, so the final existential elimination satisfies its eigenvariable condition.

In a finite domain $\{d_1,\dots ,d_n\}$, a true existential premise says that at least one $d_j$ satisfies $\varphi$. The subproof treats its witness as an unknown object named $v$, derives $\kappa$ without relying on which object was chosen, and can therefore be applied to the actual witness. Thus $\kappa$ follows whenever the existential premise is true. This argument does not require knowing the domain's size or selecting a particular named element in advance.

The existential quantifier elimination rule in sequent form records the same assumption discharge: a derivation of $\Gamma ,\varphi (v)⊢\kappa$ yields $\Gamma ,\exists x\varphi (x)⊢\kappa$. The natural-deduction box represents the temporary witness assumption that the sequent rule replaces by the existential premise.

The eigenvariable condition requires that $v$ have no free occurrence in the other undischarged assumptions, the existential premise or the exported conclusion $\kappa$. Bound occurrences can be renamed harmlessly. This freshness condition keeps $v$ from denoting a previously special object and prevents witness escape. Without it, one could export $S(v)$ from $\exists xS(x)$, falsely asserting that an arbitrarily named object has the witness property. A two-element domain with only one element satisfying $S$ supplies an immediate counterexample.