经典逻辑中的一致可证明性

一致证明(uniform proofs)是相继式演算证明,具有以下特征:在证明的任何阶段推导复杂公式时,最后一步总是引入该公式的顶层逻辑符号。我们研究这一一致证明概念对于构建经典逻辑中证明搜索的相关性。若某逻辑语言在其语境下可证明性等价于一致可证明性,则它容许一种目标导向的证明过程,该过程将逻辑符号解释为搜索指令,其含义由相应的推理规则给出。虽然经典逻辑并不直接具有这一致可证明性质,我们证明:在对假设集做一项适度且可靠的修改——即向其中添加被证公式的否定——之后,它的一个片段具有该性质,该片段仅排除全称量词在本质上是正出现的情形。我们进一步指出,所添加公式的所有使用都可分解为某些导出规则。所得证明系统及其具有的一致可证明性质被用于勾勒一种经典逻辑的证明过程。该证明过程一个有趣的方面是,它将先前提出的用于处理假设中析取信息以及处理假设性(hypotheticals)的机制纳入其中。我们的分析阐明了这些机制与一致证明概念之间的关系。