= Eigenvariable condition
An <eigenvariable condition> ensures that a variable chosen as arbitrary or as an existential witness cannot smuggle extra information into a <quantifier> inference. For the <universal quantifier introduction rule>, the generalized variable must not occur free in any undischarged assumption. For the <existential quantifier elimination rule>, the fresh witness must not occur free in the resulting conclusion or in the other undischarged assumptions. <Temporary assumptions> may contain it if they are discharged before the final inference.
Back to article page
