Is the problem that human mathematicians have decided that classical logic + ZF(C) is the best framework for them–but it isn’t the best framework for computers?
Which raises an interesting philosophical question - do contemporary mathematicians mostly do things one way rather than another (i.e. classical logic instead of intuitionistic/paraconsistent/etc logic, ZF(C) set theory instead of alternative set theories or type theory or whatever, classical analysis instead of non-standard analysis, and so on) - because they’ve settled upon the inherently superior (easier, more productive) way of doing things - or is that just an accident of history? Could it be that in some alternative timeline or parallel universe out there, mathematics took some different forks in the road, and the mathematical mainstream ended up looking very different from how it does here?
Which raises an interesting philosophical question - do contemporary mathematicians mostly do things one way rather than another (i.e. classical logic instead of intuitionistic/paraconsistent/etc logic, ZF(C) set theory instead of alternative set theories or type theory or whatever, classical analysis instead of non-standard analysis, and so on) - because they’ve settled upon the inherently superior (easier, more productive) way of doing things - or is that just an accident of history? Could it be that in some alternative timeline or parallel universe out there, mathematics took some different forks in the road, and the mathematical mainstream ended up looking very different from how it does here?