元数学

（metamathematics）亦称证明论，是数理逻辑和数学基础的一个分支。它研究数学证明的理论和规律。其主要内容包括一个理论系统的无矛盾性（亦称协调性、一致性、相容性）、完全性（亦称完备性）和独立性以及判定问题等。证明论是二十世纪前半叶由著名数学家希尔伯特提出并由他本人及合作者和他的学生最先发展起来的。证明论发端于对欧氏几何平行公理（见“欧几里德几何”）的研究，根据平行公理，要断定两条已知直线平行，必须把两条直线向两侧引到“无穷”，而且要断定它们在无限延长的整个范围内没有一处是相交的，这里有其困难之处。正是这种原因，从欧氏《几何原本》问世以来，人们便企图把平行公理降为定理，想用反证法来证明它。但是，采用与平行公理相反的断言展开推论，虽然得到了一些无法思议的结果，却始终没有引出逻辑矛盾。俄国数学家罗巴切夫斯基，总结了两千多年来人类探求平行公理奥秘的经验教训，于1826年指出：从欧几里德时代以来，两千年来徒劳无益的努力，促使我怀疑在概念本身之中并未包含大家想要证明的真实情况。他作出了两个明确的结论：第一，平行公理不能证明。第二，采用与平行公理相反的断言，可以展开一连串的推论，得到一连串的定理。尽管这些定理悖于人们的直觉观念，但它们并不包含矛盾。于是，一种新的几何——非欧几何诞生了。但是，断定罗氏平行公理不会导致矛盾，这是要严格证明的。1870年，德国数学家克莱因作出了一种证明，他用的是“解释法”。他把罗氏几何的点、线等解释为欧氏几何的某些图形。这样，罗氏几何的定理就一一对应地变成欧氏几何的定理了。如果罗氏几何中能推出矛盾，欧氏几何也就推出矛盾，反之也一样。罗氏几何的不矛盾性建立起来了，但这种不矛盾性只能叫相对不矛盾性，即罗氏几何是相对于欧氏几何不矛盾的，实际上这不过是把罗氏几何的不矛盾性转移为欧氏几何的不矛盾性，人们自然要追问欧氏几何是否没有矛盾，建立坐标系后，所有欧氏几何可借助于实数系统而用代数语言表示，欧氏几何的不矛盾性便可归结为实数系统的不矛盾性。实数系统的不矛盾性又可归于自然数系统的不矛盾性，这样追溯下去，必然出现下列情况，要证明其不矛盾的那个理论是最基本的理论，不能再归结到别的理论中去，这时必须作出绝对不矛盾性的证明。本世纪初，希尔伯特提出一个方法，即不再以点、线、面、数等数学概念作为研究对象，而把整个数学理论作为研究对象，目的是证明它没有矛盾。这时被研究的理论，也就是想证明其不矛盾的理论叫作对象理论（也就是原来意义的数学）。为证明其不矛盾性，又必须进行推理。进行推理所根据的理论，叫作元理论，又叫元数学。希尔伯特提出明确的要求，要使这种证明有意义，元数学应该狭于对象理论，换言之，只使用数学的一部分理论来证明整个数学的不矛盾性。同时，所使用的部分其不矛盾性应该是直觉上非常明确清楚，不容发生疑问的，这便是数学史上的有名的希尔伯特规划。开始，进展很顺利，人们以为整个数学的不矛盾性证明很快就会实现，可是不久，哥德尔于1931年证明了形式数论系统不完全性定理，进而又证明了要想用一个元数学去证明另一个对象理论的不矛盾，则对象理论不可能强于元数学，倒是元数学必须强于对象理论。这样以来，希尔伯特规划便根本不能实现了。但是，元数学作为专门研究理论系统的部门，继续存在和发展着。