Eigenvariable
= Eigenvariable
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.