Introduction to clarithmetic. I (Q642523)

In this paper the author introduces an(other) arithmetical theory based on his computability logic (CoL), which is an analogue of Peano arithmetic (based on classical logic). CoL, as the author puts it, is ``a semantical, mathematical and philosophical platform, and a long-term program, for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth which logic has more traditionally been.'' The author also notes in the introduction of the paper that ``the main value of CoL \dots will eventually be determined by whether and how it relates to the outside, extra-logical world.'' ``Unlike the mathematical or philosophical constructivism, however, and even unlike the early-day theory of computation, modern computer science has long understood that, what really matters, is not just \textit{computability}, but rather \textit{efficient computability}.'' In his earlier paper [``Towards applied theories based on computability logic'', J. Symb. Log. 75, No. 2, 565--601 (2010; Zbl 1201.03055)] the author introduced the CoL-based arithmetic \textbf{CLA1}, in which ``every formula expresses a number-theoretic computational \textit{problem} (rather than just a true/false \textit{fact}), every theorem expresses a problem that has an algorithmic solution, and every proof encodes such a solution.'' That system ``proves formulas expressing computable but often intractable arithmetical problems.'' ``A purpose of the present paper is to construct a CoL-based system for arithmetic which, unlike \textbf{CLA1}, proves only efficiently -- specifically, polynomial time -- computable problems. The new applied formal theory \textbf{CLA4} presented in Section 11 achieves this purpose.'' The author proves the soundness of \textbf{CLA4} and also what he calls \textit{extensional completeness} of the theory, in the sense that ``every number-theoretic computational problem that has a polynomial time solution is expressed by some theorem of \textbf{CLA4}.'' It is noted that this is weaker than \textit{intensional completeness}, which amounts to ``any formula representing an (efficiently) computable problem is provable.'' (Intentional completeness of \textbf{CLA4} has not been proven in the paper -- it might not hold.) ``Syntactically, our \textbf{CLA4} is an extension of \textbf{PA}, and the semantics of the former is a conservative generalization of the semantics of the latter.'' In the final section, the author notes that ``Both classical-logic-based and intuitionistic-logic-based systems of bounded arithmetic happen to be \textit{inherently weak} theories, as opposed to our CoL-based version, which is as strong as Gödel's incompleteness phenomenon permits, and which can be indefinitely strengthened without losing computational soundness.'' The paper is rather long and requires familiarity with the earlier works of the author where CoL was introduced and developed.