[FOM] proof assistants and foundations of mathematics
Timothy Y. Chow
tchow at math.princeton.edu
Wed Aug 8 11:34:10 EDT 2018
On Wed, 8 Aug 2018, Arnon Avron wrote:
> Maybe I am wrong, but I think that what worries Jose about Coq is the
> *mathematical* reliability, and even the consistency, of the very
> complicated mathematical typed sytem on which Coq itself is based.
> Someone who has doubts about *that* will not fully trust proofs in Coq
> even if he takes it for granted that its type system was implemented
> correctly, and no cosmic rays were affecting its behavior either.
If you are right, and Jose trusts set theory to some degree, then maybe
the following references will be relevant.
"Sets in Coq, Coq in Sets" by Bruno Barras, Journal of Formalized
Reasoning 3 (2010), 29-48. https://jfr.unibo.it/article/view/1695/1316
"On Relating Type Theories and Set Theories" by Peter Aczel, in Types for
Proofs and Programs, Lecture Notes in Computer Science Volume 1657, 1999,
pp 1-18.
See also:
https://mathoverflow.net/questions/59520/how-true-are-theorems-proved-by-coq
Tim
More information about the FOM
mailing list