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.
New to topics? Read the docs here!