[FOM] proof assistants and foundations of mathematics

[Timothy Y. Chow]

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