FOM: Barendregt's ideas on "computational f.o.m."

[Stephen G Simpson]

I'd like to call attention to Henk Barendregt's posting of 16 Jan 1998
09:43:57 proposing what he calls

 > a computational foundation of mathematics.

What is a computational f.o.m.?  Henk says that it would be like ZFC
in providing a unifying framework for the development of mathematics
and a setting for independence results, but in addition it would
provide

 > a way to feasibly formalise proofs so that their correctness can be
 > efficiently checked by computer.

Henk says that "Gamma |-_p A" should be a decidable by a simple
program (he calls this the de Bruijn criterion), but I'm not sure what
|-_p means (does it mean provability in < p bytes?), so I can't
comment on this.

According to Henk, ZFC does not satisfy the de Bruijn criterion:

 > One reason is that ZFC has no good way to handle definitions and
 > computations. Of course one can add such mechanisms, say for 
 > definitions, on top of ZFC. But then one is making a new formal 
 > system.

I would like to ask Henk, can this alleged defect of ZFC be overcome
by adding machinery for extension by definitions and, say, primitive
recursive functions on omega?  Such machinery is fairly standard, I
think.

 > Claim (not yet established but firmly believed)
 > 
 > Type Systems provide a cfom adequate for large parts of
 > mathematics.

Henk, could you please explain why type systems are necessarily better
with respect to the de Bruijn criterion than ZFC or other systems that
are more familiar in f.o.m. research?  Is there some theoretical
reason for this, or is it a conclusion based on experience to date
with automatic or computer-aided proof checking?

Incidentally, there are other mailing lists devoted to computer-aided
proof checking.  What I want to discuss here is the f.o.m. aspects of
this.

-- Steve