Definite description and Choice in HOL
R.B.Jones@win0109.wins.icl.co.uk
Thu, 16 Jun 1994 10:11:52 +0100
I endorse John Harrisons comments about the generality of the simple
lambda abstraction available in HOL. Our work on embedding Z into HOL is one
example showing how much more elaborate variable binding constructs can be
interpreted (not only in theory but in practice) in terms of simple lambda
abstraction.
I also endorse his view on the importance of a definite description operator.
>I would say that the most important feature neglected in many presentations
>of logic is some sort of description operator: "the x such that ..." or
>"some x such that ...". I believe Bourbaki postulate such a feature in their
>notional logical foundation. Without it, there seems to be a real reliance
>on nontrivial metatheory (introducing Skolem functions or getting rid of
>existential quantifiers in an elaborate way). If you don't like the Axiom of
>Choice you need to be careful about allowing free variables in the "..."s
>in the introduction rule.
The Cambridge HOL system has unnecessarily confused the relationship between
definite description and choice. In Church's paper on "the theory of simple
types" he uses a operator for definite description which does not prejudice
the principle of choice. The principle of choice can then be introduced if
required, as an axiom. In Cambridge HOL there is only a choice operator, and
you really can't do much without the axiom of choice. A minor alteration to
the primitive axioms and definitions would restore the separation.
In Cambridge HOL to really avoid the axiom of choice you would also have to
remove one of the primitive definitional principles, which effectively presumes
it. This principle, which permits function definitions of the form:
f x = .. x ..
might be considered technically redundant (and in fact is not primitive in
ProofPower). Most definitions of this form can be reduced to the form:
f = \x. .. x ..
without using the axiom of choice, but not all of them. However even where the
reduction can be done without using the axoim of choice it is easier if one can
use choice.
Roger Jones
International Computers Limited