集合论、范畴论和类型论三种中哪个是数学的基础？
首先，我们希望找到数学基础的定义是什么？
NG de Bruijn 做出了非凡的声明
我们对“数学”这个词还没有一个可行的定义。（AUT001，第 4 页）
如果我们不能定义数学，我们也不能定义数学基础的概念。
解决这个困难的一个办法是：“我无法定义它，但当我看到它时我知道它是什么”（没有吃过猪，看过猪跑）。
罗素悖论
罗素悖论被视为对 19 世纪大部分基础工作的潜在致命打击，包括弗雷格、戴德金和康托的工作。 罗素（和怀特海）决定继续本着弗雷格将数学还原为逻辑的逻辑主义纲领的精神。
德布鲁因说
我们对“逻辑”这个词还没有一个可行的定义。
许多哲学家在前几个世纪就思考过数学的本质，但这场危机使问题变得紧迫。粗略来说，主要有以下三种观点：
- 柏拉图主义或实在论观点：理想的数学对象，例如复平面，客观且独立于我们而存在，尽管我们可以推断出它们的属性。哥德尔持这种观点。
- 形式主义观点：数学与符号有关。
- 直觉主义者认为数学对象只不过是人类思维的创造。这使他们对证明采取激进的态度，并全面拒绝其他人认为不可或缺的许多技术和概念。他们拒绝数学对象的现实性，并且反对将公式仅仅作为交流机制，这使他们坚决反对其他学派。
从弗雷格、罗素、希尔伯特、布劳威尔和其他许多人的反应来看，显然这些悖论构成了一种紧急情况。罗素的“恶性循环原理”和他的解决方案，即分支类型理论、布劳威尔的直觉主义和希尔伯特的形式主义——这些相当于在发现臭虫时烧掉所有的衣服和家具。
现代数学基础
今天，人们经常看到各种被描述为“数学基础”的东西，特别是范畴论和类型论。基础工作肯定是在范畴论的框架内完成的，但这并不等于范畴论本身就是基础性的。
范畴论中的对象具有结构，对象之间的态射是结构保持的，就像群之间有同态，拓扑空间之间有连续映射一样。
由于数学的很大一部分与结构有关，范畴论是一个自然的选择。然而，这并不意味着它解决了基本问题。相反，它倾向于引入新的类，特别是因为它不幸且不必要地习惯于假设适当的类无处不在。它远非取代集合论，而是依赖于集合论。
至于类型理论是否是基础性的，我们需要问你在谈论哪种类型理论：
- 数学原理：当然，这就是它的确切目的。
- Church的简单类型理论：PM的孙女，同样具有表现力，而且简单很多。
- AUTOMATH：绝对不是。De Bruijn 始终将其称为“数学语言”。他还说，这就像一家餐馆，你可以在那里点任何种类的食物：素食、犹太洁食或其他任何食物。从设计上来说，AUTOMATH 对基础选择是中立的。Isabelle/Pure 也秉承同样的精神。
- 马丁-洛夫类型理论：他本人表示，它的目的是作为形式化毕夏普式分析的工具，这显然是一个基本主张。但它拒绝了绝大多数现代数学。
- 归纳构造微积分（Coq、Lean）：原始论文（描述较弱的系统）开头是“构造微积分是自然演绎风格的构造性证明的高阶形式主义”，并且该论文没有提出任何基础主张。科匡德的回顾性论文也没有提出这样的主张。由于它被证明比 ZF 集合论强得多，我们甚至可以说它做出了基础假设。
100 年前，每个人都在担心数学基础是否一致。我们弄清楚了一些我们一直认为理所当然的细节，比如选择公理，如何防止罗素悖论，以及“真实”和“可证明”之间不可避免的差异（即哥德尔的不完备性）。现在这部分已经基本解决了，我们相当有信心数学基础是一致的。
数学基础是通过形式系统和集合论解决一致性和严谨性的问题。
其他观点：
数学的基础是任何足以证明实际数学中通常被视为公理的结果的形式主义。
详细点击标题