 A few remarks about these rules are in order. One is that, since only finitely many terms can occur in the finite section of a proof preceding a given application of a rule, we could require that the special term, \(a\), used in an application of \(\forall\)-I or \(\exists\)-E should not occur in the hypothesis of any of the subproofs containing the rule application (or in any premiss of the whole proof): in the terminology used in discussing Gentzen’s tree-like formulation of natural deduction, \(a\) cannot occur in a hypothesis above the rule application unless that hypothesis has already been discharged by some earlier application of a rule of supposition. This would slightly simplify the overall framework by rendering unnecessary the restriction on reiteration into general subproofs. On the other hand, in constructing a very long formalized proof, it is convenient to allow ourselves to re-use special terms. If we did do without the restriction on reiteration, we could reformulate \(\forall\)-Introduction without mentioning a special subproof. We could just say that \(\forall x(A(x))\) may be asserted after \(A(a)\), provided that \(a\) does not occur in earlier hypotheses that have not been discharged (many popular undergraduate textbooks adopt this course). This would simplify the statement of the rules a bit (though not the process of constructing proofs: checking that \(a\) doesn’t occur in “prohibited” hypotheses will be time-consuming in constructing a long proof). On the other hand, it would obscure the relationship between the \(\forall\) and \(\exists\) rules.