[FOM] proof assistants and foundations of mathematics

[Joe Shipman]

Accusing them of working in a theory known to be inconsistent seems unfair, because you don’t know that the moves needed to reach 0=1, which they didn’t make, are actually permitted by the theory you assume they “work in”. 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.

(And the ones who do work in logic and set theory are trivially aware that all their results can be regarded as proving within ZFC that certain axioms not in ZFC entail certain other propositions.)

Most mathematicians “work in” weaker theories, but a large majority of them have no objection to ZFC. (However, the debate about Grothendieck Universes is alive, in my opinion.)

— JS

> On Aug 9, 2018, at 1:30 AM, Franck Slama <franck.slama.pro at gmail.com> wrote:
> 
> What is *the* foundation of traditional mathematics? I don't think there is such *a* foundation of "traditional" mathematics. If you're thinking about set theory, is it ZF? ZFC? General set theory? Kripke-Platek set theory? Something else?
> Many mathematicians (in fact, probably all that are not in the area of formal logic) work in an unspecified theory, and it's not a problem at all for them. They work in something of the flavour of naive set theory, which, even if known to be inconsistent, is perfectly reasonable for doing everyday maths on the paper.