Comment by jfmc
3 days ago
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?