一句话:提出参数化理论 CLA11,通过调参得到相对于三复杂度类的可靠且完备算术系统,并证明完备性。
论文研究基于可计算逻辑的 clarithmetic 数论:公式表示交互式计算问题,真即存在算法解;对解施加复杂度约束可得到不同版本。作者引入参数化系统 CLA11(P1,P2,P3,P4),其中 P1、P2、P3 分别控制振幅、空间与时间复杂度。近乎机械地调节前三个参数,可针对广泛的三复杂度类自动获得可靠且完备的理论:可靠指每个定理表示的问题都有该类中的解,且解可从证明自动抽取;完备指该类中每个可解问题都由某定理表示。调节 P4 可在放弃递归可公理化但保持简洁优雅的代价下,将外延完备性强化为内涵完备性。本文为第一部分,引入系统并证明完备性;可靠性留待第二部分。
Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a parameterized/schematic version CLA11(P1,P2,P3,P4). By tuning the three parameters P1,P2,P3 in an essentially mechanical manner, one automatically obtains sound and complete theories with respect to a wide range of target tricomplexity classes, i.e. combinations of time (set by P3), space (set by P2) and so called amplitude (set by P1) complexities. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a solution from the given tricomplexity class and, furthermore, such a solution can be automatically extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a solution from the given tricomplexity class is represented by some theorem of the system. Furthermore, through tuning the 4th parameter P4, at the cost of sacrificing recursive axiomatizability but not simplicity or elegance, the above extensional completeness can be strengthened to intensional completeness, according to which every formula representing a problem with a solution from the given tricomplexity class is a theorem of the system. This article is published in two parts. The present Part I introduces the system and proves its completeness, while Part II is devoted to proving soundness.