In many accounts of proof theory, a term $t$ that stands in for an arbitrary witness to the truth of an existential formula $\exists x\phi \left(x\right)$ or the falsity of a universal formula $\forall x\phi \left(x\right)$.

The introduction and elimination rules for these quantifiers replace terms with other terms, whether by replacing constants with variables or variables with constants. When exchanging these terms, the manner in which a constant is introduced is important. For example, the truth conditions for existential quantifiers are such that the truth of $\exists x\phi \left(x\right)$ in a model entails the existence of a witness, i.e., a member of the domain of which $\phi \left(x\right)$ is true. Despite the fact that $\exists x\phi \left(x\right)$ does not always provide enough information to conclusively determine this witness, one can introduce a term $t$, i.e., instantiate the formula, that acts as an arbitrary witness of the formula $\phi \left(x\right)$.

However, when one infers, e.g., $\phi \left(t\right)$ from $\exists x\phi \left(x\right)$ there is a need to keep the term $t$ sufficiently generic. Suppose that one has established, for example, that one has a consistent set of premisses $\left\{Pa,\exists x\neg Px\right\}$. Were one to instantiate the latter formula without ensuring the genericity of the term witnessing $\neg Px$, one might infer the formula $\neg Pa$, i.e., infer a contradiction from a consistent set of premisses. Many proof theories include eigenvariable conditions that ensure that terms representing witnesses to the falsity of a formula $\forall x\phi$ or the truth of a formula $\exists x\phi$ do not lead to such conflicts.