[拼音]：Xi’erbote jihua
[外文]：Hilbert's program
又称证明论计划，是在20世纪初数学奠基问题的论战中，由D.希尔伯特提出的旨在保卫古典数学、避免悖论以解决数学奠基问题的一种方案。
20世纪初，悖论尤其是罗素悖论的出现，引起了当时数学界和逻辑界的极大震动。它直接冲击了以严谨著称的数学和逻辑学科，动摇了传统的数学概念、数学命题和数学方法的可信性标准，也就是说悖论的出现关系到整个数学的奠基问题，从而引起所谓第三次数学基础危机。
以L.E.J.布劳威尔为代表的直觉主义者（见数学基础）从他们的直觉主义数学观出发，否定实无穷，坚持‘存在’即被构造，排斥康托尔集合论和传统逻辑的排中律，否认古典数学中的大量的非构造性定义和纯存在性证明，从而摈弃了大部分古典数学成果。希尔伯特认为：这是不可取的，是“错误的途径”。他认为古典数学(包括康托尔集合论)是“我们最有价值的宝藏”，而传统逻辑中的“排中律”是普遍有效的，希望保存这种古典数学的“有成效的概念结构和推理方法”。也就是说，希尔伯特是希望保卫古典数学的。同时，希尔伯特也认为：“绝对无穷概念的命题确实是超越人们直观性证据之外”的东西，“是通过人们的心智过程被插入或外推出来的概念”。但是，数学的各个分支都涉及无穷集合，例如数学分析它在一定的意义上就是一首“无穷的交响乐”。可见，无穷在思维过程中是不可缺少的，应有其适当的位置。由于无穷不能在经验中直接验证，故希尔伯特称之为理想元素，并将古典数学中以实无穷为前提的命题称做理想命题，反之将有直观意义的命题称做现实命题。希尔伯特认为：理想元素方法在数学中是常用的，行之有效的方法。如在几何中引进了无穷远点以后，不仅有“两不同点可决定惟一直线”而且还可以有“两不同直线可以决定惟一的一个点”。在代数中引进了虚数 i以后，就可以简化方程式根的定理，因此尽管理想元素可能没有意义，但是由它可以推出有意义的元素和定理来，并可以简化理论结构。希尔伯特从而将古典数学分成涉及实无穷的“理想数学”和以“有穷主义”为特征的现实数学（即构造性数学）。希尔伯特与他的弟子P.贝尔奈斯曾对“有穷主义”一词作如下解释：“我们常用‘有穷’一词放在别的表达式之前，表示有关的考虑，断言或定义均限于基本上可以想象的对象以及基本上可以完成的过程，从而可以在具体处理的范围内加以完成。”简言之，希尔伯特的有穷方法是指不涉及实无穷的、直观上明显可靠的、能在有穷步骤内根据确定的机械的办法实施的，并可终结。希尔伯特认为：产生悖论的原因不在于“实无穷”，而在于对“实无穷”的错误认识；问题不在于使用理想元素，而在于说明使用理想元素不会带来矛盾。实际上，希尔伯特所创立的形式公理法当时已被广泛沿用，E.F.F.策梅洛据以建立的第一个集合论公理系统即公理集合论已能排斥已知集论悖论，同时又能发展集论中原有合理的有效内容，所以问题确实在于进一步说明不会产生新的悖论。
在希尔伯特看来，每一门数学都可以看成基于它的公理的一个演绎系统，它们是根本不会产生逻辑矛盾的，亦即是协调的。数学的可靠性就在于它的协调性（即无矛盾性）。协调性问题在非欧几里得几何学创立时曾经讨论过，当时为了证得非欧几何的协调性是把它化归到欧氏几何的协调性，即如果欧氏几何无矛盾则非欧几何亦无矛盾。这是一种相对的证明方法，若要证明整个数学无矛盾，就不能再用这种化归的方法，而是要求给出“绝对的”证明。为此，希尔伯特提出了著名的证明论计划，其基本内容为：
（1）将所要讨论的古典数学理论T（有内容的）（如数论）公理化，把所得的公理化理论和所用的逻辑彻底地形式化，使得有内容的古典数学理论T（如数论）能表成一些形式符号和形式符号公式(它们是没有内容的)组成的系统，记为TF，TF形式地摹写了T中的现实命题和理想命题以及其间的逻辑关系。这种形式符号系统TF称为T的形式理论（如形式数论），TF是作为一种独立结构而存在的，它使得表达现实命题和理论命题在方法上协调起来成为可能，并且使得所用的逻辑也可以得到一个“确切、科学的处理”。通过对形式理论TF的协调性的研究来建立原来的古典数学理论T的可靠性。
（2）由于研究形式理论TF时需要用到逻辑和数论，故希尔伯特建议采用有穷方法来建立一个逻辑系统和初等数论，以便与经典逻辑和普通数论相区别，从而避免循环论证。这样建立起来的逻辑和数论，希尔伯特称之为元数学（见证明论）。将用Tm来讨论TF的协调性，Tm中的符号和公式是有内容的。对TF的讨论采用构造的方法，不得涉及实无穷。这一点希尔伯特与布劳威尔是一致的。
（3）用元数学Tm来证明在形式理论TF中，不会有某个论断A与其否定塡A同时可以推出，也就是证明形式理论TF的协调性。如能证得TF的协调性就可以保证所代表的古典数学理论T不会产生矛盾。换言之，如果形式理论TF的协调性能够元数学地证明，则TF所摹写的古典数学理论及其理想命题都可以保留。
这就是希尔伯特证明论计划的主要步骤。
希尔伯特在计划中区分了三种数学理论。第一种是古典的（即普通的）数学理论T，T是直观的、非形式的，T 中的符号和公式都是有内容的。第二种是形式数学理论TF，TF是一个形式符号系统，它是第一种数学理论的形式化，将通过证明TF的协调性来建立古典数学的可信性，TF通称为对象理论，对象理论TF中的符号和公式都是没有内容的、纯形式的，但TF的系统特征(如协调性)即可用符号排列的组合来表述。第三种数学理论Tm是用来描述和研究第二种数学理论的，希尔伯特称Tm为元数学或证明论，在元数学中，人们应按前述的“有穷主义”办事。也就是说，希尔伯特认为可信性只存在于有限之中，而理想元素只是理性规定而已。这一点他与直觉主义是相通的，并将这一观点贯彻在元数学中。其目的在于证明对象理论的协调性。从而给出TF所代表的古典数学理论T的无矛盾性的绝对证明。
希尔伯特在他的计划中强调了两个原则：其一为彻底地形式化；其二为有穷主义。无前者则一门古典数学理论及其所用的逻辑将无从得到精确表达，因而不能成为确定的研究对象；无后者则难以保证所用工具不超过系统TF内所有的工具，无法避免循环论证。
希尔伯特在他的计划中突出了一个目的：要通过元数学Tm来证明对象理论TF的协调性，以说明TF所代表的古典数学理论T是不会产生矛盾的，从而保卫古典数学成果。
希尔伯特计划约在1922年问世，曾经引起相当普遍的重视，吸引了许多数学家（包括象哥德尔这样的大数学家）为促其实现而努力。一些较为简单的对象理论，诸如命题演算，一阶谓词演算，只含加法的算术等的协调性已被先后证得，这些工作促进了数理逻辑的发展也增强了对计划的信心。但是1931年K.哥德尔发表了著名的不完备性定理（见哥德尔不完备性定理）；这给希尔伯特的证明论计划以沉重打击。希尔伯特本人虽因此而感到震惊，但并不认为自己的计划已被否定，而认为只需将有穷方法加以扩充，再增加超限归纳法作为证明论的工具，原计划还是可行的。1936年G.根岑用超限归纳法证明了纯数论的协调性，但这已不是希尔伯特原来的计划。希尔伯特的计划虽然未能实现，但它对现代数学的发展有很大贡献。
（1）它创立了元数学（证明论），在使用了公理化方法和形式化方法以后，它第一次使一门数学理论整体地作为一个确定的、可用数学方法来研究的研究对象；它使得用来说明古典数学理论无矛盾的、形式理论的协调性能予精确表示；它使得现实命题和理想命题表达方法的一致成为可能。这些都是超越前人、令人钦服的新思想。同时，事实证明，这样把一种理论整体地作为研究对象用另一种理论加以研究是很有成效的。常常能够得到许多新的见解。这对现代数学和计算机科学的发展都是很有意义的。
（2）希尔伯特在计划中提出了一个可信性标准:数学的可信性在于它的协调性。与其同时代的布劳威尔或罗素的主张相比较，这更易为大多数的数学家所乐于接受。所以，当希尔伯特计划问世后，曾经吸引相当多的追随者为之奋斗。特别是哥德尔原来也是想实现希尔伯特计划的，但在实践中发现这是不可行的，而后他才建立了著名的不完备性定理。这就是说，哥德尔原来也是赞同希尔伯特的可信性标准的。不完备性定理这一划时代成果是在实践这一标准的过程中发现的。
（3）希尔伯特在计划中所倡导的有穷主义的构造方法即是一种以有穷主义为特征的构造性数学研究。这也是现代构造性数学的一支。这一研究曾为希尔伯特的弟子贝尔奈斯和克莱塞等的工作所继续发展。
（4）使用元数学方法，对于数理逻辑本身亦有很大推动。英国的帕里斯等由此得出了新的不可判定问题。他们发现了一个在皮亚诺算术中既不能证明也不能否证的纯粹的组合问题，它不仅给哥德尔不完备性定理一个具体实例，而且使人怀疑要解决许多尚未解决的数论难题，可能是白费力气，应另作他图。
总之，希尔伯特的计划虽然没有实现，但它对现代数学的发展有很大的促进作用。希尔伯特企图把有穷主义观点下的构造性与涉及实无穷的理想元素在应用上的有效性统一起来，这一愿望虽然不能实现，但在它的直接影响、启迪和促进下，推动了大量的新思想、新见解和新知识的出现，并且创建了象元数学这样重要的、有深远影响的新分支，这对现代数学的发展很有贡献。元数学（证明论）作为数理逻辑的重要分支正生气勃勃地发展着。