FOM: Reaction to Simpson

[Henk Barendregt]

Reaction to Steve Simpson's posting of Thu, 5 Mar 1998 11:48:11 -0500
(EST)

---------------------------------------------------------------------

DEFINITION
A foundation of mathematics (F.O.M.) is a formal system such that

1. Enough mathematics is derivable.

CLAIM
ZFC set-theory is a F.O.M.

DEFINITION 
A computational foundation of mathematics (C.F.O.M.) is a formal
system such that

1. Enough mathematics is derivable.

2. There is a way to express that AE statements are effectively
provable.

3. Fully formalized proofs can be generated efficiently in an
interactive way by a human with the help of a workstation (once an
intuitive proof is known). A small program can verify these fully
formalized proofs.

4. Computational aspects of statements should be executable. If an AE
statement is effectively provable, then we should be able to get from
the fully formalized proof an efficiently executable code of the
corresponding Skolem function.

CLAIM 
Having a C.F.O.M. is interesting. (For technological applications, for
genuine logical interest and for mathematicians.)

CLAIM 
ZFC is not a C.F.O.M. ZFC satisfies 1 and 2 (via the Kleene
T-predicate), but not 3 and 4.

That ZFC does not satisfy 4 is related to an observation of Vaughan
Pratt: the code of a simple computable function is already large.

CLAIM
There does exists a C.F.O.M. Type theories in the tradition of
Automath are examples.

In order to satisfy 3, the system better satisfies 4.

----------------------------------------------------------------------

Henk Barendregt