| _version_ | 1866901621849456640 |
|---|---|
| author | SÉRGIO DE ANDRADE, PAULO |
| author_facet | SÉRGIO DE ANDRADE, PAULO |
| contents | The foundations of mathematics have historically been approached through various formal systems, with set theory, category theory, and type theory emerging as prominent paradigms. While each offers a robust framework for mathematical reasoning, they often present distinct perspectives on fundamental concepts such as existence, structure, and proof. Set theory, rooted in the notion of collections of objects, provides a universal language for most of classical mathematics (Cantor, 1895; Zermelo, 1908). Category theory, emphasizing structure and relationships between mathematical objects, offers a powerful abstract framework (Eilenberg and Mac Lane, 1945). Type theory, originating from logic and computer science, focuses on constructive definitions and the intrinsic typing of terms and propositions (Russell, 1908; Church, 1940; Martin-Löf, 1984). This paper explores the conceptual and formal pathways towards a foundational synthesis of these three theories. We investigate their individual strengths and limitations, identify common underlying principles, and analyze existing attempts at cross-pollination and unification. By examining how concepts like 'object', 'morphism', 'element', 'type', and 'proof' are interpreted and structured within each paradigm, we propose a framework for their potential integration. The goal is to articulate a more cohesive and comprehensive foundational landscape that leverages the benefits of all three, addressing their historical disunity and paving the way for new avenues in mathematical research, formal verification, and computational logic. |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_17689577 |
| institution | Zenodo |
| language | |
| publishDate | 2025 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Foundational Synthesis: Unifying Set, Category, and Type Theories SÉRGIO DE ANDRADE, PAULO The foundations of mathematics have historically been approached through various formal systems, with set theory, category theory, and type theory emerging as prominent paradigms. While each offers a robust framework for mathematical reasoning, they often present distinct perspectives on fundamental concepts such as existence, structure, and proof. Set theory, rooted in the notion of collections of objects, provides a universal language for most of classical mathematics (Cantor, 1895; Zermelo, 1908). Category theory, emphasizing structure and relationships between mathematical objects, offers a powerful abstract framework (Eilenberg and Mac Lane, 1945). Type theory, originating from logic and computer science, focuses on constructive definitions and the intrinsic typing of terms and propositions (Russell, 1908; Church, 1940; Martin-Löf, 1984). This paper explores the conceptual and formal pathways towards a foundational synthesis of these three theories. We investigate their individual strengths and limitations, identify common underlying principles, and analyze existing attempts at cross-pollination and unification. By examining how concepts like 'object', 'morphism', 'element', 'type', and 'proof' are interpreted and structured within each paradigm, we propose a framework for their potential integration. The goal is to articulate a more cohesive and comprehensive foundational landscape that leverages the benefits of all three, addressing their historical disunity and paving the way for new avenues in mathematical research, formal verification, and computational logic. |
| title | Foundational Synthesis: Unifying Set, Category, and Type Theories |
| url | https://doi.org/10.5281/zenodo.17689577 |