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.

Choose an arbitrary fresh eigenvariable $v$. If $\neg R(v)$ held, existential quantifier introduction rule would contradict the premise. Derive $R(v)$ by double-negation elimination, then generalize:

HenceAt the final universal introduction, $v$ is free in no open assumption: the only remaining premise is the closed first-order formula $\neg \exists x\neg R(x)$. Thus the eigenvariable condition is satisfied. The passage from double negation to the positive relation uses the paper's classical rule.

A variable $v$ is fresh for the relevant context when it occurs free in none of its undischarged assumptions. For the existential quantifier elimination rule, it must also not occur free in the final conclusion $\kappa$ or the existential premise: it is a new eigenvariable, allowed in the temporary witness assumption $\varphi (v)$ and formulas inside that witness subproof. Bound variable names can always be renamed to avoid collisions.

The premise $\exists x\varphi (x)$ guarantees some witness, without saying which object it is. Temporarily call one such witness $v$ and assume $\varphi (v)$. If the subproof yields $\kappa$ without depending on any special identity or extra property of $v$, its conclusion holds whichever witness exists. The existential quantifier elimination rule therefore discharges $\varphi (v)$ and retains only the original existential premise and other open assumptions.This eigenvariable condition prevents inferring $\varphi (v)$ for a previously chosen object merely from existence. In particular, $\exists xQ(x)$ does not license $Q(v)$ outside the discharged witness subproof.

The existential premise is $\exists x(Q(x)\to R(x))$, with the logical implication inside the existential quantifier. Eliminate it using a fresh witness $a$, specialize $\forall xQ(x)$ to that same witness, and introduce the required existential quantifier before closing the witness subproof:

The eigenvariable $a$ is absent from the premises and from $\exists xR(x)$. Consequently,

Choose an eigenvariable $v$ fresh for the premise. Use the existential quantifier introduction rule to contradict the premise under a temporary assumption $R(v)$:At line 6 the assumption $R(v)$ has been discharged and the sole remaining premise has no free $v$, satisfying the eigenvariable condition. Thus

The dot after $\forall x$ gives it scope over the following implication: read the premise as $H=\forall x(P(x)\to Q(x))$. Choose a fresh arbitrary eigenvariable $u$. A natural deduction proof isAt line 6, $u$ is free in no undischarged assumption, so the universal quantifier introduction rule is valid.

The proposed variant is not derivable in a sound first-order logic. For a countermodel, use the two-element domain $\{0,1\}$, interpret both predicates $P,Q$ as $\{0\}$, and assign the free variable $x$ the value 0. Then $\forall x(P(x)\to Q(x))$ is true, as is $P(x)$ under the assignment, but $\forall xQ(x)$ is false at element 1. The premise's bound $x$ and the conclusion's free $x$ have different scopes.Attempting to generalize from $Q(x)$ in the variant would violate the eigenvariable condition, because $x$ remains free in the undischarged assumption $P(x)$.

Let $H=\forall x\forall y(S(x,y)\vee \neg S(x,y))$ and abbreviateAssume $\exists bB(b)$ and eliminate the existential quantifier using a fresh eigenvariable $u$. Inside that subproof, specialize $B(u)$ at $p=u$. Write $s=S(u,u)$. The premise $H$ supplies $s\vee \neg s$, so a disjunction elimination rule finishes the contradiction:Line 7 abbreviates two consecutive universal quantifier elimination rule applications; no new rule is used. The fresh witness $u$ is absent from $H$, the assumed existential statement and the exported $\perp$, so the existential quantifier elimination rule satisfies its eigenvariable condition. This is the self-application behind the barber paradox, written entirely with the supplied rules.

Choose fresh arbitrary eigenvariables $u,v$. Under $u=v$, use the equality elimination rule to transport $P(u)$ to $P(v)$. For the reverse direction, first derive $v=u$ by the symmetry derivation above. In full natural deduction form:All temporary assumptions are discharged before either universal quantifier introduction rule application, so both eigenvariable conditions hold. No premises remain:

In a finite domain, an existential quantifier says that at least one candidate satisfies $\varphi$. Reason with a fresh name $v$ for such an unspecified witness. If the same conclusion $\kappa$ follows using only $\varphi (v)$ and the original premises, without depending on which candidate $v$ names, then $\kappa$ follows from the existential premise itself.

This is exactly existential elimination in boxed form: the sequent $\Gamma ,\varphi (v)⊢\kappa$ is the branch inside the box. The eigenvariable $v$ must not occur free in the original undischarged context or in the exported conclusion $\kappa$. Otherwise the proof could smuggle in information about a specially chosen individual or export a fact about a witness whose name has just left scope. Freshness does not mean that the domain contains an additional object; it means that its temporary name carries no other assumptions.

The proposed proof is invalid: its existential-elimination step exports $Q(x_0)$ while the witness name $x_0$ still occurs free in that conclusion. Introducing an existential quantifier later does not retrospectively repair that scope error.

Introduce the existential quantifier before discharging the witness box:The conclusion of existential elimination now has no free occurrence of $a$, and the name occurs in neither original premise, satisfying the eigenvariable condition.

A fresh variable is an arbitrary eigenvariable whose value is not constrained by the undischarged assumptions. For universal introduction, it must not occur free in those assumptions; otherwise a fact about one constrained object could be incorrectly generalized to all objects. For existential elimination, its temporary witness must additionally not occur free in the conclusion or in other undischarged assumptions outside the witness subproof. Choosing a completely unused variable is a sufficient convention. These are the eigenvariable conditions, and concern free occurrences rather than harmless reuse of bound names.

Adding unused assumptions to the context of a logical derivation. The original derivation still proves the same conclusion because it need not use every available assumption. When eigenvariables are used, rename them first if necessary to preserve the eigenvariable condition for any newly added assumptions. This explains how disjunction elimination with different branch contexts can be written using a common context containing all their assumptions.