Oftentimes when we know a statement of the form
,
we reason as follows: ``We know that there is something for which
holds. Let be a name for that something, so that holds
for . Then '' where is a derivation of some
conclusion , presumably with the help of the premise
that holds for , i.e., the premise
.
It is customary to refer to as a witness, and to
the formula
as the witness premise.
No special assumptions about the witness must be made;
It must serve only as a ``dummy''--any other name should
do just as well. In particular, the witness should not
occur in the final conclusion .
This form of reasoning is captured in NDL with deductions
of the form