A foundation for mathematics is a formal system in which a "reasonable"
amount of actual mathematics can be derived. Since the correctness
of
statements has industrial relevance, it is useful to actually make
formalizations in full: in this way proofs can be checked by a small
program. Proof-assistants have been constructed; these are tools that
help
a user to develop parts of mathematics in an implementation of a formal
system.
Now there is a choice as to how much efficient computational
power
a formal system should have. By this we mean that if we need
to derive
|- F(a) = b (1)
where F represents, say, some primitive recursive function, then the
actual
formal proof of this fact should not be too expensive. In this respect
Peano arithmetic and ZFC are not having an efficient computational
power.
Our claim is that for proof-assistants one needs a foundation
with
an efficient computational power. This is need is not only caused by
the
sometimes neccessary proofs of statements like (1). It is also of
importance for statements that seemingly do not have any computational
content. The reason is that in the process of formalization it will
turn
out that steps that are intuitively clear can (and have to) be captured
by
symbolic computations.
Back to Talks Page