Existential witness
= Existential witness
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>.