FOM: computational fom

[Henk Barendregt]

We need a computational foundation of mathematics

--------------------------------------------------------
Although  have not read all contributions about the
definition and scope of "foundations of mathematics", I
like to state the following.

Mathematics consists of the following:

In a (mathematical) context Gamma one proves that 
statement A is valid.

A fom is a formal theory that is capable of formulating
Gamma and A and to formulate that A is a consequence of
Gamma:

Gamma |- A.

[First-order predicate logic with equality is only a foundation
for limited fragments of mathematics. ZFC is a foundation for
a substantial fragment.]

Why do we want/like a fom? 
* To have a frame for which people can agree that it produces
  valid results.
* To have a frame in which most results fit, so that one does not
  have disjoint islands of mathematical knowledge. (J.-Y.G.)
* To produce metamathematical results, as for example the
  incompleteness and undecidability results.

There is a further scope of fom, hitherto neglected in this 
chatbox. Let me call a fom satisfying it a computational fom (cfom).

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

Gamma |-_p A

should be a decidable predicate. Moreover it should satisfy the
de Bruijn criterion:

Gamma |-_p A is decidable by a simple program.

Indeed, if a program of 10 Mbyte is needed, we will not trust
verification by it. But a small program can be checked by hand.

Now ZFC (or topos theory) does not fulfill this scope.
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.

Why does one want a cfom?

|| In order to do reliable proof-checking for complex proofs
|| (complexity either deriving from mathematical depth or from
|| sheer number, like in specifications of IT systems).

Now the claim is that type systems provide a good cfom.
Type systems (TS) consist of a pure type system (PTS) plus
inductive types (IT), coming with their recursors for 
primitive recursion and induction:

TS = PTS + IT

Computations are done following the Poincare' Principle.
If we have a proof of A(2+2) then that same proof is also a 
proof of A(4). 

De Bruijn adopted the Poincare' principle for beta-delta reduction
(delta reduction for the unfolding of definitions) and Martin-Loef
for iota reduction corresponding to the work of the recursors.

That we do need computational power in a cfom is related to a remark
of V. Pratt in this forum (dated Jan 14, 98 04:04:35 pm). He 
mentioned that simple computable functions have a complicated 
formal code. If we do not work with this code as an executable, then we never will get a cfom. Of course there is a price to be paid
for adopting the Poincare' Principle. In order to believe in a 
proof-checker we have to be convinced that it is correct. This 
has to be done by hand. In a proof-checker employing the Poincare'
Principle this checking by hand is a little more complicated, 
since we have to be convinced that the implementation of the 
recursors is done properly.

Type systems have two parameters: logical force and computational
power. Having a system in which these parameters may be set is 
useful. One may choose for a predicative logic, but strong 
computational power, as does Martin-Loef. Or one may opt for 
strong logic and weak computational power, as does de Bruijn.
The Coq system has both parameters in a strong position.

Claim (not yet established but firmly believed)

Type Systems provide a cfom adequate for large parts of
mathematics.

[Of course not for all, since Goedels theorem applies.
But Goedels true but unprovable arithmetic statement G can be proved
in second order arithmetic. By switching a parameter of the TS, one
can prove G.]

One of the applications of cfom is a reliable computer 
algebra system. One may call such systems even a 
computer mathematics system.

For some background, see my article "The impact of the lambda 
calculus", last section, in: Bulletin of Symbolic Logic, vol 3 (2),
1997.

Henk Barendregt
---------------------------------------------------------
professor of fo(m&cs)
Nijmegen, The Netherlands
henk at cs.kun.nL