[FOM] proof assistants and foundations of mathematics

[Timothy Y. Chow]

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