In proof theory, the condition satisfied by a term $t$ appearing in a formula $\phi$ when $\phi$ is the only formula in which the term $t$ appears. In the case of sequent calculi, this amounts to the condition that the term $t$ (the eigenvariable in the inference) appears in the principal formula of the inference and in no other formula in the sequent. In the case of the left-introduction rule for the existential quantifier and right-introduction rule for the universal quantifier, i.e.,

where $\phi \left(x/t\right)$ is the formula in which each instance of $t$ is replaced by an instance of $x$, the eigenvariable condition is the condition that $t$ not appear in any formula in $\Gamma \cup \Delta$.

In natural deduction proofs, the eigenvariable condition bears on the elimination rule for $\exists$ and the introduction rule for $\forall$, so that the term that is being instantiated or abstracted does not occur in any assumption that has not been discharged. This condition precludes inferring, e.g., the theoremhood of a formula $\mathrm{Pt}\to \forall \mathrm{xPx}$ from an inference) such as:

In other words, the eigenvariable condition fails because the term $t$ appears in an undischarged assumption (i.e., $\mathrm{Pt}$).