*希尔伯特提出的解决协调性问题的方案。包括两个步骤：(1)对每个古典数学分支，建立一个模拟它的*形式系统，形式系统的对象是无任何意义的符号，数学命题的推导关系变成符号串的变化关系。在这形式系统中可以严格地推导出相应的古典数学分支中一切定理的形式表示式。在形式推导中有相当于排中律的变形规则。(2)用立足于有限观点（即涉及的讨论、判断或定义都必须限制在可以彻底给出的对象和可以彻底进行的过程上面）的有限方法，证明该形式系统的无矛盾性。1931年*哥德尔发表*不完全性定理，否定了该方案的某些设想。但方案所产生的有关方法对数理逻辑的发展起了很大作用。