计算与形式系统中确定性的来源

在他的《方法论》中，勒内·笛卡尔寻求“对生活中一切有用事物的清晰而确定的知识”。近三个世纪后，在《数学基础》中，大卫·希尔伯特试图“重新构造数学定义和推理，使其不可动摇”。希尔伯特的纲领明确依赖于形式系统（等价地，计算系统）来为数学提供确定性。计算和形式系统的概念在他那个时代尚未被定义，但笛卡尔的方法可以被理解为以本质上相同的方式寻求确定性。在本文中，我将形式系统解释为具体的人工制品，并研究它们提供高水平确定性——可以说是理性话语所能达到的最高水平——的方式。本世纪数学逻辑和计算机科学对形式系统的丰富理解阐明了诸如笛卡尔和希尔伯特等通过严格分析寻求确定性的纲领的性质。