[FOM] proof assistants and foundations of mathematics

José Manuel Rodriguez Caballero josephcmac at gmail.com
Sun Aug 12 23:39:03 EDT 2018

Joe Shipman said:
“It seems to me that no professional mathematician who is not working in logic and set theory, in his everyday work, uses anything that?s not formalizable in ?ZFC plus a proper class of Inaccessibles? (Grothendieck Universes) in well-established ways.”

I am not sure that VERY, as defined by Jean Benabou in elementary topos, can be formalized in ZFC.

Kind Regards,
Jose M.

More information about the FOM mailing list