[FOM] Devlin on incorrect proofs
jasper at cs.kun.nl
Tue Jun 3 09:45:19 EDT 2003
> We might be able to raise our confidence level in a checked proof if it
> were written in a precise enough symbolism to be checked by a computer
> program. But then wouldn't some small margin of potential error still
> remain in the supposed correctness of the program itself?---either in the
> specification of the algorithm, or in its implementation, or in the
> physical functioning of the computer? I would like to know from members of
> this list who are in a position to know, whether there are any theoretical
> results about confidence-levels in automated proof-checking that cannot be
> exceeded (perhaps as a function of the length of input, i.e. length of
> proof to be checked for correctness).
There is a whole branch of science / math / informatics devoted to
automated proof checking and automated reasoning.
Usually these proof checkers utilize the Curry-Howard correspondence to
convert mathematics into type theory. That is to say, every mathematical
statement is turned into a type, and a formal proof is then a term of
that statement's corresponding type.
The idea is that type checking is easy, that is to say, can be performed
by a very small independent program: so small that it, in turn, can be
verified 'by hand'. This is called the "de Bruijn-principle". Since we
are now confident about the validity of the type checking program, we
can in turn utilize it to infer the truth of mathematical statements: we
feed the type checker (a) with the formalised version of the statement,
that is to say, a type; and (b) the formalised proof of the statement,
that is, a term of the type theory. Then we say "go check that term (b)
has type (a)". If the term type-checks, the theorem is proved.
Obviously, a 100% security level can never be achieved, for the reasons
you mention. There is a 'tower' of things to trust: we need to trust the
Curry-Howard isomorphism to be adequate, then we need to trust our
capability of carrying out the formalisation without flaws, then we need
to trust the type checking program, then we need to trust the computer's
faultless functioning, and therefore we need to trust the compiler, the
computer's chips, etc. etc. until, at last, we need to trust that our
understanding of the physical laws is correct, by which we have molded
the physical materials into a computer.
After some experience with formalised mathematics, I personally feel
that the biggest issue is the adequacy of the Curry-Howard isomophism,
that is, the question whether we can faithfully enough represent
mathematics inside type theory - although there may be ways which I have
not considered yet, and which would solve the (rather freakish) problems
I've run into.
Het verschil tussen theorie en praktijk is dat in theorie
er geen verschil is tussen theorie en praktijk.
More information about the FOM