FOM: logical vs mathematical
Roger Bishop Jones
rbjones at rbjones.com
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
(You don't get off the ground without some form of abstraction.)
Set comprehension is then defined in terms of functional abstraction.
More information about the FOM