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.

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.