FOM: logical vs mathematical

[Roger Bishop Jones]

Till Mossakowski Monday, September 11, 2000 4:57 PM writes:

> Actually, the "theorem proving in HOL" community has formalized a good
> portion of mathematics in
>
> HOL + comprehension + Axiom of infinity
>
> This system is obviously weaker than ZFC, but still it has some
> technical advantages (namely the use of lambda abstraction,
> and the Hilbert choice operator, among others), that make
computer-assisted
> proofs easier.
>
> Both comprehension and infinity are not part of HOL, but they are
> added as axioms later on. They seem to be the minimum of mathematical
> axioms that are needed to formalize any reasonable part of mathematics.

This is perhaps a little misleading.
The HOL logic used in the cambridge HOL system (and several other theorem
provers) is based on Church's Simple Theory of Types (STT).
Rather than set comprehension HOL (following STT) has functional abstraction
as primitive.
(You don't get off the ground without some form of abstraction.)
Set comprehension is then defined in terms of functional abstraction.

Roger Jones