|
|
|
|
|
|
by kevinbuzzard
777 days ago
|
|
|
My impression is that some parts of maths work best using set theory, some parts work best using type theory, some work best using a category-theoretic foundation and ignoring size issues etc etc. There's no one "best" foundations, and mathematicians on paper just freely (and mostly unknowingly) switch between foundations depending on what they're doing. This is problematic for a project such as formalising FLT because it involves developing mathematics in a bunch of different areas (algebra, analysis, geometry) where different foundations might be more appropriate (for example getting homological algebra working in dependent type theory has been annoying and hard for all the wrong reasons, and it's taken the Lean community years to figure out how to do it). So I don't really understand the point made in this post. Dependent type theory makes the expression of some theorems more involved and complicated -- but set theory makes the expression of some other theorems more involved and complicated, simple type theory makes the expression of some others more involved etc etc. You're right that we're just powering through this: but formalising mathematics in Lean sometimes feels like fighting against type theory (and sometimes type theory is a very welcome foundation). The point really is that the Lean community, because of its viewpoint of "formalise all mathematics in one system", has been forced to figure out how to power through the areas where dependent type theory was not the ideal foundation. Maybe the same can be said of Mizar and set theory -- I'm unclear about how much formalisation in Mizar is motivated by "let's do this because it will be unproblematic in set theory" and how much is "let's choose to do battle with set theory". In mathlib we've decided to do everything so doing battle with dependent type theory is a necessary consequence. I find it hard to believe that another foundational choice (such as Practal) solves these sorts of problems: presumably what's actually true is that some stuff which is annoying in Lean is nice in Practal but some other stuff which is nice in Lean is annoying in Practal. |
|
|
I think you understand the point perfectly well. You just don't believe that there can be a logical system better suited to a foundation of mathematics than first-order logic (set theory), simple type theory, or dependent type theory. You believe you will need to compromise, no matter which foundation you choose, so better just to pick your poison and get on with it. And I think pretty much everyone in the theorem proving space has that same opinion, so it is certainly a most reasonable opinion.
But I don't believe that the right logical foundation will make it harder to do mathematics on a computer than on paper, I think it will make it easier. In fact, I am pretty sure I have found that right logical foundation, Abstraction Logic [1]. I believe that it is indeed the best logical foundation, because it is simple and elegant (more so than any other foundation I am aware of), and it seems obvious that first-order logic, simple types, and dependent types are just special cases of it.
But a logic is not a working and proven system such as Lean + mathlib, so a lot of work needs to be done before my belief can be stated as a fact.
[1] http://abstractionlogic.com