Introduction to clarithmetic. III (Q392285)

This is a continuation of the author's previous paper (Part I) [Inf. Comput. 209, No. 10, 1312--1354 (2011; Zbl 1243.03075)] and the unpublished manuscript (Part II) [``Introduction to clarithmetic. II'', Preprint, \url{arxiv:1004.3236}], familiarity with which is assumed for studying the present paper. The newly introduced arithmetical theories (based on computability logic) are called CLA8, CLA9 and CLA10 with the following properties: -- CLA8 is sound and complete with respect to PA-provably recursive-time computability (in the same sense as CLA7, studied in Part II, is sound and complete with respect to primitive recursive- time computability.) It augments CLA7 by the rule (1) \(\{F(x) \sqcup \neg F(x), \;\exists x F(x)\} / \{\sqcup x F(x)\}\) for elementary \(F(x)\). ``The story does not end with provably recursive-time computability though. Not all computable problems have recursive (let alone provably) time complexity bounds. In other words, not all computable problems are recursive-time computable. An example is \((\ast) \,\sqcap\!x\big(\exists y\,p(x,y)\rightarrow\sqcup y\,p(x,y)\big)\), where \(p(x,y)\) is a decidable binary predicate such that the unary predicate \(\exists y\, p(x,y)\) is undecidable (for instance, \(p(x,y)\) means `Turing machine \(x\) halts within \(y\) steps'). Problem \((\ast)\) is solved by the following effective strategy: Wait till Environment chooses a value \(m\) for \(x\). After that, for \(n=0,1,2,\cdots\), figure out whether \(p(m,n)\) is true. If and when you find an \(n\) such that \(p(m,n)\) is true, choose \(n\) for \(y\) in the consequent and retire. On the other hand, if there was a recursive bound \(\tau\) for the time complexity of a solution \({\mathcal M}\) of \((\ast)\), then the following would be a decision procedure for (the undecidable) \(\exists y\, p(x,y)\): Given an input \(m\) (in the role of \(y\)), run \({\mathcal M}\) for \(\tau(|m|+1)\) steps in the scenario where Environment chooses \(m\) for \(x\) at the very beginning of the play of \((\ast)\), and does not make any further moves. If, during this time, \({\mathcal M}\) chooses a number \(n\) for \(y\) in the consequent of \((\ast)\) such that \(p(m,n)\) is true, accept; otherwise reject.'' ``A next natural step on the road of constructing incrementally strong clarithmetical theories for incrementally weak concepts of computability is to go beyond PA-provably recursive-time computability and consider the weaker concept of constructively PA-provable computability of (the problem represented by) a sentence \(X\). The latter means existence of a machine \({\mathcal M}\) such that PA proves that \({\mathcal M}\) computes \(X\), even if the running time of \({\mathcal M}\) is not bounded by any recursive function.'' -- CLA9 is sound and complete with respect to constructively PA-provable computability. ``That is, a sentence \(X\) is provable in CLA9 if and only if it is constructively PA-provably computable. Deductively, CLA9 only differs from CLA8 in that, instead of (1), it has the following, stronger, rule:'' \(\{F(x)\sqcup\neg F(x)\} / \{\exists x F(x)\rightarrow\sqcup x F(x)\}\) for elementary \(F(x)\). -- CLA10 is sound and complete with respect to PA-provable computability. It augments CLA9 by the rule \(\{\exists x F(x)\} / \{\sqcup x F(x)\}\) where \(\exists x F(x)\) is an elementary sentence.