(CoL)

Section 7

Clarithmetic (CoL-based arithmetic) 

          7.1   Introduction

        7.2   Clarithmetic versus bounded arithmetic

        7.3   Motivations

        7.4   Common preliminaries for all our theories of clarithmetic

        7.5   Clarithmetics for polynomial time, polynomial space, elementary and primitive recursive computability

        7.6   Clarithmetics for provable computability

        7.7   Tunable clarithmetic 

7.1 Introduction

As we agreed earlier, the ultimate purpose of logic is providing a tool for navigating the real life. As such, first and foremost it should be able to serve as a basis for applied (“substantial”) theories, one of the best known examples of which is Peano arithmetic PA. Pure logics, such as classical logic or CL12, are “about everything”, with no specific interpretation applied to their otherwise meaningless nonlogical atoms. For this reason, a formula of a pure logic can be valid or invalid, but not true or false. In contrast, an applied theory always comes with a particular interpretation, which makes all its atoms meaningful, and all sentences “true” or “false” (in our case meaning computable or incomputable). To make this point more clear to a computer scientist, pure logics can be compared with programming languages, and applied theories based on them with application programs written in those languages. A programming language created for its own sake, mathematically or esthetically appealing but otherwise unusable as a general-purpose, comprehensive and convenient tool for writing application programs, will hardly be of much interest.

In this respect, CoL is a reasonable alternative to classical logic. One can base applied theories on CoL just as meaningfully as on classical logic (and certainly more meaningfully than on intuitionistic or linear logics which offer no concept of truth), but with significant advantages, especially if we care about constructive, computational and complexity-theoretic aspects of the theory. Number theories based on CoL are called “Clarithmetics”. 

The nonlogical axioms of a clarithmetic generally will be a collection of (formulas expressing) problems whose algorithmic solutions are known. Often, together with nonlogical axioms, we also have nonlogical rules of inference, preserving the property of computability. Then, the soundness of the corresponding underlying axiomatization of CoL --- which usually comes in the strong, constructive sense --- guarantees that every theorem T of the theory also has an algorithmic solution and that, furthermore, such a solution can be mechanically extracted from a proof of T. Does not this look like exactly what the constructivists have been calling for?

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 computability but rather efficient computability. And here comes the good news: CoL, without any modifications whatsoever, can be used for studying efficient or complexity-conscious computability just as successfully as for studying computability-in-principle. This is no surprise. Let us take the fragment CL12 of CoL for specificity. As we saw from Theorem 6.7.4, CL12 is a sound and complete logic of not only (1) computability-in-principle, but also of (2) linear amplitude, constant space and linear time computability. This means it is also a logic of any sort of computability between these two extremes. If different sorts of computability required different versions of CoL, then CoL would not be universal enough, and thus would not quite be a Logic with a capital “L”.  It would be no fun to develop a separate “logic” for each of the so many interesting classes from the complexity zoo.

But if CoL does not differentiate between various sorts of computational complexity, then how could it be useful for studying them? The whole point is that the differences between clarithmetical theories tailored to various complexity classes should be and is achieved due to differences in the non-logical postulates of those theories rather than the underlying logic. Roughly speaking, if the nonlogical axioms of a clarithmetic represent problems computable within a given complexity constraints and if the nonlogical inference rules preserve this property, then CoL as a pure logic is gentle  enough to guarantee that all theorems of the theory also enjoy the same property. Of course, any very weak logic --- take the empty logic as an extreme --- would also have this “virtue”. But CoL is as strong as a logic could be and, as we are going to see later, it allows us to achieve not only soundness but also completeness of clarithmetics based on it. Here we should differentiate between two --- extensional and intensional --- sorts of completeness for clarithmetical theories. Extensional completeness with respect to a given complexity class C means that every problem with a C-complexity solution is represented (expressed) by some theorem of the theory, while intensional completeness means that every sentence expressing a problem with a C-complexity solution is a theorem of the theory. Note that intensional completeness implies extensional completeness but not vice versa, because a problem may be expressed via different sentences, some of which might be provable and some not.  Goedel’s celebrated theorem is about intensional rather than extensional incompleteness. In fact, in the context of PA or other classical-logic-based theories, extensional completeness is not interesting at all. It is trivially achieved there because the provable sentence 0=0 represents all true sentences. In clarithmetics usually both sorts of completeness can be achieved, even though, due to the Goedel incompleteness phenomenon, intensional completeness can only be achieved at the expense of sacrificing recursive enumerability (but not simplicity or elegance). 

By now eleven clarithmetical theories, named CLA1 through CLA11, have been introduced and studied [Jap10,  Jap11c,  Jap14,  Jap16a,  Jap16b,  Jap16c]. These theories are notably simple: most of them happen to be conservative extensions of PA whose only non-classical axiom is the sentence xy(y = x')  asserting computability of the successor function ', and whose only non-logical rule of inference is “constructive induction”, the particular form of which varies from system to  system. The diversity of such theories is typically related to different complexity conditions imposed on the underlying concept of interactive computability. For instance, CLA4 soundly and completely captures the set of polynomial time solvable interactive number-theoretic problems,^[Jap11c]  CLA5 does the same for polynomial space,^[Jap16a]  CLA6 for elementary recursive time (=space), ^[Jap16a]  and CLA7 for primitive recursive time (=space). ^[Jap16a]   Most interesting is the system CLA11, which, due to having four parameters, is in fact a scheme of clarithmetical theories rather than a particular theory. Tuning its parameters in an essentially mechanical way, CLA11 yields sound and complete systems for an infinite and diverse class of computational complexities, including those to which the earlier disparate systems of clarithmetic were tailored. Parameters #1, #2 and #3 are sets of terms or pseudoterms used as bounds in certain postulates, and parameter #4 is a (typically empty yet “expandable”) set of formulas used as supplementary axioms. The latter determines the intensional strength of the theory, while parameters #1, #2 and #3 respectively govern the amplitude, space and time complexities of the problems represented by the theorems of the theory. 

The logical basis of all clarithmetical theories studied so far is CL12.  More expressive fragments of CoL can be considered in the future for this purpose, if the syntax of such fragments is sufficiently developed.

7.2 Clarithmetic vs. bounded arithmetic

It has been long noticed that many complexity classes can be characterized by certain versions of arithmetic. Of those, systems of bounded arithmetic^{[Haj93, Kra95]}  should be named as the closest predecessors of our systems of clarithmetic. Just like our clarithmetical systems, they control computational complexity by explicit resource bounds attached to quantifiers, usually in induction or similar postulates. The best known alternative line of research, primarily developed by recursion theorists, controls computational complexity via type information instead. Here we will not attempt any comparison with these alternative approaches because of big differences in the defining frameworks.

The story of bounded arithmetic starts with Parikh's 1971 work [Par71], where the first system  IΔ₀ of bounded arithmetic was introduced. Paris and Wilkie, in [Par85] and a series of other papers, advanced the study of IΔ₀ and of how it relates to complexity theory. Interest towards the area dramatically intensified after the appearance of Buss' 1986 influential work [Bus86], where systems of bounded arithmetic for polynomial hierarchy, polynomial space and exponential time were introduced. Clote and Takeuti [Clo92], Cook and Nguyen [Coo10] and others introduced a host of theories related to other complexity classes. 

All theories of bounded arithmetic are weak subtheories of PA, typically obtained by imposing certain syntactic restrictions on the induction axiom or its equivalent, and then adding some old theorems of PA as new axioms to partially bring back the baby thrown out with the bath water. Since the weakening of the deductive strength of PA makes certain important functions or predicates no longer definable, the non-logical vocabularies of these theories typically have to go beyond the original vocabulary {0, ',+,✕} of PA. These theories achieve soundness and extensional completeness with respect to the corresponding complexity classes in the sense that a function f(x) belongs to the target class if and only if it is provably total in the system --- that is, if there is a Σ₁-formula F(x,y) that represents the graph of f(x), such that the system proves x!yF(x,y).

Here we want to point out several differences between clarithmetic and bounded arithmetic.

7.2.1. Generality While bounded arithmetic and the other approaches are about functions, clarithmetics are about interactive problems, with functions being nothing but special cases of the latter. This way, clarithmetics allow us to systematically study not only computability in its narrow sense, but also many other meaningful properties and relations, such as, for instance, various sorts of enumerabilities, approximabilities or reducibilities. As we remember, just like function effectiveness, such relations happen to be special cases of our broad concept of computability. Having said that, the differences discussed in the subsequent paragraphs of this subsection hold regardless of whether one keeps in mind the full generality of clarithmetics or restricts attention back to functions  only, the “common denominators” of the two approaches.

7.2.2. Intensional strength Our systems extend rather than restrict PA. Furthermore, instead of PA, as a classical basis one can take anything from a very wide range of sound theories, beginning from certain weak fragments of PA and ending with the absolute-strength theory Th(N) of the standard model of arithmetic (the “truth arithmetic”). It is exactly due to this flexibility that we can achieve not only extensional but also intensional completeness --- something inherently unachievable within the traditional framework of bounded arithmetic, where computational soundness by its very definition entails deductive weakness.

7.2.3. Language Due to the fact that our theories are no longer weak, there is no need to have any new non-logical primitives in the language and the associated new axioms in the theory: all recursive or arithmetical relations and functions can be expressed through 0, ',+,✕  in the standard way. Instead, the languages of the theories CLA1-CLA11 of clarithmetic only have the two additional logical connectives  ,   and two additional quantifiers , . It is CoL’s constructive semantics for these operators that allows us to express nontrivial computational problems. Otherwise, formulas not containing these operators --- formulas of the traditional language of PA, that is --- only express elementary problems (moveless games). This explains how our approach makes it possible to reconcile unlimited deductive strength with computational soundness. For instance, the formula xyF(x,y) may be provable even if F(x,y) is the graph of a function which is “too hard” to compute.  This does not have any relevance to the complexity class characterized by the theory because the formula xyF(x,y), unlike its “constructive counterpart” xyF(x,y), carries no nontrivial computational meaning.

7.2.4. Quantifier alternation Our approach admits arbitrarily many alternations of bounded quantifiers in induction or whatever similar postulates, whereas the traditional bounded arithmetics are typically very sensitive in this respect, with different quantifier complexities yielding different computational complexity classes.

7.2.5. Uniformity As already pointed out, our system CLA11 offers uniform treatments of otherwise disparate systems for various complexity classes. It should be noted that the same holds for the bounded-arithmetic approach of [Coo10], albeit for a rather different spectrum of complexity classes. The ways uniformity is achieved, however, are drastically different. In the case of [Coo10], the way to build your own system is to add, to the base theory, an axiom expressing a complete problem of the target complexity class. Doing so thus requires quite some nontrivial complexity-theoretic knowledge. In our case, on the other hand, adequacy is achieved by straightforward, brute force tuning of the corresponding parameters of CLA11. E.g., for linear space, we simply need to take parameter #2 to be the set of (0, ',+)-combinations of variables, i.e., the set of terms that “canonically” express the linear functions. If we (simultaneously) want to achieve adequacy with respect to polynomial time, we shall (simultaneously) take parameter #3 to be the set of (0, ',+,✕)-combinations of variables, i.e., the set of terms that express the polynomial functions. And so on.

7.3 Motivations

The main motivations for studying clarithmetics are as follows, somewhat arbitrarily divided into the categories “general”, “theoretical” and “practical”.

7.3.1. General Increasingly loud voices are being heard^[Gol06]  that, since the real computers are interactive, it might be time in theoretical computer science to seriously consider switching from Church’s narrow understanding of computational problems as functions to more general, interactive understandings. Clarithmetics serve the worthy job of lifting “efficient arithmetics” to the interactive level. Of course, the already existing results are only CoL’s first modest steps in this direction, and there is still a long way to go. In any case, our generalization from functions to interaction appears to be beneficial even if, eventually, one is only interested in functions, because it allows a smoother treatment and makes our systems easy-to-understand in their own rights. Imagine how awkward it would be if one had tried to restrict the language of classical logic only to formulas with at most one alternation of quantifiers because more complex formulas seldom express things that we comprehend or care about, and, besides,  things can always be Skolemized anyway. Or, if mankind had let the Roman-European tradition prevail in its reluctance to go beyond positive integers and accept 0 as a legitimate quantity, to say nothing about the negative, fractional, or irrational numbers.

The “smoothness” of our approach is related to the fact that, in it, all formulas --- rather than only those of the form x!yF(x,y) with F∈Σ₁ --- have clearly defined meanings as computational problems. This allows us to apply certain systematic and scalable methods of analysis that otherwise would be inadequate. For instance, the soundness proofs for various clarithmetical theories go semantically by induction on the lengths of proofs, by showing that all axioms have given complexity solutions, and that all rules of inference preserve the property of having such solutions. Doing the same is impossible in the traditional approaches to bounded arithmetic (at least those based on classical logic), because not all intermediate steps in proofs will have the form x!yF(x,y) with F∈Σ₁. It is no accident that, to prove computational soundness, such approaches usually have to appeal to syntactic arguments that are around “by good luck”, such as cut elimination.

As mentioned, our approach extends rather than restricts PA. This allows us to safely continue relying on our standard arithmetical intuitions when reasoning within clarithmetic, without our hands being tied by various constraints, without the caution necessary when reasoning within weak theories. Generally, a feel for a formal theory and a “sixth sense” that it takes for someone to comfortably reason within the theory require time and efforts to develop. Many of us have such a “sixth sense” for PA but not so many have it for weaker theories. This is so because weak theories, being artificially restricted and thus forcing us to pretend that we do not know certain things that we actually do know, are farther from a mathematician’s normal intuitions than PA is. Even if this was not the case, mastering the one and universal theory PA is still easier and promises a greater payoff than trying to master tens of disparate yet equally important weak theories that are out there. 

7.3.2. Theoretical Among the main motivations for studying bounded arithmetics has been a hope that they can take us closer to solving some of the great open problems in complexity theory, for, quoting Cook and Nguen [Coo10], “it ought to be easier to separate the theories corresponding to the complexity classes than to separate the classes themselves”. The same applies to our systems of clarithmetic and CLA11 in particular which allows us to capture, in a uniform way, a very wide and diverse range of complexity classes.  

While the bounded arithmetic approach has been around and extensively studied since long ago, the progress towards realizing the above hope has been very slow.  This fact alone justifies all reasonable attempts to try something substantially new and so far not well explored. The clarithmetics line of research qualifies as such. Specifically, studying “nonstandard models” of clarithmetics, whatever they may mean, could be worth the effort.

Among the factors which might be making clarithmetics more promising in this respect than their traditional alternatives is that the former achieves intensional completeness while the latter inherently have to settle for merely extensional completeness. Separating theories intensionally is generally easier than separating them extensionally, yet intensional completeness implies that the two sorts of separation mean the same. 

Another factor relates to the ways in which theories are axiomatized in uniform treatments, namely, the approach of CLA11 versus that of [Coo10]. As noted earlier, the uniform method of [Coo10] achieves extensional completeness with respect to a given complexity class by adding to the theory an axiom expressing a complete problem of that class. The same applies to the method used in [Clo92]. Such axioms are typically long formulas as they carry nontrivial complexity-theoretic information.  They talk --- through encoding and arithmetization --- about graphs, computations, etc. rather
than about numbers. This makes such axioms hard to comprehend directly as number-theoretic statements, and makes the corresponding theories hard to analyze. This approach essentially means translating our complexity-theoretic knowledge into arithmetic. For this reason, it is likely to encounter the same kinds of challenges as the ordinary, informal theory of computation does when it comes to separating complexity classes.  Also, oftentimes we may simply fail to know a complete problem of a given, not very well studied, complexity class.

The uniform way in which CLA11 axiomatizes its instances is very different from the above. Here all axioms and rules are “purely arithmetical”, carrying no direct complexity-theoretic information. This means that the number-theoretic contents of such theories are easy to comprehend, which, in turn, carries a promise that their model theories might be easier to successfully study, develop and use in proving independence/separation results.

7.3.3. Practical More often than not, the developers of complexity-bound arithmetics have also been motivated by the potential of practical applications in computer science. Here we quote Schwichtenberg's [Sch06] words:  ‘It is well known that it is undecidable in general whether a given program meets its specification. In contrast, it can be checked easily by a machine whether a formal proof is correct, and from a constructive proof one can automatically extract a corresponding program, which by its very construction is correct as well. This at least in principle opens a way to produce correct software, e.g. for safety-critical applications. Moreover, programs obtained from proofs are “commented” in a rather extreme sense. Therefore it is easy to apply and maintain them, and also to adapt them to particular situations.’ In a more ambitious and, at this point, somewhat fantastic perspective, after developing reasonable theorem-provers, CoL-based efficiency-oriented systems can be seen as declarative programming languages in an extreme sense, where human “programming” just means writing a formula expressing the problem whose efficient solution is sought for systematic usage in the future. That is, a program simply coincides with its specification. The compiler’s job would be finding a proof (the hard part) and translating it into a machine-language code (the easy part). The process of compiling could thus take long but, once compiled, the program would run fast ever after.

What matters in applications like the above, of course, is the intensional rather than extensional strength of a theory. The greater that strength, the better the chances that a proof/program will be found for a declarative, ad hoc or brute force specification of the goal. Attempts to put an intensionally weak theory (regardless of its extensional strength) to practical use would usually necessitate some pre-processing of the goal, such as expressing it through a certain standard-form Σ₁-formula. But this sort of pre-processing often essentially means already finding --- outside the formal system --- a solution of the target problem or, at least, already finding certain insights into such a solution. 

In this respect, CLA11 is exactly what we need. Firstly, because it is easily, “mechanically” adjustable to a potentially infinite variety of target complexities that one may come across in real life. It allows us to adequately capture a complexity class from that variety without any preliminary complexity-theoretic knowledge about the class, such as knowledge of some complete problem of the class (yet another sort of “pre-processing”) as required by the approaches in the style of [Clo92] or [Coo10]. All relevant knowledge about the class is automatically extracted by the system from the definition (ad hoc description) of the class, without any need to look for help outside the formal theory itself. Secondly, and more importantly, CLA11 fits the bill because of its intensional strength, which includes the full deductive power of PA and which is only limited by the Goedel incompleteness phenomenon. Even when the theory possesses no arithmetical knowledge on top of what is implied by the Peano axioms, is still provides “practically full” information about computability within the corresponding complexity constraints. This is in the same sense as PA, despite Goedel’s incompleteness, provides  “practically full” information about arithmetical truth. Namely, if a formula F is not provable in the theory, it is unlikely that anyone would find an algorithm solving the problem expressed by F within the required complexity restrictions: either such an algorithm does not exist, or showing its correctness requires going beyond ordinary combinatorial reasoning formalizable in PA.

7.4 Common preliminaries for all our theories of clarithmetic

All systems of clarithmetic presented on this website have the same language, obtained from the language of CL12  by removing all nonlogical predicate letters, removing all constants but 0, and removing all but the following three function letters:

• successor, unary. We write tʹ for successor(t).
• sum, binary. We write t₁+t₂ for sum(t₁,t₂).
• product, binary. We write t₁✕t₂ for product(t₁,t₂).

Let us call this language L. Throughout the rest of Section 7, unless otherwise specified or implied by the context, when we say “formula”, it is to be understood as formula of L. As always, sentences are formulas with no free occurrences of variables. An L-sequent is a sequent all of whose formulas are sentences of L. For a formula F, F means the -closure of F, i.e., x₁…x_nF, where x₁,…,x_n are the free variables of F listed in their lexicographic order. Similarly for F, F, F.  

A formula is said to be elementary iff it contains no choice operators. We will be using the lowercase p, q,… as metavariables for elementary formulas. This is as opposed to the uppercase letters E,F,G,…, which will be used as metavariables for any (elementary or nonelementary) formulas.

As one can see, L is an extension of the language of PA  --- namely, the extension obtained by adding the choice operators , , , . The language of PA is the elementary fragment of L, in the sense that formulas of the former are nothing but elementary formulas of the latter. We remind the reader that, deductively, PA is the theory based on classical first-order logic with the following nonlogical axioms, that we shall refer to as the Peano axioms:

1. x (0≠xʹ)
2. xy (xʹ=yʹ  x=y)
3. x (x+0=x)
4. xy (x+yʹ = (x+y)ʹ)
5. x (x✕0 = 0)
6. xy (x✕yʹ = (x✕y) + x)
7. (p(0)  x (p(x) p(xʹ)) x p(x)) for each elementary formula p(x)

The concept of an interpretation explained in Section 5.2 can now be restricted to interpretations that (as functions) are only defined on ʹ, + and ✕, as the present language L has no other nonlogical function or predicate letters. Of such interpretations, the standard interpretation ^† is the one whose universe  is the standard universe and which interprets  the letter ʹ as the standard successor function var₁+1, interprets + as the sum function var₁+var₂,  and interprets ✕ as the product function var₁✕var₂. We often terminologically identify a formula F with the game F^†, and typically write F instead of F^† unless doing so may cause ambiguity. Correspondingly, whenever we say that an elementary sentence is true, it is to be understood as that the sentence is true under the standard interpretation, i.e., is true in what is more commonly called the standard model of arithmetic.

Terminologically we will further identify natural numbers with the corresponding decimal numerals (constants). Usually it will be clear from the context whether we are talking about a number or a decimal numeral. For instance, if we say that x is greater than y, then we obviously mean x and y as numbers; on the other hand, if we say that x is longer than y, then x and y are seen as numerals. Thus, 999 is greater but not longer than 100.

All theories of clarithmetic presented in the following subsections share not only the language L but also logical postulates. Namely, the only logical rule of inference of each theory is our old friend LC (Logical Consequence).  There are no logical axioms, but the instances of LC that take no premises can be considered as such. All theories also share the Peano axioms. Having said this, in our following descriptions of those theories we will only present their (nonlogical) extra-Peano axioms and nonlogical rules.

A sentence F is considered provable in such a theory iff there is a sequence of sentences, called a proof of F, where each sentence is either a (Peano or extra-Peano)  axiom, or  follows from some previous sentences by one of the (logical or nonlogical) rules of inference, and where the last sentence is F. An extended proof is defined in the same way, only, with the additional requirement that each application of LC should come together with an attached CL12-proof of the corresponding sequent. With some fixed, effective, sound and complete axiomatization A of classical first order logic in mind, a superextended proof is an extended proof with the additional requirement that every application of Wait in the justification of a CL12-derivation in it comes with an A-proof of the elementarization of the conclusion. The property of being a superextended proof is (efficiently) decidable, while the properties of being an extended proof or just a proof are only recursively enumerable.

A weaker property than provability is what we call “prepresentability” (“pr” for “provably”). We say that a sentence F is prepresentable in a given theory T of clarithmetic iff there is a T-provable sentence X with X^†=F^†, where, as we remember,  ^†  is  the standard interpretation. The earlier discussed intensional completeness theorems establish the provability of all “good” sentences, while the extensional completeness theorems merely establish the prepresentability of such sentences.

Generally, as in the above definition of provability and proofs, in all clarithmetical theories we will only be interested in proving sentences. So, for technical convenience, we agree that, if a formula F is not a sentence but we say that it is provable in such a theory, it simply means that F is provable. Correspondingly, for readability, when formulating an inference rule

Keep this convention in mind when reading the subsequent subsectios of this section.

An  n-ary (n≥0)  pseudoterm, or pterm for short,  is an elementary formula p(y,x₁,…,x_n) with all free variables as shown and one of such variables --- y in the present case --- designated as what we call the value variable of the pterm,   such that PA proves x₁…x_n!y p(y,x₁,…,x_n). Here, as always,  !y means “there is a unique y such that”.  If p(y, x₁,…,x_n) is a pterm, we shall usually refer to it as p(x₁,…,x_n) or just p, making p boldface and dropping the value variable y or dropping all variables. Correspondingly, where F(y) is a formula, we write F(p(x₁,…,x_n)) or just F(p)  to denote the formula y(p(y, x₁,…,x_n) F(y)), which, in turn, is equivalent to y(p(y, x₁,…,x_n) F(y)). These sort of expressions, allowing us to syntactically treat pretms as if they were genuine terms of the language, are unambiguous in that all “disabbreviations” of them are provably equivalent in the system. Terminologically, genuine terms of L, such as (x+y)✕z, will  also count as pterms. Every n-ary pterm p(x₁,…,x_n) represents --- in the obvious sense --- some PA-provably total n-ary function f(x₁,…,x_n). For further notational and terminological convenience, in many contexts we shall identify pterms with the functions that they represent.

In our metalanguage, |x| will refer to the length of the binary representation of x. As in the case of other standard functions, the expression |x| will be simultaneously understood as a pterm naturally representing the function |x|. The delimiters “|…|”  will automatically also be treated as parentheses, so, for instance, when f is a unary function or pterm, we usually write “f|x|” to mean the same as the more awkward expression “f(|x|)”.  Further generalizing this notational convention, if x stands for an n-tuple (x₁,…,x_n) (n≥0) and we write p|x|,  it is to be understood as p(|x₁|,…,|x_n|).

7.5 Clarithmetics for polynomial time, polynomial space, elementary and primitive recursive computability

 
For a variable x, by a polynomial sizebound for x we shall mean a standard formula of the language of PA saying that |x|≤t(|y₁|,…,|y_n|), where y₁,…,y_n  are any variables different from x, and t(|y₁|,…,|y_n|) is any (0,ʹ,+,✕)-combination of the pterms |y₁|,…,|y_n|.  An exponential sizebound is defined the same way, only with “|x|≤t(y₁,…,y_n)” instead of “|x|≤t(|y₁|,…,|y_n|)”.  So, for instance, |x|≤ |y|+|z| is a polynomial sizebound for x while |x|≤ y+z is an exponential sizebound.

We say that a formula F is polynomially bounded iff the following condition is satisfied: Whenever xG(x) [resp. xG(x)] is a subformula of F,  G(x) has the form S(x)H(x) [resp. S(x)H(x)], where S(x) is a polynomial sizebound for x none of whose free variables is bound by  or  within F. “Exponentially bounded” is defined the same way, with the only difference that S(x) is required to be an exponential rather than a polynomial sizebound.

Where t is a term, we will be using t0 and t1 as abbreviations for the terms 0ʹʹ✕t and (0ʹʹ✕t)ʹ, respectively.  

Theory CLA4 only has two extra-Peano axioms: xy(y=xʹ), xy(y=x0) and a single nonlogical rule (of Induction), where F(x) is any polynomially bounded formula:

 Theory CLA5 has a single extra-Peano axiom: xy(y=xʹ) and a single nonlogical rule (of Induction), where F(x) is any polynomially bounded formula: 

Theory CLA6 only differs from CLA5 in that F(x) in Induction is required to be an exponentially bounded formula. 

Theory CLA7 only differs from CLA5 and CLA6 in that there are no restrictions at all on F(x) in Induction. 

Fact 7.5.1  Every (elementary L -) sentence provable in PA is also provable in any of our clarithemtical theories, including the ones defined in subsequent subsections.

This fact allows us to construct “lazy” proofs where some steps can be justified by simply indicating their provability in PA. That is, we can treat theorems of PA as if they were axioms of our clarithmetical theory.

Example 7.5.2 The following sequence is a lazy proof of x(x=0  x≠0) in CLA4.  This sentence says that the “zeroness” predicate is decidable:

I.      0=0  0≠0                                      LC: (no premises)
II.     x (x=0 x0=0)                           PA 
III.    x (x≠0 x0≠0)                           PA
IV.    x (x=0  x≠0 x0=0  x0≠0)     LC: II,III 
V.      x (x1≠0)                                      PA
VI.    x (x=0  x≠0 x0=0  x0≠0)     LC: V 
VII.   x (x=0  x≠0)                              Induction: I,IV,VI 

An extended version of the above proof will include the following three additional justifications (CL12-proofs):

             A justification for Step I:
1.    0=0                    Wait:  (no premises)
2.    0=0  0≠0           -Choose: 1 

             A justification for Step IV:
1.   x (x=0 x0=0),  x(x≠0 x0≠0)     s=0  s0=0                                 Wait: (no premises)
2.   x (x=0 x0=0),  x(x≠0 x0≠0)     s=0  s0=0  s0≠0                      -Choose: 1 
3.  x (x=0 x0=0),  x(x≠0 x0≠0)      s≠0  s0≠0                                 Wait:  (no premises)
4.  x (x=0 x0=0),  x(x≠0 x0≠0)      s≠0  s0=0  s0≠0                      -Choose: 3 
5.   x (x=0 x0=0),  x(x≠0 x0≠0)      s=0  s≠0  s0= 0  s0≠0           Wait:  2,4
6.   x (x=0 x0= 0),  x(x≠0 x0≠0)      x(x=0  s≠0  x0=0  x0≠0)   Wait:  5 

            A justification for Step VI:
1.   x (x1≠0)      s=0 s1≠0                                 Wait:  (no premises)
2.   x (x1≠0)      s≠0 s1≠0                                 Wait:  (no premises) 
3.   x (x1≠0)     s=0  s≠0 s1≠0                        Wait: 1,2 
4.   x (x1≠0)     s=0  s≠0 s1=0  s1≠0             -Choose:  3
5.   x (x1≠0)      x(x=0  x≠0 x1=0  x1≠0)    Wait:  4 

As we just saw, (additionally) justifying an application of LC takes more space than the (non-extended) proof itself. And this is a typical case for clarithmetical proofs. Luckily, however, there is no real need to formally justify LC. Firstly, this is so because CL12 is an analytic system, and proof-search in it is a routine (even if sometimes long) syntactic exercise. Secondly, thanks to Thesis 6.7.5, there is no need to generate formal CL12-proofs anyway: instead, we can use intuition on games and strategies. 

Below we write CLA4! for the extension of CLA4 obtained from the latter by taking all true (in the standard model) sentences of the language of PA as additional axioms.  Similarly for CLA5!, CLA6!, CLA7!.

 Theorem 7.5.3 (adequacy of CLA4) Consider an arbitrary sentence S of the language L.
            Constructive soundness: If S is provable in CLA4 or CLA4!, then S^† has a polynomial time solution. Such a solution can be automatically extracted from an extended CLA4- or CLA4!-proof of S.
            Extensional completeness: If S^† has a polynomial time solution, then S is prepresentable in CLA4. 
            Intensional completeness: If S^† has a polynomial time solution, then S is provable in CLA4!. 

 Theorem 7.5.4 The same adequacy theorem holds for CLA5 [resp. CLA6, resp. CLA7], only with “polynomial space” [resp. “elementary recursive time (=space)”, resp. “primitive recursive time (=space)”]  instead of “polynomial time”.

 CLA4 was introduced and proven adequate in [Jap11c]. The same for CLA5, CLA6 and CLA7 was done in [Jap16a].

7.6 Clarithmetics for provable computability

 Theory CLA8 is obtained from the earlier seen CLA7 by taking the following rule of Finite Search as an additional rule of inference, where p(x) is any elementary formula:

            A justification for the above rule is that, if we know how to decide the predicate p(x) (left premise), and we also know that the predicate is true of at least one number (right premise), then we can  apply the decision procedure to p(0), p(1), p(2),… until a number n is hit such that the procedure finds p(n) true, after which the conclusion x p(x) can be solved by choosing n for x in it.

Theory CLA9 is obtained from CLA7 by taking the following rule of Infinite Search as an additional rule of inference, where p(x) is any elementary formula:

            Note that this rule merely “modifies” Finite Search by changing the status of x p(x) from being a premise of the rule to being an antecedent of the conclusion. A justification for Infinite Search is that, if we know how to decide the predicate p(x), then we can apply the decision procedure to p(0), p(1), p(2), … until (if and when) a number n is hit such that the procedure finds p(n) true, after which the conclusion can be solved by choosing n for x in its consequent.  Note that, unlike the earlier-outlined strategy for Finite Search, the present strategy may look for n forever, and thus never make a move. This, however, only happens when x p(x) is false, in which case the conclusion is automatically won.

Theory CLA10 is obtained from CLA7 by adding to it the above rule of Infinite Search and the following rule of Constructivization, where q(x) is any elementary formula containing no free variables other than x:

            The admissibility of this rule, simply allowing us to change x to x, is obvious in view of the restriction that x p(x) is a sentence (as p(x) contains no free variables other than x). Indeed, if an x satisfying p(x) exists, then it can as well be “computed” (generated), even if we do not know what particular machine “computes” it. Note the non-constructive character of this justification.

The three theories CLA8-CLA10 are adequate with respect to the three natural concepts of computability explained below: PA-provably recursive time (=space) computability, constructively PA-provable computability, and (simply) PA-provable computability.

A natural extreme beyond primitive recursive time is PA-provably recursive time. That means considering PA-provably recursive functions instead of primitive recursive functions as time complexity bounds for computational problems.  It can be easily seen to be equivalent to PA-provably recursive space, just like there is no difference between time and space at the level of elementary recursive or primitive recursive functions. Theory CLA8 turns out to be adequate with respect to PA-provably recursive time computability in the same sense as CLA7 is (constructively) sound and complete with respect to primitive recursive time computability.

Not all computable problems have recursive (let alone provably so) time complexity bounds though. In other words, unlike the situation in traditional theory of computation, in our case not all computable problems are recursive time computable. An example is x(y p(x,y) y p(x,y)), where p(x,y) is a decidable binary predicate such that the unary predicate y p(x,y) is undecidable (for instance, p(x,y) means “Turing machine x halts within y steps”).  The problem x(y p(x,y) y p(x,y)) is solved by the following effective strategy: Wait till Environment chooses a value m for x. After that, for n=0,1,2,…, 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 t for the time complexity of a solution M of x(y p(x,y) y p(x,y)), then the following would be a decision procedure for (the undecidable) y p(x,y):  Given an input m (in the role of x), run M for t(|m|+1) steps in the scenario where Environment chooses m for x at the very beginning of the play of x(y p(x,y) y p(x,y)), and does not make any further moves. If, during this time, M chooses a number n for y in the consequent such that p(m,n) is true, accept; otherwise reject. So, 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 M such that PA proves that M computes X, even if the running time of M is not bounded by any recursive function. Theory CLA9 turns out to be sound and complete with respect to this sort of computability, in the sense that a sentence X is provable in CLA9 if and only if X is constructively PA-provably computable. 

An even weaker concept of (simply) PA-provable computability is obtained from that of constructively PA-provable computability by dropping the “constructiveness” condition. Namely, PA-provable computability of a sentence X means that PA proves that a machine M solving X exists, yet without necessarily being able to prove “M solves X” for any particular machine M. An example of a sentence that is PA-provably computable yet not constructively so is S  S, where S is an elementary sentence such that PA proves neither S nor S, such as, for instance, Gödel's sentence. Let L be a machine that chooses the left disjunct of S  S and retires. Similarly, let R be a machine that chooses the right disjunct and retires. One of these two machines is a solution of S S, and, of course, PA “knows” this. Yet, PA does not “know” which one of them is a solution (otherwise either S or S would be provable); nor does it have a similar sort of “knowledge” for any other particular machine. System CLA10 turns out to be sound and complete with respect to the present sort of computability, in the sense that a sentence X is provable in CLA10 if and only if X is PA-provably computable.

CLA8, CLA9 and CLA10 were introduced and proven adequate in [Jap14].

7.7 Tunable clarithmetic

Among the pterms/functions that we use in this section is (x)_y, standing for the yth least significant bit of the binary representation of x, i.e. the yth bit from the right, where the bit count starts from 0 rather than 1. When y≥|x|,  “the yth least significant bit of the binary representation of x”, by convention, is 0. Another abbreviation is Bit, defined by Bit(y,x)  =_def  (x)_y=1.

By a bound we shall mean a pterm p(x₁,…,x_n) with all free variables as shown  ---  which may as well be written simply as  p(x)  or p  --- satisfying the monotonicity condition (x₁≤y₁…x_n≤y_n p(x₁,…,x_n)≤ p(y₁,…,y_n)). A boundclass means a set of bounds closed under variable renaming. A boundclass triple is a triple R = (R_amplitude, R_space, R_time) of boundclasses.

Where p is a pterm and F is a formula, we  use the abbreviation x≤pF for x(x≤pF),  x≤pF for x(x≤pF),  |x|≤pF for x(|x|≤ p F), and  |x|≤pF for x(|x|≤ pF). Similarly for the blind quantifiers, and similarly for < instead of ≤.

Let F be a formula and B a boundclass. We say that F is B-bounded iff every -subformula [resp. -subformula] of F has the form |z|≤ b|s| H [resp. |z|≤ b|s| H], where z and all items of the tuple s are pairwise distinct variables not bound by  or  in F, and b|s| is a bound from B. 

Every boundclass triple R and set A of sentences induces the theory CLA11^R_A that we deductively define as follows. 

The extra-Peano axioms of CLA11^R_A, with x and y below being arbitrary two distinct variables, are:

• xy(y=xʹ)
• xy(y=|x|)
• xy(Bit(y,x)Bit(y,x))
• All sentences of A.      

CLA11^R_A has two nonlogical rules of inference: R-Induction and R-Comprehension. These rules are meant to deal exclusively with sentences, and correspondingly, in our schematic representations of them below, as in the earlier cases, each premise or conclusion H should be understood as its -closure H, with the prefix  dropped merely for readability.

The rule of R-Induction is

where x and all items of the tuple s are pairwise distinct  variables, F(x) is an  R_space-bounded formula, and b(s) is a bound from R_time.

The rule of R-Comprehension is

where x,y and all items of the tuple s are pairwise distinct variables,  p(y) is an elementary formula not containing x,  and b(s) is a  bound from R_amplitude.

Let B be a set of bounds. We define the linear closure of B as the smallest boundclass C such that B⊆C,  0∈C and, whenever bounds b and c are in C, so are the bounds bʹ and b+c. The polynomial closure of B is defined the same way but with the additional condition that, whenever b and c are in C, so is b✕c. Correspondingly, we say that B is linearly closed  [resp. polynomially closed] iff B is the same as its linear [resp. polynomial] closure.

Let b=b(x₁,…,x_m) and c=c(y₁,…,y_n) be two functions which depend exactly on the corresponding tuples of displayed variables, or pterms understood as such functions. We write b≤c  iff m=n and b(a₁,…,a_m)≤c(a₁,…,a_m) is true for all natural numbers a₁,…,a_m. Next, where B and C are boundclasses, we write b≤C to mean that b≤c for some c∈C, and write B≤C to mean that b≤C for all b∈B. Finally, where a₁,s₁,t₁,a₂,s₂,t₂ are bounds, we write (a₁,s₁,t₁) ≤ (a₂,s₂,t₂) to mean that a₁≤a₂, s₁≤s₂ and t₁≤t₂.

Definition 7.7.1 We say that a boundclass triple R is regular iff the following conditions are satisfied:

1. For every bound b(s)∈R_amplitude∪R_space∪R_time  and any (=some) variable z not occurring in b(s), the game z(z=b|s|)  has an R tricomplexity solution, and such a solution can be effectively constructed from b(s).
2. R_amplitude is at least linear, R_space is at least logarithmic, and R_time is at least polynomial. This is in the sense that, for any variable x, we have x≤R_amplitude, |x|≤ R_space and x,x²,x³,…≤R_time.
3. All three components of R are linearly closed and, in addition, R_time is also polynomially closed.
4. For each component B∈{R_amplitude, R_space, R_amplitude} of R, whenever b(x₁,…,x_n) is a bound in B and c₁,…,c_n∈R_amplitude∪R_space, we have b(c₁,…,c_n)≤B.
5. For every triple (a₁(x), s₁(x), t₁(x)) of bounds in R_amplitude✕R_space✕R_time  there is a triple  (a₂(x), s₂(x), t₂(x)) in R_amplitude✕R_space✕R_time such that (a₁(x), s₁(x), t₁(x))≤(a₂(x), s₂(x), t₂(x)) and  |t₂(x)|≤ s₂(x) ≤a₂(x) ≤t₂(x). 

Definition 7.7.2 We say that a theory CLA11^R_A is regular iff the boundclass triple R is regular and, in addition, the following conditions are satisfied:

1. Every sentence of A has an R tricomplexity solution. Here, if A is infinite, we additionally require that there is an effective procedure that returns an R tricomplexity solution for each sentence of A.
2. For every bound b(x) from R_amplitude∪R_space∪R_time  and every (=some) variable z not occurring in b(x), CLA11^R_A proves  z(z=b|x|).

We agree that, whenever A is a set of sentences, A! is an abbreviation of  A∪Th(N), where Th(N) is the set of all true (in the standard model) sentences of PA.

Theorem 7.7.3 (Adequacy of CLA11) Assume a theory CLA11^R_A is regular, and consider an arbitrary sentence S of its language. Recall that ^†  is the standard interpretation.

1. Constructive soundness:  If S is provable in CLA11^R_A or CLA11^R_A!, then S^† has an R tricomplexity solution. Such a solution can be automatically extracted from an extended CLA11^R_A- or CLA11^R_A!-proof of S.
2. Extensional completeness: If S^† has an R tricomplexity solution, then S is prepresentable in CLA11^R_A.
   
3. Intensional completeness:  If S^† has an R tricomplexity solution, then S is provable in CLA11^R_A!.
   

Below we are going to see an infinite yet incomplete series of natural theories that are regular and thus adequate in the sense of the above theorem. All these theories look like CLA11^R_∅, with the subscript ∅ indicating that the A (supplemental axioms) parameter is empty.

Given a set S of bounds, by S^♥ [resp. S^♠] we shall denote the linear closure [resp. polynomial closure] of S. We define the series B₁¹, B₁², B₁³,…, B₂,  B₃, B₄, B₅, B₆, B₇, B₈ of boundclasses as follows:

1. B₁¹  =  {|x|}^♥ (logarithmic boundclass);  B₁² = {|x|²}^♥;  B₁³ = {|x|³}^♥; … ;
2. B₂   =  {|x|}^♠ (polylogarithmic boundclass);
   
3. B₃    =  {x}^♥ (linear boundclass);
4. B₄   =  {x✕|x|, x✕|x|², x✕|x|³,…}^♥ (quasilinear boundclass);
5. B₅   =  {x}^♠ (polynomial boundclass);
6. B₆   =  {2^|x|, 2^|x|2, 2^|x|3,…}^♠ (quasipolynomial boundclass);   
7. B₇    =  {2^x}^♠ (exponential-with-linear-exponent boundclass);
8. B₈   =  {2^x, 2^x2, 2^x3,…}^♠ (exponential-with-polynomial-exponent boundclass).

Fact 7.7.4 For any boundclass triple R listed below, the theory CLA11^R is regular:

(B₃,B₁¹,B₅);  (B₃,B₁²,B₅);  (B₃,B₁³,B₅);  …;  (B₃,B₂,B₅);  (B₃,B₂,B₆);  (B₃,B₂,B₇);  (B₃,B₃,B₅);  (B₃,B₃,B₆);  (B₃,B₃,B₇);  (B₄,B₁¹,B₅);  (B₄,B₁²,B₅);  (B₄,B₁³,B₅);  …;  (B₄,B₂,B₅); (B₄,B₂,B₆); (B₄,B₄,B₅);   (B₄,B₄,B₆);  (B₄,B₄,B₇);   (B₅,B₁¹,B₅);  (B₅,B₁²,B₅);  (B₅,B₁³,B₅);  …; (B₅,B₂,B₅);  (B₅,B₂,B₆);   (B₅,B₅,B₅);   (B₅,B₅,B₆);    (B₅,B₅,B₇);  (B₅,B₅,B₈).