[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.
More information about the FOM