Mathematicians don't care about foundations
a day ago
- #type theory
- #informal mathematics
- #mathematical foundations
- Most mathematicians are indifferent to foundational issues, working informally without deep knowledge of foundations like ZFC.
- Mathematical foundations, established in the 19th century, didn't invalidate prior mathematics, showing the robustness of mathematical ideas beyond formal frameworks.
- Mathematics is fundamentally informal, relying on shared intuitions and understandings, with formal definitions serving as vessels for deeper ideas.
- The 'crisis in foundations' in the early 20th century had minimal impact on most mathematics, affecting only foundational theories themselves.
- Mathematicians' lack of commitment to specific foundational systems like ZFC opens the door for adopting more expressive foundations, such as structural set theory or type theory.
- A shift to 'naive type theory' in education could lead mathematicians to adopt it as their default framework, without deep concern for its foundational aspects.
- Constructive and predicative approaches in dependent type theory present challenges for classical mathematicians, due to differences in provable statements like LEM and AC.
- Despite these challenges, constructive mathematics can still relate classical theorems conditionally, e.g., 'LEM implies the intermediate value theorem'.