The direct rules cannot prove fÞ y or "x.f[x]: the best they can offer is a hypothetical argument or a scheme of proofs. Nor can they exploit $x.f[x], although they can of course make use of f[a] once a is given.
The ("E )-rule says that all instances f[a] obtainable by substituting terms hold, and it says no more than this. But by "x:X.f[x] we intend f[x] to be true throughout the type X ( cf Remark 1.3.5), not just for those values a with names which can be used for substitution.
Universal quantification over numbers (and not just a scheme ranging over numbers) is needed to formulate the principle of induction,
|
Remark 2.5.12 illustrates the role of the part of the proof corresponding to the nested ", as a repeating feature of a tree. The type X of the variable (the range of quantification) is essential to understanding the quantified formula "x:X.f[x].
The indirect rules To prove fÞ y we must temporarily assume f, and deduce y from that. Then we are (by definition) able to deduce fÞ y without assumption. The additional hypothesis f, and anything we deduced from it, are no longer part of the context for fÞ y, and so our notation must provide a way of ``shielding'' them. The demarcation between facts, assumptions and hypotheses (page 1.1) has changed.
The word indirect has been borrowed from the euphemism indirect proof for excluded middle (Definition 1.8.1), because in these cases at certain stages in the deduction we make assertions which are subsequently withdrawn. We saw similar transformations of expressions as trees on pages 1.1.1- 1.1.2. Dag Prawitz [Pra65] called them proper rules and improper rules.
DEFINITION 1.5.1 The boxed or indirect logical rules are
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||