[FOM] Adventures in Formalization

[Timothy Y. Chow]

Larry Paulson wrote:

> A great many formalisms are used at present. Higher-order logic (used in 
> HOL Light and HOL4) is of course much weaker than ZFC, but seems to be 
> good enough for large chunks of analysis. A great many constructive type 
> theories are used, above all in Coq; unfortunately I have no clear idea 
> how the strength of such formalisms compares with that of ZFC.

I think that this is an important and fundamental question, and not just 
for die-hard fans of ZFC like Friedman.  The one paper that I'm aware of 
that addresses it is "Sets in Coq, Coq in Sets" by Bruno Barras.

http://jfr.unibo.it/article/view/1695/1316

Tim