[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

>
> Mario Carneiro said:
> Of course this goes against the intuition that a theorem that has been
> formalized in *any* proof assistant is more likely to be correct than one
> that has not. But this is not really a comparison on equal footing since
> this position is concerned with "human error" in the verification that a
> statement is in fact provable from a formal system, while you are more
> concerned with the possibility that the proof is valid but the underlying
> logic is not consistent. (I think you said that you are not seriously
> concerned with a failure of consistency, but I don't know how else to make
> sense of your differential trust of Q0 over CIC.) Indeed, "it would be a
> shame if their work will be dismissed in the future because of some problem
> with the foundations of mathematics" sounds like a worry that CIC is
> inconsistent.


Rather than worried about the consistency of CIC (calculus of inductive
constructions), I'm worried about the fact that I do not understand why
Voevodsky said that CIC was no cleanly defined from the point of view of
the foundations of mathematics. When Voevodsky said that Peano arithmetics
may be inconsistent, he was criticized, but that was a statement with the
modal verb MAY. When Voevodsky said that CIC is not cleanly defined, he
used the verb IS, which indicates that he was certain about it. I'm not
aware of any criticism to Voevodsky for this statement.

By the way, Voevodsky did not used CIC for his UniMath utopia, but rather
the part of CIC related to Martin-Lof type theory. Voevodsky has surprised
the mathematical community several times in the past, e.g., when he applied
homotopy theory in a non-trivial way to Algebraic Geometry, something that
was though to be impossible by the experts in both fields. I finish with
the following quotation of S Cin about Voevodsky:

Pity the community of mathematicians having to deal with this man who
> thinks so outside the box. His project will probably have to wait.  Sad he
> left us so soon.


Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180813/423e7329/attachment.html>