FOM: logical vs mathematical

Roger Bishop Jones rbjones at
Mon Sep 11 16:52:22 EDT 2000

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
> 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

More information about the FOM mailing list