Comment by xjm
3 days ago
First sentence:
> All of modern mathematics is built on the foundation of set theory
That's ignoring most of formalized mathematics, which is progressing rapidly and definitely modern. Lean and Rocq for example are founded on type theory, not set theory.
I think what is more accurate to say is that the broad crisis in foundations of mathematics was initially resolved by formalizing set theory.
Not a mathematician, but AFAIK ZFC is a valid foundation. Dependent types helps a lot with bookkeeping, but cannot prove more theorems.
Lawrence Paulson is a great person to clarify those topics (Isabelle/HOL is not based on types yet it can proof most maths).
> but cannot prove more theorems
usually you're more interested in better ergonomics: can you do X with less work?
it's like picking a programming language - depending on what you're attempting, some will be more helpful.
and ZFC is a lot more low level than what day-to-day mathematics usually bothers with. So most mathematians actually work in an informally understood higher-order wrapper, hoping that what they write sufficiently explains the actual "machine code"
the idea then behind adopting alternative foundations is that these come with "batteries included" and map more directly to the domain language.
>hoping that what they write sufficiently explains the actual "machine code"
actual, having faith that what they write could compile, run, and pass tests, but never doing so.
Isabelle/HOL is still types. The underlying type theory of Isabelle/HOL is not theory of dependent types, but theory of simple types. Isabelle/ZF would be a better example as it encodes Zermelo–Fraenkel set theory.
Right!
It’s not really. It leads to paradoxes. There are alternative formulations which avoid these.
Uh? Could you write an example or two?
And formalised mathematics are ignored in mathematical practice by most mathematicians, and even the ones that know of it often don't use that as a foundational language due to relative inconvenience.
I think at this stage, most mathematicians recognize that formal proof verification is a real and interesting thing. We have extremely prominent mathematicians like Scholze & Tao making a point of using these tools.
But in many cases, it's extra effort for not much reward. The patterns which most mathemematicians are interested in are (generally) independent of the particular foundations used to realize them. Whether one invests the effort into formal verification depends on how hard the argument is and how crucial the theorem.
You are conflating two things - the language of math, and the language of proving facts about the language of math.
The former is almost entirely sets, while the later is necessarily types.