打造你自己的算术 II：正确性
摘要：基于可计算逻辑的清晰算术是一种数论。这些理论的公式代表了交互式计算问题，它们的“真实性”被理解为算法解决方案的存在。对这些解决方案的各种复杂性约束导致了各种版本的清晰算术。本文介绍了一种参数化/示意版本CLA11(P1, P2, P3, P4)。通过以基本机械方式调整参数P1、P2和P3，可以自动获得与广泛目标三重复杂性类相一致和完备的理论，即时间（由P3设置）、空间（由P2设置）和所谓的振幅（由P1设置）复杂性的组合。所谓的一致是指该系统的每个定理T代表一个交互的数论计算问题，其解决方案属于给定的三重复杂性类，并且此类解决方案可以从T的证明中自动提取出来。而完备则指该系统的每个具有解决方案属于给定三重复杂性类的交互式数论问题都可以由系统的一些定理来代表。此外，通过调整第四个参数P4，可以在不牺牲递归公理化的前提下加强所述外延完备性，根据该完备性，该系统的每个代表具有来自给定三重复杂性类的解决方案的问题的公式都是该系统的一个定理。本文刊登于两部分，前一部分第I部分介绍了该系统并证明了其完备性，而本文第II部分则专门证明了其一致性。
作者：Giorgi Japaridze (Department of Computing Sciences, Villanova University)
论文ID：1510.08566
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22