= Solution
A fresh variable is an arbitrary <eigenvariable> whose value is not constrained by the undischarged assumptions. For <universal introduction>, it must not occur free in those assumptions; otherwise a fact about one constrained object could be incorrectly generalized to all objects. For <existential elimination>, its temporary witness must additionally not occur free in the conclusion or in other undischarged assumptions outside the witness subproof. Choosing a completely unused variable is a sufficient convention. These are the <eigenvariable conditions>, and concern free occurrences rather than harmless reuse of bound names.
Back to article page
