[FOM] proof assistants and foundations of mathematics
Timothy Y. Chow
tchow at math.princeton.edu
Wed Aug 15 13:40:25 EDT 2018
Mk wrote:
> (2) the more concrete issue of a mathematician being allegedly able to
> program a routine within CIC that would prove that 0=1 and therefore
> many, many other theorems.
[...]
> As far as (2) is concerned, it was pointed out by one of the
> participants in this discussion that the responsibility for avoiding
> such malignant routines is the programmer's, not CIC's. I believe this
> rebuttal misses the point, though. If such routines can in principle be
> programmed, this may occur even without the conscious knowledge of the
> programmer. Therefore proofs in such a logical framework are not
> "absolutely reliable", which sort of defeats the whole purpose, or does
> it?
The notion of "absolute reliability" is, in my opinion, a childhood dream
that may be part of what attracts certain people to this area, but I think
that most people with long experience eventually realize that they have to
let go of it. It is certainly not what most people regard as the "whole
purpose." A more nuanced way of stating the "whole purpose" is that we
want to *reduce* the probability of mistakes in proofs. (There are other
purposes as well; as mentioned not so long ago on FOM, a large body of
formalized mathematics could conceivably be used to help train computers
to do research in mathematics.)
I'm not sure which "one of the participants in this discussion" you're
referring to. Certainly, a proof of 0=1 could result either from an
inconsistency in the axioms or an error in the implementation. A
programmer should not be blamed for the former, and the axioms should not
be blamed for the latter. Jose first clarified that he was not so
concerned with implementation details. Now it seems that he's not
concerned with the consistency of CIC either, but only with understanding
Voevodsky's remark. I'm not sure what your concern is, either---are you
worried that CIC might be inconsistent? As I said elsewhere, I don't
think that Voevodsky said anything that would justify such doubts.
Tim
More information about the FOM
mailing list