经过千年的犹豫和百年的争执，人们意识到不能再回避无穷作为数学的实体，终于将现代的数学建立在集合论的基础上。

时间淘汰了盛行过的各种流派，在现代有影响的还有三大数学流派，它们都在1900年到1930年间形成。首先是罗素为代表的逻辑学派，认为数学和逻辑是全等的。每一条的数学真理都能够表示为真正的逻辑命题。数学真理的逻辑命题是逻辑真理。数学真理可以由少数逻辑公理和逻辑规则推导出来。他以集合论为基础，相当成功的把古典数学纳入了一个统一的公理系统。形式主义的奠基人是希尔伯特，他将抽象的原则发挥到极致，认为数学研究的是没有意义符号之间的结构性质，数学的推理是一个“有限化”的机械的操作。逻辑主义和形式主义都在集合论上，建立支撑整个数学的公理系统，所不同的是：逻辑主义将数学归结为逻辑后，还想探寻逻辑规律后面的真理含义。形式主义不在乎它们是什么，甚至逻辑公理系统的公理也无所谓真假，只是约定的符号而已，关心的是它们组成系统的相容性，不自相矛盾是数学的终极意义。前者努力将数学建立在公理系统上，后者致力于公理系统的逻辑结构和推理的严谨性，最终发展了数理逻辑来指导这个建设。虽然他们的理性化目标都没有达到，但是，他们的公理化系统和对数学的基本主张成为现代数学的主导思想。

克劳威尔代表的直觉主义是一种有限主义的主张，不考虑无穷的数学对象，不允许使用无穷步骤的推理，不承认无穷领域使用排中律。否认选择公理，认为根据选择公理而作的集合，没有能行性，就不能承认其存在。认为数学对象必须是思维构造的产物，不能够被构造出来的概念不存在。不存在的否定不等于存在。这主张的一切都在直观可以想象的范围内，固然是安全可靠，但也把许多很有意义的结果排除在外。现代数学的构造主义撤销了直觉主义激进的主张，只坚持构造性的证明。

尽管集合论对无穷的研究被接受，受到有限主义的影响，人们对于无限领域的推理还是十分的谨慎。在无穷时的证明始终是数学家的心病，希尔伯特将大部分人公认的方法归纳为“有限化”的规则：证明是一个逻辑推理的过程，每一步只能是已知的定理，或根据前面有限个数学对象，按照逻辑的推论，推理的步骤必须是有限的。这里“有限”的意义来自法国年轻数学家厄布朗的总结：每一步证明只讨论确定的有限数目的对象及函数；这些对象及函数要能确定它们的真值产生协调一致的计算结果；一个对象如不指出如何构造它，就不能肯定其存在；必须永远不考虑一个无穷集体中所有对象的集合。

在无穷领域里的推理，数学家的关注有三个方面：逻辑规则，无限的数学对象和无限的推理过程。我们逐一来了解它们。

从最保守的有限主义到比较宽松的结构主义都反对在无穷的领域使用反证法，只允许使用归谬法。反证法是：先假设要证明定理的反命题成立，然后以此推出矛盾，否定了反命题，依照排中律，定理就必然成立。这样的证明是非构造性的，不能指出如何构造它，称为“存在性证明”。不承认排中律，就要放弃一大批数学成果，这是现代数学不能承受的牺牲。反证法在现代证明中已经广泛地使用。就像康托尔没有构造出一个超越数，就证明存在着不可数的超越数。现代数学承认反证法的证明，但更欣赏结构性证明的价值。归谬法是从前提中推出矛盾，以此来否定前提，可以用它得出否定性的结论。显然归谬法比反证法弱，反证法里包含着归谬法的环节，然后用否定之否定的还原律来完成证明。

古典的形式逻辑有同一律、矛盾律、排中律和充足理由律。归谬法只需要根据矛盾律，反证法需要根据矛盾律和排中律。这四条定律是古典形而上学的逻辑说法，在数理逻辑中命题逻辑的演绎规则被严格地规范在逻辑系统里研究（见【附录】），数理逻辑研究证明，反证律可以推出归谬律和还原律，后两者联合起来可以推出反证律。所以结构主义，不认为在无穷时，否定之否定就等于肯定。不存在的否定不等于存在。

现代数学基于集合论允许使用无穷作为数学的实体。有限主义禁止使用无穷的数学实体和过程。那后者怎么处理反映无穷多个关系，比如说从1加到N的累加公式证明？用数学归纳法。因为自然数是用归纳法来定义的，所以用数学归纳法来证明所有自然数具有某种性质的命题，是符合直觉的，是自明的。从集合论的观点，数学归纳法原理可以从自然数是良序集和反证法里得到证明。

数学归纳法定理：设S(n)是自然数为参数的逻辑命题，假如：a）S(1)是真的；b）对于任何n，S(n)为真，推出S(n+1)为真；则对于所有的n，S(n)为真。

证明：假如这结论不成立，因为自然数是良序集，让S(n)为假的数必定有最小的，记为k。因为a），k不可能是1；因为k是让S(n)为假的最小数，所以S(k-1)为真，根据2），推出S(k)为真。这与假设矛盾，定理得证。

注意，用数学归纳法证明的是潜无穷的无穷多个关系，比如说，下面运用数学归纳法证明是错误的。

集合{1}是有限集，假如{1,2,…,n}是有限集，那么多一个元素的{1,2,…,n,n+1}也是有限集，根据数学归纳法，这对所有n都成立，所以自然数的集合{1,2,3…}是个有限集。

数学归纳法证明了对于所有自然数成立的命题，是指对于任何（有限）的自然数，而不是自然数的全体（实无穷）。

哥德尔定理揭示了希尔伯特“有限化”证明的局限性，哥德尔定理里所说的“判定”或“证明”是指局限于使用公理系统里的公理和“有限化”方法的形式证明。哥德尔定理是使用了公理系统之外的“元数学”来证明的。哥德尔定理说“PM不能证明自身的相容性（consistency）。”这个事有点大。如果不能够用可信的方法证明集合论的无矛盾性(至少ZF系统无矛盾)和数学分析的无矛盾性，我们还有信心在这上面做研究吗？这里，最基本的当然是算术的无矛盾性。哥德尔的不完全性定理说明，用有限化的方法，这个目标是达不到的。希尔伯特引进证明论来研究这个问题。证明论又称元数学，它研究数学证明的合理性问题，是数理逻辑的一个分支。1935年，甘岑用超穷归纳法证明自然数算术形式系统的无矛盾性。几年后，他和其他人又给出了其他的证明。数学分析的无矛盾性，1967年由日本高桥元男用非构造性的方法证明。

超穷归纳法也称超限归纳法，有几种表达形式，一个是这样的：设S(x)是良序集Ω上序为参数的逻辑命题，假如：a）对Ω上最小元l，S(l)是真的；b）若所有x < y，S(x)为真，推出S(y)为真，则对于Ω上所有的x，S(x)为真。

不难看出数学归纳法只是超限归纳法的特殊情况，相同的方法可以证明它的正确性。超限归纳法是数学归纳法向良序集的推广，它的方法也不依赖于选择公理，但很多应用是无穷的偏序集，用到了选择公理可以将它良序化，或者直接用等价的Zorn引理。“有限化”要求“一个对象如不指出如何构造它，就不能肯定其存在”，限制了选择公理的应用。哥德尔定理之后，人们意识到“有限化”的局限，探索较宽的限制，比如说原来“有限化”对于无穷的对象只能用数学归纳法，现在倾向于接受“超穷归纳法”，它在无穷集合上被广泛应用，犹如数学归纳法在自然数上那样的犀利。

什么是无限的推理过程？比如说一个偶数能不能分解成两个素数的和，理论上逐个试过总是可以有个肯定或否定的答案，有人由此得出哥德巴赫猜想不是不可判定的。这其实相似于数论上的定理，理论上逐个试过总是可以有个肯定或否定的答案；计算机程序逐个试过总知道会不会停机。但这里的“试过”可能是一个无限的过程，是不能实现的，不合法。哥德尔的不可判定定理和图灵的停机问题都是否定了这样推理的结论。

哥德尔定理说明了现行演绎推理的局限。但放宽一些局限并不能解决哥德尔揭示的问题。就像归纳法中的“所有”只包含着趋向无穷的过程，而不包括无穷的极限，这是潜无穷和实无穷的区别。数学的推理不能使用无限的推理过程，就像无穷步的计算没有结果一样。哥德尔定理后，人们对解决这类古典难题的信念大减，现在对难题努力的意义是寻找新的思想方法。

数学不同流派的分歧在于不同的和谐信念和严谨性追求，人们总以为数学是枯燥冰冷的逻辑，实际上这些数学家争执的是抽象世界中美学的不同理解。G. H. Hardy说：“Beauty is the first test: there is no permanent place in the world for ugly mathematics.”

【附录】

数理逻辑中命题逻辑系统P，与大家熟悉的语言描述的命题逻辑系统等价，描述了数学里应用的命题逻辑演绎推理的规则。它由两个符号和三条形成规则定义合式公式：

1）单独一个命题词是合式公式；

2）如果X是合式公式，则┐X是合式公式；

3）如果X和Y是合式公式，则（X→Y）是合式公式。

记A1, …, An┣ A 为合式公式A1, …, An推出合式公式 A。P系统里有5条形式推理规则，它们严格地规范了命题逻辑的演绎运算。

（ε）A1, …, An┣ Ai(i=1,2,…,n)；肯定前提律。前提中每个命题都可以作为整个前提的结论。

（τ）如果Γ┣Δ┣ A（Δ不空）, 则Γ┣ A；演绎推理传递律。Γ和Δ分别是一组命题。

（┐）如果Γ, ┐A┣ B, ┐B, 则Γ┣ A；反证律。在Γ前提下，反命题推出错，得出在Γ前提下正命题成立。

（→-）A→B，A┣ B；蕴含词消去律。如果A则B，有A，推出B。（三段论推理）

（→+）如果Γ, A┣ B则Γ┣ A→B；蕴含词引入律。在Γ前提下，有A推出B，即Γ时，如果A则B。 

除了(┐)条即反证律外，其他4条都很基本。由反证律和其他条可以推出还原律（┐┐A┣ A）和归谬律（如果Γ, A┣ B, ┐B, 则Γ┣  ┐A）。反过来，由还原律和归谬律合起来可以推出反证律。

因为直觉主义等构造主义流派认为反证律太强，反对无条件使用，所以包含反证律的系统称为古典逻辑演算，包含减弱程度反证律的称为非古典逻辑演算。有几种非古典逻辑演算系统，在P中把反证律换作归谬律称为极小系统，在极小系统中加上推理规则（A, ┐A┣ B）称为海丁系统。这些弱化的逻辑系统在结构性证明中使用。