Introduction to clarithmetic. II (Q259084)

This is Part II of a series of three papers, whose Part I was [the author, ibid. 209, No. 10, 1312--1354 (2011; Zbl 1243.03075)] and Part III was [the author, Ann. Pure Appl. Logic 165, No. 1, 241--252 (2014; Zbl 1303.03089)]. Giving the good news that Part I is self-contained, the author warns that ``this article fully and heavily relies on the terminology, notation, conventions and technical results of its predecessor, with which the reader is assumed to be well familiar.'' ``The present paper constructs three new \textbf{CL12}-based systems: \textbf{CLA5}, \textbf{CLA6}, \textbf{CLA7} and proves their soundness and extensional completeness with respect to polynomial space computability, elementary recursive time (and/or space) computability, and primitive recursive time (and/or space) computability, respectively. While \textbf{CLA4} was already simple enough, the above three systems are even more so. All of them only need \(\sqcap x\sqcup y (y=x+1)\) as a single extra-Peano axiom. As before, the only logical rule is LC. And the induction rule (the only nonlogical rule) of each of these systems is \(\{F(0), F(x)\rightarrow F(x+1)\}\vdash\{F(x)\}\). The three systems differ from each other only in what (if any) conditions are imposed on the formula \(F(x)\) of induction. In \textbf{CLA5}, as in \textbf{CLA4}, \(F(x)\) is required to be polynomially bounded. \textbf{CLA6} relaxes this requirement and allows \(F(x)\) to be an exponentially bounded formula. \textbf{CLA7} takes this trend towards relaxation to an extreme and imposes no restrictions on \(F(x)\) whatsoever. This way, unlike \textbf{CLA4}, \textbf{CLA5} and \textbf{CLA6}, theory \textbf{CLA7} is no longer in the realm of bounded arithmetics.''