Eigenvariable condition

An eigenvariable condition ensures that a variable chosen as arbitrary or as an existential witness cannot smuggle extra information into a quantifier inference. For the universal quantifier introduction rule, the generalized variable must not occur free in any undischarged assumption. For the existential quantifier elimination rule, the fresh witness must not occur free in the resulting conclusion or in the other undischarged assumptions. Temporary assumptions may contain it if they are discharged before the final inference.

A variable used as an arbitrary parameter in a natural deduction subproof, subject to an eigenvariable condition. For universal introduction, it must be free in no undischarged assumption. For existential elimination, a temporary witness must also be free in no conclusion exported from its subproof. These restrictions distinguish an arbitrary object from one constrained by a special hypothesis.

An invalid quantifier inference that exports a formula still referring freely to a temporary existential witness. From $\exists xS(x)$ one cannot infer $S(v)$ for an independently named object $v$. A two-element interpretation with exactly one $S$-object refutes that inference. Introducing another quantifier after the invalid step does not repair it; the introduction must take place before the witness scope is closed.