Practical Foundations of Mathematics

Paul Taylor

1.5  Proof Boxes

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,

q[0]
"n:N.q[n] q[n+1]
"n:N.q[ n].

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


depth.3width0pt #1
#
# 1
#
#
#
#
#
#
#
#
# \multispan6
\multispan5
f\span \omit \span \omit
hyp
"x0:
:\span \omit \span\omit
:
y\span \omit \span \omit
y[x0]
\multispan6
f y\span \omit \span \omit
"x.y[x]
fy\span \omit \span \omit \span
$x.f[x]
\multispan6
f
hyp
y
hyp
$x0:
f[x0]
witn
:
:
:
q
q
^
x
 
*
0 
q
\multispan6
q\span \omit \span \omit
E
q
$E