(CoL)

Section 6** **

**Axiomatizations**

6.1 Outline

6.2 The Gentzen-style system **CL7**

6.3 The Gentzen-style system **Int ^{+}**

6.4 The cirquent calculus system **CL15**

6.5 The brute force system **CL13**

6.6 The brute force system **CL4**

6.7 The brute force system **CL12**

6.1 Outline

** **

An axiomatization of the set of valid formulas of the full language of Section 5 has not been found so far. In fact, it is not known if such an axiomatization exists in principle. However, axiomatizations do exist for a number of fragments of the language, obtained by disallowing certain operators, disallowing one or another sort of game letters, or imposing some other restrictions on formulas.

In this section we explore six of such axiomatic systems: **CL7**, **Int ^{+}**,

**CL15**,

**CL13**,

**CL4**and

**CL12**. The first four are

*propositional*systems (only nullary game letters allowed), while the last two are

*first-order*systems (no arity restrictions on game letters).

**CL7**,

**Int**and

^{+}**CL15**are

*general-base*, meaning that only general game letters are allowed.

**CL12**is

*elementary-base*, meaning that only elementary game letters are allowed. The remaining systems

**CL13**and

**CL4**are

*mixed-base*, allowing both sorts of game letters. The sets of operators allowed in formulas are: just {} for

**CL7**; {, , } for

**Int**; {, , ,

^{+}**, } for**

**CL15**; {, , , , , , , , } for

**CL13**; {, , , , , , ,

**,**

**} for**

**CL4**; and { ,,, , , , ,

**,**

**, external } for**

**CL12**. We also divide these systems into the categories

*Gentzen style*(

**CL7**,

**Int**),

^{+}*cirquent calculus*(

**CL15**) and

*brute force*(

**CL13**,

**CL4**,

**CL12**). Gentzen-style systems are sequent calculus systems in the traditional sense. It turns out that only very limited fragments of CoL can be axiomatized this or any other traditional (e.g. Hilbert-style) way, and some novel sorts of proof systems are necessary. Cirquent calculus and brute force systems are such novel sorts. Cirquent calculus operates with cirquents rather than formulas or sequents. Brute force systems operate with formulas or sequents, but in an unusual way, with their rules being relatively directly derived from the underlined game semantics and hence somewhat resembling games themselves.

All of the above systems have been proven to be adequate (sound and complete). Specifically, we have:

**Theorem 6.1.1** Let **S** be any one of the systems **CL7**, **Int ^{+}**,

**CL15**,

**CL13**,

**CL4**or

**CL12**defined in the forthcoming Subsections 6.2-6.7. With “

**S**-formula” meaning a formula of the language of

**S**and “

**S**-proof” meaning “proof in

**S**”, we have:

1. ** Adequacy**: An

**S**-formula

*F*is logically valid iff

*F*is provable in

**S**.

** **2.

**: There is an effective procedure that takes an arbitrary**

*Uniform-constructive soundness***S**-proof of an arbitrary

**S**-formula

*F*and generates a logical solution for

*F*.

In the sequel we shall refer to the property of satisfying the above two clauses together as ** uniform**-

**.**

*constructive adequacy*

6.2 The Gentzen-style system **CL7**

** **

**CL7- formulas** are formulas of the language of CoL that do not contain any function letters, do not contain any game letters (including the logical letters and

**) other than nonlogical 0-ary general game letters, and do not contain any operators other than .**

A **CL7- sequent** is a pair Γ⇒

*F*, where Γ is a (possibly empty) multiset of

**CL7**-formulas, and F is a

**CL7**-formula.

As usual, when Γ and Δ are multisets of formulas and *F* is a formula, we shall write “Γ,Δ” for Γ∪Δ and “Γ,*F*” for Γ∪{*F*}.

The ** axioms** of

**CL7**are all

**CL7**-sequents of the form Γ,

*F*⇒

*F.*And the system only has the following two

**of inference:**

*rules*

A ** CL7-proof** of a sequent

*S*is a sequence

*X*

_{1},…,

*X*

_{n}_{ }of sequents, where

*S*=

*X*, and where each

_{n}*X*is either an axiom or follows from some earlier sequents of the sequence by one of the rules of inference. A

_{i}**of a formula**

*CL7-proof**F*is a

**CL7**-proof of the empty-antecedent sequent ⇒

*F.*

* *

With understood as linear implication, **CL7** proves nothing less and nothing more than the implicative fragment of affine logic does. Adding the (left) ** contraction** rule

to **CL7** results in an unsound system. Let us call it **CL7**+Contraction. An example of a formula provable in the latter but not in **CL7** is (*E*(*F**G*))((*E**F*)(*E**G*)). It can be shown^{[Jap09b]} however that **CL7**+Contraction is sound and complete if we rewrite as either or . The logical behaviors of these two rimplications in isolation are thus undistinguishable. This stops being the case when the rimplications are taken in combination with other operators. For instance, the intuitionistically provable principle (*E*⊃*G*)((*F*⊃*G*)⊃(*E**F*⊃G)) is valid with ⊃ read as but not as . An example of a classical tautology invalid with all three operators ⊃∈{,,} is Peirce’s Law ((*E*⊃*F*)⊃*E*)⊃*E*.

**CL7** was studied and proven uniform-constructively adequate in [Jap09b].

**Open problem 6.2.1 **Does CL7 remain complete with respect to multiform (rather than uniform) validity? (Expectation: yes).

6.3 The Gentzen-style system **Int ^{+}**

** **

**Int ^{+}-formulas** are formulas of the language of CoL that do not contain any function letters, do not contain any game letters (including the logical letters , ) other than nonlogical 0-ary general game letters, and do not contain any operators other than , , . It turns out that logically valid

**Int**-formulas are exactly those provable in the positive (negation- and absurd-free) fragment of propositional intuitionistic logic

^{+}**Int**. As a deductive system,

^{+}**Int**is the result of replacing by in the earlier discussed

^{+}**CL7**+Contraction, allowing and as additional operators in formulas, and adding the following rules to the system, with

*i*ranging over {1,2}:

The full propositional intuitionistic logic **Int** is obtained from **Int ^{+}** by allowing in the language, and adding the axiom Γ, ⇒

*F*. Such a system is sound but incomplete with respect to our semantics. Below is an example of a logically valid yet not

**Int**-provable principle, with

*F*(the intuitionistic negation of

*F*) understood as an abbreviation of

*F*:

(*E **F ** G*) (* **E ** H ** J*) (*E ** F*) (*E ** G*) * *( *E ** H*) ( *E ** J*).

The uniform-constructive adequacy of** Int ^{+}** with respect to our semantics follows from slightly stronger results proven in [Jap07d, Mez10].

**Open problems 6.3.1 **

- Does
**Int**remain complete with respect to multiform (rather than uniform) validity?^{+}

- Add to the language of
**Int**, and adequately axiomatize (if possible) the corresponding superintuitionistic logic. What kinds of (if any) Kripke models would such a logic have?^{+} - Is the first-order (with quantifiers
*,*) positive (negation- and absurd-free) - Add to the language of
**Int**, but replace the general game letters of the latter with nonlogical elementary game letters. Adequately axiomatize (if possible) the corresponding logic.^{+}

- If the preceding task is achieved, then try the first-order version of it as well.

- In the language of
**Int**, replace with . What logic are we getting? How about the variations of this logic in the style of the above items 1-5?^{+}

6.4 The cirquent calculus system **CL15**

** **

**CL15- formulas** are formulas of the language of CoL that do not contain any function letters, do not contain any game letters (including the logical letters ,) other than nonlogical 0-ary general game letters, and do not contain any operators other than , , ,

**, . Besides, it is required that is only applied to atoms. This condition can be violated if we understand (**

*E*

*F*), (

*E*

*F*),

**E and E as abbreviations of**

*E*

*F,*

*E*

*F,*

*E*and

*E*, respectively. We may as well write

*E*

*F*or write

*E*

*F*,

*understanding these expressions as abbreviations of*

*E*

*F*and

*E*

*F*(i.e.

*E*

*F*), respectively.

**Definition 6.4.1** A **CL15 -cirquent** (hencefore simply “cirquent”) is a triple

*C*=(

**,**

*F***,**

*U***) where:**

*O*is a nonempty finite sequence of*F***CL15**-formulas, whose elements are said to be theof*oformulas**C*. Here the prefix “o” is for “occurrence”, and is used to mean a formula together with a particular occurrence of it in. So, for instance, if*F*=〈*F**E*,*G*,*E*〉, then the cirquent has three oformulas even if only two formulas.- Both
and*U*are nonempty finite sequences of nonempty sets of oformulas of*O**C*. The elements ofare said to be the*U*of*undergroups**C*, and the elements ofare said to be the*O*of*overgroups**C*. As in the case of oformulas, it is possible that two undergroups or two overgroups are identical as sets (have identical), yet they count as different undergroups or overgroups because they occur at different places in the sequence*contents*or*U*. Simply “*O*” will be used as a common name for undergroups and overgroups.*group* - Additionally, every oformula is required to be in (the content of) at least one undergroup and at least one overgroup.

While oformulas are not the same as formulas, we may often identify an oformula with the corresponding formula and, for instance, say “the oformula *E*” if it is clear from the context which of the possibly many occurrences of *E* is meant. Similarly, we may not always be very careful about differentiating between groups and their contents.

We represent cirquents using three-level diagrams such as the one shown below:

This diagram represents the cirquent with four oformulas *F*_{1}, *F*_{2}, *F*_{3}, *F*_{4}, three undergroups {*F*_{1}}, {*F*_{2},*F*_{3}}, {*F*_{3},*F*_{4}} and two overgroups {*F*_{1},*F*_{2},*F*_{3}}, {*F*_{2},*F*_{4}}. We typically do not terminologically differentiate between cirquents and diagrams: for us, a diagram *is* (rather than *represents*) a cirquent, and a cirquent *is* a diagram. Each (under- or over-) group is represented by a •, where the ** arcs** (lines connecting the • with oformulas) are pointing to the oformulas that the given group contains.

The ** axioms** of

**CL15**are all cirquents of the form

(〈*F*_{1},*F*_{1},…, * F _{n}*,

*F*〉, 〈{

_{n}*F*

_{1},

*F*

_{1}}, …, {

*F*,

_{n}*F*}〉, 〈{

_{n}*F*

_{1},

*F*

_{1}}, …, {

*F*

_{n},

*F*

_{n}}〉),

where *n* is any positive integer, and *F*_{1},…,*F _{n}* are any formulas. The diagram of such a cirquent looks like an array of

*n*“diamonds”, as shown below for the case of

*n*=3:

**CL15** has nine rules of inference. Below we explain them in a relaxed fashion, in terms of deleting arcs, swapping oformulas, etc. Such explanations are rather clear, and translating them into rigorous formulations in the style and terms of Definition 6.4.1, while possible, is hardly necessary. All rules take a single premise.

**1. Exchange **This rule comes in three flavors:

**,**

*Undergroup Exchange***and**

*Oformula Exchange***. Each one allows us to swap any two adjacent objects (undergroups, oformulas or overgroups) of a cirquent, otherwise preserving all oformulas, groups and arcs.**

*Overgroup Exchange*Below we see three examples. In each case, the upper cirquent is the premise and the lower cirquent is the conclusion of an application of the rule. Between the two cirquents --- here and later --- is placed the name of the rule by which the conclusion follows from the premise.

The presence of Exchange essentially allows us to treat all three components (

**,**

*F***,**

*U***) of a cirquent as multisets rather than sequences.**

*O***2. Weakening **The premise of this rule is obtained from the conclusion by deleting an arc between some undergroup

*U*with ≥2 elements and some oformula

*F*; if

*U*was the only undergroup containing

*F*, then

*F*should also be deleted (to satisfy Condition 3 of Definition 6.4.1), together with all arcs between

*F*and overgroups; if such a deletion makes some overgroups empty, then they should also be deleted (to satisfy Condition 2 of Definition 6.4.1). Below are three examples:

**3. Contraction** The premise of this rule is obtained from the conclusion through replacing an oformula

*F*by two adjacent oformulas

*F*,

*F*, and including them in exactly the same undergroups and overgroups in which the original oformula was contained. Example:

**4. Duplication **This rule comes in two versions:

**and**

*Undergroup Duplication***. The conclusion of Undergroup Duplication is the result of replacing, in the premise, some undergroup**

*Overgroup Duplication**U*with two adjacent undergroups whose contents are identical to that of

*U*. Similarly for Overgroup Duplication. Examples:

**5. Merging** In the top-down view, this rule merges any two adjacent overgroups, as illustrated below.

**6. Disjunction Introduction** The premise of this rule is obtained from the conclusion by replacing an oformula

*F*

*G*by two adjacent oformulas

*F*,

*G*, and including both of them in exactly the same undergroups and overgroups in which the original oformula was contained, as illustrated below:

**7.** ** Conjunction Introduction** The premise of this rule is obtained from the conclusion by applying the following two steps:

- Replace an oformula
*F**G*by two adjacent oformulas*F*,*G*, and include both of them in exactly the same undergroups and overgroups in which the original oformula was contained.

- Replace each undergroup
*U*originally containing the oformula*F**G*(and now containing*F*,*G*instead) by the two adjacent undergroups*U*-{*G*} and*U*-{*F*}.

Below we see three examples.

**8.** ** Recurrence Introduction** The premise of this rule is obtained from the conclusion through replacing an oformula

*F*by

*F*(while preserving all arcs), and inserting, anywhere in the cirquent, a new overgroup that contains

*F*as its only oformula. Examples:

**9. Corecurrence Introduction **The premise of this rule is obtained from the conclusion through replacing an oformula

*F*by

*F*, and including

*F*in any (possibly zero) number of the already existing overgroups in addition to those in which the original oformula

*F*was already present. Examples:

A **CL15 -proof** (or simply a proof in this subsection) of a cirquent

*C*is a sequence of cirquents ending in

*C*such that the first cirquent is an axiom, and every subsequent cirquent follows from the immediately preceding cirquent by one of the rules of

**CL15**. A

**CL15**of a formula

*-proof**F*is understood as a

**CL15**-proof of the cirquent (〈F〉,〈{F}〉,〈{F}〉), i.e. of the cirquent

Let us look at some examples. The following is a proof of *F ** F*, i.e. *F ** F*:

The following example shows a proof of *F ** F ** F*:

At the same time, the converse *F **F ** F* of the above formula has no proof. However, the latter becomes provable after prefixing each occurrence of *F* with with **. Below is a proof of ***F ** **F ** **F.* The meaning of the principle expressed by this formula can be characterized by saying that solving two copies of a problem of the form *F* does not take any more resources (is not any harder) than solving just a single copy.

Below is a proof of

*F*

*F.*Unlike the previously seen examples, proving this formula requires using Duplication.

Now we prove *E ** **F ** ***(***E ** F*). The converse **(***E ** F*) *E ** **F*, on the other hand, can be shown to be unprovable.

The formulas proven so far are also provable in affine logic (with , understood as multiplicatives, **, as exponentials, and ***F* as *F*^{⊥}). In general, **CL15** is a proper extension of the corresponding (additive-free) fragment of affine logic. The following example shows the **CL15**-provability of the formula *F**F*, which is not provable in affine logic. The converse *F* *F*, on the other hand, is unprovable in either system.

Another --- longer but recurrence-free --- example separating **CL15** from affine logic is (*E**F*) (*G**H*) (*E**G*) (*F**H*) (the already mentioned Blass principle), or even the special case (*E**E*) (*E**E*) (*E**E*) (*E**E*) of it; constructing a **CL15**-proof of this formula is left as an exercise.

**CL15** was introduced and proven uniform-constructively adequate in [Jap13a, Jap13b]. W. Xu and S. Liu in [Xu13] showed that **CL15** remains sound with , instead of* ***,. Completeness, however, is lost in this case because, as already mentioned, the formula ***F*(*F**F**F*) *F* is valid while* A***(***A**A**A*) *A* is not.

**Open problems 6.4.2 **

- Is CL15 decidable?
- Extend the language of CL15 so as to include the choice connectives and , and axiomatize (if possible) the set of valid formulas in this extended language.
- Replace
**, with , in the language of CL15. Is the set of valid formulas in this new language axiomatizable (and how)?**

- Does CL15 remain complete with respect to multiform (rather than uniform) validity?

6.5 The brute force system **CL13**

** **

**CL13- formulas** are formulas of the language of CoL that do not contain any function letters, do not contain any non-nullary game letters, and do not contain any operators other than , , , , , , , , . As in the case of

**CL15**, officially is only allowed to be applied to atoms, otherwise understood as the corresponding DeMorgan abbreviation.

*E*

*F*is also understood as an abbreviation of its standard meaning. To define the system axiomatically, we need certain terminological conventions.

- A
means an atom with or without negation .*literal* - As in the previous case, we often need to differentiate between
*subformulas*as such, and particular*occurrences*of subformulas. We will be using the termto mean a subformula together with a particular occurrence. The prefix “o” will be used with a similar meaning in terms such as*osubformula*,*oatom*, etc.*oliteral* - An osubformula is
iff it is not in the scope of . Otherwise it is*positive*. According to our conventions regarding the usage of , only oatoms may be negative.*negative* - A
is a positive oliteral.*politeral* - A
*-(*is a (sub)formula of the form*sub)formula**E**F*. Similarly for the other connectives of the language. - A
is one of the form*sequential (sub)formula**E**F*or*E**F*. We say that*E*is theof such a (sub)formula, and*head**F*is its.*tail* - Similarly, a
is one of the form*parallel (sub)formula**E**F*or*E**F*, ais one of the form*toggling (sub)formula**E**F*or*E**F*, and ais one of the form*choice (sub)formula**E**F*or*E**F.* - A formula is said to be
iff it contains no general atoms and no operators other than , , , , .*quasielementary*

- A formula is said to be
iff it is a formula of classical propositional logic, i.e., contains no general atoms and no operators other than , , .*elementary*

- A
(or*semisurface osubformula*) is an osubformula (or occurrence) which is not in the scope of a choice connective.*occurrence*

- A
(or*surface osubformula*) is an osubformula (or occurrence) which is not in the scope of any connectives other than , , .*occurrence* - The
of a formula*quasielementarization**F*, denoted by |*F*|, is the result of replacing in*F*every sequential osubformula by its head, every -osubformula by , every -osubformula by , and every general politeral by (the order of these replacements does not matter). For instance, |((*P**q*)((*p**P*)(*Q**R*))) (*q*(*r**s*))| = ((*q*)(*p*)) . - The
of a quasielementary formula*elementarization**F*, denoted by ||*F*||, is the result of replacing in*F*every -osubformula by and every -osubformula by (again, the order of these replacements does not matter). For instance, ||(*s*(*p*(*q**r*)))(*s*(*p**r*))|| = (*s*)(*s*). - A quasielementary formula
*F*is said to beiff its elementarization ||*stable**F*|| is a tautology of classical logic. Otherwise*F*is.*unstable*

We now define **CL13** by the following six rules of inference, where P*F *means “from premise(s) P conclude *F*”. Axioms are not explicitly stated, but the set of premises of the () rule can be empty, in which case (the conclusion of) this rule acts like an axiom.

*Rule**():*

*H**F*, where

*F*is a stable quasielementary formula, and

**is the smallest set of formulas satisfying the following condition:**

*H*- Whenever
*F*has a surface osubformula*E*_{0}*E*_{1}, for both*i*∈{0,1},contains the result of replacing in*H**F*that osubformula by*E*._{i}

*Rule** *(): *H * *F*, where *F* is a quasielementary formula, and *H* is the result of replacing in *F* a surface osubformula *E**G* by *E* or *G*.

*Rule** *(): |*F*|, *H **F*, where *F* is a non-quasielementary formula (note that otherwise *F*=|*F*|), and ** H** is the smallest set of formulas satisfying the following two conditions:

- Whenever
*F*has a semisurface osubformula*G*_{0}*G*_{1}, for both*i*∈{0,1},contains the result of replacing in*H**F*that osubformula by*G*._{i} - Whenever
*F*has a semisurface osubformula*E**G*,contains the result of replacing in*H**F*that osubformula by*G*.

*Rule** *(): *H * *F*, where H is the result of replacing in *F* a semisurface osubformula *E**G* by *E* or *G*.

*Rule** *(): *H * *F*, where *H* is the result of replacing in *F* a semisurface osubformula *E**G* by *G*.

*Rule** *(M): *H * *F*, where *H* is the result of replacing in *F* two --- one positive and one negative --- semisurface occurrences of some general atom *P* by a nonlogical elementary atom *p* which does not occur in *F*.

A **CL13- proof** of a formula

*F*can be defined as a sequence of formulas ending with

*F*such that every formula follows from some (possibly empty) set of earlier formulas by one of the rules of the system.

**Example 6.5.1** In view of the discussions of Section 3.10, the formula (*p**p*) (*q**q*) (*p**q*) (*p**q*) expresses --- or rather implies --- the known fact that, if two predicates *p* and *q *are recursively approximable, then so is their intersection *p**q*. The following sequence is a **CL13**-proof of this formula, re-written into its official form ((*p**p*) (*q**q*)) ((*p**q*) (*p**q*)):

- (
*p**q*) (*p**q*) (): (no premises) - (
*p**q*) ((*p**q*) (pq)) (): 1 - (
*p**q*) (*p**q*) (): (no premises) - (
*p**q*) ((*p**q*) (*p**q*)) (): 3 - (
*p*(*q**q*)) ((*p**q*) (*p**q*)) (): 2,4 - (
*p**q*) (*p**q*) (): (no premises) - (
*p**q*) ((*p**q*) (*p**q*)) (): 6 - (
*p**q*) (*p**q*) (): (no premises) - (
*p**q*) ((*p**q*) (*p**q*)) (): 8 - (
*p*(*q**q*)) ((*p**q*) (*p**q*)) (): 7,9 - ((
*p**p*)*q*) ((*p**q*) (*p**q*)) (): 2,7 - ((
*p**p*)*q*) ((*p**q*) (*p**q*)) (): 4,9 - ((p
*p*) (*q**q*)) ((*p**q*) (*p**q*)) (): 5,10,11,12

**Example 6.5.2** Pick any two distinct connectives &_{1} and &_{2} from the list ,,,. Then **CL13** proves the formula *P*&_{1}*Q ** P*&_{2}*Q* if and only if &_{1} is to the left of &_{2} in the list. Similarly for the list ,,,. Below we verify this fact only for the case {&_{1},&_{2}}={,}. The reader may want to try some other combinations as exercises.

Here is a **CL13**-proof of *P**Q ** P**Q*:

*p**p*(): (no premises)- (
*p*)*p*(): 1 *q**q*(): (no premises)- (
*p**q*)*q*(): 3 - (
*p**Q*)*Q*(M): 4 - (
*p**Q*) (*p**Q*) (): 2,5 - (
*P**Q*) (*P**Q*) (M): 6

On the other hand, the formula *P**Q ** P**Q*, i.e. (*P**Q*) (*P**Q*), has no proof. This can be shown through attempting and failing to construct, bottom-up, a purported **CL13**-proof of the formula. Here we explore one of the branches of a proof-search tree. (*P**Q*) (*P**Q*) is not quasielementary, so it could not be derived by (be the conclusion of) the () or () rule. The () rule does not apply either, as there is no in the formula. This leaves us with one of the rules (), () and (M). Let us see what happens if our target formula is derived by (). In this case the premise should be *Q * (*P**Q*). The latter can be derived only by () or (M). Again, let us try (M). The premise in this subcase should be *q * (*P**q*) for some elementary atom *q*. But the only way *q ** *(*P**q*) can be derived is by () from the premise *q ** *(*q*). This formula, in turn, could only be derived by (), in which case *q* is one of the premises. Now we are obviously stuck, as *q* is not the conclusion of any of the rules of the system. We thus hit a dead end. All remaining possibilities can be checked in a similar routine/analytic way, and the outcome in each case will be a dead end.

**Exercise 6.5.3** Construct a **CL13**-proof of (*P**P*) (*P**P*) (*P**P*).

**Exercise 6.5.4** For which of the four disjunctions ∪∈{,,,} are the following formulas **CL13**-provable and for which are not? (1) *P*∪*P*; (2) *P*∪*Q ** Q*∪*P*; (3) *P*∪*P ** P*; (4) *p*∪*p ** p*.

System **CL13** was introduced and proven uniform-constructively adequate in [Jap11a].

**Open problems 6.5.4 **

- Consider the first-order version of the language of CL13 with choice (to start with) quantifiers. Adequately axiomatize the corresponding logic.
- What is the computational complexity of (the property of provability in) CL13? (Expectation: PSPACE-complete).
- Consider the set of the theorems of CL13 that do not contain nonlogical elementary letters. Does this set remain complete with respect to multiform (rather than uniform) validity?

6.6 The brute force system **CL4**

** **

**CL4- formulas** are formulas of the language of CoL that do not contain any operators other than , , , , , , ,

**,**

**. For simplicity and safety, we additionally require that, in any formula, no quantifier binds a variable which also has a free occurrence in that formula. As in the previous cases, negation applied to non-atoms is understood as the corresponding DeMorgan abbreviation, and**

*E*

*F*is also the standard abbreviation. An

**is a**

*elementary*CL4-*formula***CL4**-formula which contains no choice operators and no general game letters. Our axiomatization of

**CL4**relies on the following terminology and notation.

- A
is*literal**L*(*t*_{1}*,*…,*t*) or_{n}*L*(*t*_{1}*,*…,*t*), where_{n}*L*(*t*_{1}*,*…,*t*) is an atom. Such a literal is said to be_{n}or*elementary*depending on whether the letter*general**L*is elementary or general. - A
of a subformula is an occurrence which is not in the scope of , , , , and/or .*surface occurrence* - The
||*elementarization**F*|| of a formula*F*is the result of replacing in*F*all surface occurrences of subformulas of the form*G**H*or*xG*by , all surface occurrences of subformulas of the form*G**H*or*xG*by , and all surface occurrences of general literals by . - A formula is said to be
iff its elementarization is classically valid; otherwise it is*stable*. By “classical validity”, in view of GÃ¶del's completeness theorem, we mean provability in some fixed standard version of classical first-order calculus with function letters and =, where = is the identity predicate (so that, say,*unstable**x*=*x*,*x*=*y*(*E*(*x*)↔*E*(*y*)), etc. are provable). - We will be using the notation
*F*[*E*_{1},…*,E*] to mean a formula_{n}*F*together with some*n*fixed surface occurrences of subformulas*E*_{1},…*,E*. Using this notation sets a context, in which_{n}*F*[*G*_{1},…*,G*] will mean the result of replacing in_{n}*F*[*E*_{1},…*,E*] those occurrences of_{n}*E*_{1},…*,E*by_{n}*G*_{1},…*,G*, respectively. Note that here we are talking about_{n}*occurrences*of*E*_{1},…*,E*. Only those occurrences get replaced when moving from_{n}*F*[*E*_{1},…*,E*] to_{n}*F*[*G*_{1},…*,G*], even if the formula also had some other occurrences of_{n}*E*_{1},…*,E*._{n}

We now define **CL4** by the following four ** rules** of inference, where P

*F*means “from premise(s) P conclude

*F*”. Axioms are not explicitly stated, but the set of premises of the Wait rule can be empty, in which case (the conclusion of) this rule acts like an axiom.

-*Choose:**F*[*H _{i}*]

*F*[

*H*

_{0}

*H*

_{1}], where

*i*∈{0,1}.

-*Choose:**F*[*H*(*t*)] *F*[*xH*(*x*)], where *t* is either a constant or a variable with no bound occurrences in the premise.

*Wait: E **F *(n≥0), where *F* is stable, and ** E** is a set of formulas satisfying the following two conditions:

1. Whenever *F* has the form *F*[*G**H*], ** E** contains both

*F*[

*G*] and

*F*[

*H*].

2. Whenever *F* has the form *F*[x*G*(*x*)], ** E** contains

*F*[

*G*(

*y*)] for some variable

*y*which does not occur in the conclusion.

** **

*Match:**F*[*p*(** t**),

*p*(

**)]**

*s**F*[

*P*(

**),**

*t**P*(

**)], where**

*s**P*is an

*n*-ary (

*n*Â³0) general game letter,

**and**

*t***are**

*s**n*-tuples of terms, and

*p*is an

*n*-ary elementary game letter which does not occur in the conclusion.

The definitions of proof and provability in **CL4** are standard. The following is a **CL4**-proof of *x**y*(*P*(*x*) *P*(*y*)):

1. *p*(*x*) *p*(*y*) Wait: (no premises)

2. *P*(*x*) *P*(*y*) Match: 1

3. *y*(*P*(*z*) * P*(*y*)) -Choose: 2

4. *x**y*(*P*(*x*) *P*(*y*)) Wait: 3

On the other hand, **CL4** does not prove *y**x*(*P*(*x*) *P*(*y*). Indeed, obviously this unstable formula cannot be the conclusion of any rule but -Choose. If it is derived by this rule, the premise should be *x*(*P*(*x*) *P*(*t*)) for some constant or variable *t* different from *x*. *x*(*P*(*x*) *P*(*t*)), in turn, could only be derived by Wait where, for some variable *z* different from* t*, *P*(*z*) *P*(*t*) is a (the) premise. The latter is an unstable formula and does not contain choice operators, so the only rule by which it can be derived is Match, where the premise is *p*(*z*) *p*(*t*) for some elementary game letter *p*. Now we deal with a classically non-valid and hence unstable elementary formula, and it cannot be derived by any of the four rules of **CL4**.

Note that, in contrast, the “blind version” *y**x*(*P*(*x*) *P*(*y*)) of *y**x*(*P*(*x*) *P*(*y*)) is provable:

1. *y**x*(*p*(*x*) *p*(*y*)) Wait: (no premises)

2. *y**x*(*P*(*x*) *P*(*y*)) Match: 1

‘*There is y such that, for all x,* *P*(*x*) *P*(*y*)’ is true yet not in a constructive sense, thus belonging to the kind of principles that have been fueling controversies between the classically- and constructivistically-minded. As noted earlier, CoL is offering a peaceful settlement, telling the arguing parties: “There is no need to fight at all. It appears that you simply have two different concepts of ‘*there* *is*’/‘*for all*’. So, why not also use two different names: . **/**** and /. Yes, ***y**x*(*P*(*x*) *P*(*y*)) is indeed right; and yes, *y**x*(*P*(*x*) *P*(*y*)) is indeed wrong.” Clauses 1 and 2 of Exercise 6.6.1 illustrate a similar solution for the law of the excluded middle, the most controversial principle of classical logic.

The above-said remains true with the elementary letter *p* instead of the general letter *P*, for what is relevant there is the difference between the constructive and non-constructive versions of logical operators rather than how atoms are understood. Then how about the difference between the elementary and non-elementary versions of atoms? This distinction allows CoL to again act in its noble role of a reconciliator/integrator, but this time between classical and linear logics, telling them: “It appears that you have two different concepts of the objects that logic is meant to study. So, why not also use two different sorts of atoms to represent such objects: elementary atoms *p*,*q*,… and general atoms *P*,*Q*,.... Yes, *p**p**p* is indeed right; and yes, *P**P**P* (Exercise 6.6.1, clause 4) is indeed wrong”. However, the term “linear logic” in this context should be understood in a very generous sense, referring not to the particular deductive system proposed by Girard in [Gir87] but rather to the general philosophy and intuitions traditionally associated with it. The formula of clause 3 of the following exercise separates **CL4** from linear logic. That formula is provable in affine logic though. Switching to affine logic, i.e. restoring the deleted (from classical logic) rule of weakening, does not however save the case: the **CL4**-provable formulas of clauses 10, 11 and 18 of the following exercise are provable in neither linear nor affine logics.

**Exercise 6.6.1** Verify the following provabilities (Yes:) or unprovabilities (No:) in **CL4**. In clauses 14 and 15 below, provability of *E*⇔*F *means provability of both* * *E**F* and *F**E*.

1. Yes: *P**P*.

2. No: *P**P*. Compare with 1.

3. Yes: *P**P ** * *P*.

4. No: *P ** P**P*. Compare with 3,5.

5. Yes: *P * *P**P*.

6. Yes: (*P**Q*) (*P**R*) *P* (*Q**R*).

7. No: *P * (*Q**R*) (*P**Q*) (*P**R*). Compare with 6,8.

8. Yes: *p * (*Q**R*) (*p**Q*) (*p**R*).

9. No: *p* (*Q**R*) (*p**Q*) (*p**R*). Compare with 8.

10. Yes: (*P**P*) (*P**P*) (*P**P*) (*P**P*).

11. Yes: (*P * (*R**S*)) (*Q * (*R**S*)) ((*P**Q*) *R*) ((*P**Q*) *S*) (*P**Q*) (*R**S*).

12. Yes: *xP*(*x*) *xP*(*x*).

13. No: *xP*(*x*) *xP*(*x*). Compare with 12.

14. Yes: *xP*(*x*) *xQ*(*x*) ⇔ *x*(*P*(*x*) *Q*(*x*)). Similarly for instead of , and/or ** instead of ****. **

15. Yes: *x**yP*(*x*,*y*) ⇔ *y**xP*(*x*,*y*). Similarly for instead of , and/or ** instead of ****.**

16. Yes: *x*(*P*(*x*) *Q*(*x*)) *xP*(*x*) *xQ*(*x*).

17. No: *x*(*P*(*x*) *Q*(*x*)) *xP*(*x*) *xQ*(*x*). Compare with 16.

18. Yes: *x*((*P*(*x*) *xQ*(*x*)) (*xP*(*x*) *Q*(*x*))) *xP*(*x*) *xQ*(*x*).

19. Yes: *x**y*(*y*=*f*(*x*)).

20. No: *x**y*(*y*=*f*(*x*)). Compare with 21.

Taking into account that classical validity and hence stability is recursively enumerable, from the way

**CL4**is axiomatized it is obvious that the set of theorems of

**CL4**is recursively enumerable. Furthermore, it is known from [Jap07a] that the

*,*

*-*free fragment (of the set of theorems) of

**CL4**is decidable in polynomial space. Later M. Bauer [Bau14] proved that this fragment is in fact PSPACE-complete. Next, it is a straightforward observation that elementary formulas are derivable in

**CL4**(in particular, from the empty set of premises by Wait) exactly when they are classically valid. Hence

**CL4**is a conservative extension of classical predicate logic: the latter is nothing but the elementary fragment (i.e. the set of all elementary theorems) of the former.

System **CL4** (albeit without = and function letters) was introduced and proven uniform-constructively adequate in [Jap07a].

**Open problems 6.6.2 **

- Is the propositional fragment of CL4 PSPACE-complete?
- Consider the set of the theorems of CL4 that do not contain nonlogical elementary letters. Does this set remain complete with respect to multiform (rather than uniform) validity?
- Try to axiomatize the set of multiformly valid CL4-formulas.

6.7 The brute force system **CL12**

** **

**CL12- formulas** are formulas of the language of CoL that do not contain any general game letters, and do not contain any operators other than , , , , , , ,

**,**

**. As usual, applied to non-atoms, as well as , are understood as abbreviations of their official counterparts.**

** **

**CL12- sequents** are expressions of the form

*E*

_{1},…,

*E*

_{n}*F*where

*E*

_{1},…,

*E*(

_{n}*n*≥0) and

*F*are

**CL12**-formulas. Semantically, such a sequent is understood the same way as the (non-

**CL12**) formula

*E*

_{1}…

*E*

_{n}*F*, so for instance, when we say that the former is

**, we mean that so is the latter. And a**

*logically valid***of the former means a logical solution of the latter.**

*logical solution*

The language of **CL12** is thus incomparable with that of **CL4**. Namely, **CL4** allows general game letters while** CL12** does not; on the other hand, **CL12** allows (uniterated) while **CL4** does not. Due to the presence of ,** CL12** is a very powerful tool for constructing CoL-based applied theories. It is the logical basis for all systems of clarithmetic (CoL-based arithmetic) constructed so far. For this reason, **CL12 **is also the best-studied fragment of CoL, especially from the complexity-theoretic point of view.^{[Jap15] }Below is some terminology used in our axiomatization of **CL12**. Some terms have the same meaning as in the case of **CL4**, and the meanings of some other terms are “slightly” readjusted.

A ** surface occurrence** of a subformula is an occurrence that is not in the scope of any choice operators.

A formula not containing choice operators --- i.e., a formula of the language of classical first order logic --- is said to be ** elementary**. A sequent is

**iff all of its formulas are so. The**

*elementary***||**

*elementarization**F*|| of a formula

*F*is the result of replacing in

*F*all surface occurrences of - and -subformulas by , and all - and -subformulas by . Note that ||F|| is (indeed) an elementary formula. The

**||**

*elementarization**G*

_{1},…,

*G*

_{n }

_{ }*F*|| of a sequent

*G*

_{1},…,

*G*

_{n }

_{ }*F*is the elementary formula ||

*G*

_{1}||…||

*G*|| ||

_{n}*F*||.

A sequent is said to be ** stable** iff its elementarization is classically valid (i.e. provable in some standard version of first-order calculus with constants, function letters and =); otherwise it is

**.**

*unstable* We will be using the notation *F*[*E*] to mean a formula *F *together with some (single) fixed surface occurrence of a subformula *E*. Using this notation sets a context, in which *F*[*H*] will mean the result of replacing in *F*[*E*] that occurrence of *E* by *H*.

Bold-face letters ** G**,

**,… will usually stand for finite sequences of formulas. The standard meaning of an expression such as**

*K***,**

*G**F*,

**should also be clear: this is the sequence consisting of the formulas (order respected) of**

*K***, followed by the formula**

*G**F*, and followed by the formulas of

**.**

*K*We now define **CL12** by the following six ** rules** of inference, where P

*S*means “from premise(s) P conclude

*S*”. Axioms are not explicitly stated, but the set of premises of the Wait rule can be empty, in which case (the conclusion of) this rule acts like an axiom.

1. -*Choose:**G ** **F*[*H _{i}*]

*G*

*F*[

*H*

_{0}

*H*

_{1}], where

*i*∈{0,1}.

2. -*Choose:*** G**,

*E*[

*H*],

_{i}

*K*

*F*

**,**

*G**E*[

*H*

_{0}

*H*

_{1}],

*K*

*F*, where

*i*∈{0,1}.

3. -*Choose:**G ** **F*[*H*(*t*)] *G **F*[*xH*(*x*)], where *t* is either a constant or a variable with no bound occurrences in the premise.

4. -*Choose:*** G**,

*E*[

*H*(

*t*)],

*K*

*F*

**,**

*G**E*[

*xH*(

*x*)],

*K*

*F*, where

*t*is either a constant or a variable with no bound occurrences in the premise.

5. *Replicate:*** G**,

*E*,

*K**, E*

*F*

**,**

*G**E*,

*K*

*F*.

6. *Wait: G*_{1}*F*_{1}, …, *G*_{n}*F _{n }*

*K**E*(

*n*≥0), where

*K**E*is stable and the following four conditions are satisfied:

- Whenever the conclusion has the form
*K**E*[*H*_{0}*H*_{1}], both*K**E*[*H*_{0}] and*K**E*[*H*_{1}] are among the premises. - Whenever the conclusion has the form
,*L**J*[*H*_{0}*H*_{1}],*M**E*, both,*L**J*[*H*_{0}],*M**E*and,*L**J*[*H*_{1}],*M**E*are among the premises.

- Whenever the conclusion has the form
*K**E*[*xH*(*x*)], for some variable*y*not occurring in the conclusion,*K**E*[*H*(*y*)] is among the premises.

- Whenever the conclusion has the form
,*L**J*[*xH*(*x*)],*M**E*, for some variable*y*not occurring in the conclusion,,*L**J*[*H*(*y*)],*M**E*is among the premises.

Each rule --- seen bottom-up --- encodes an action that a winning strategy should take in a corresponding situation, and the name of each rule is suggestive of that action. For instance, Wait (indeed) prescribes the strategy to wait till the adversary moves. This explains why we have called “Replicate” the rule which otherwise is nothing but what is commonly known as Contraction.

A **CL12**-** proof** of a sequent

*S*is a sequence

*S*

_{1},…,

*S*of sequents, with

_{n}*S*=

_{n}*S*, such that each

*S*follows by one of the rules of

_{i}**CL12**from some (possibly empty in the case of Wait, and certainly empty in the case of

*i*=1) set P of premises such that P ⊆ {

*S*

_{1},…,

*S*

_{i}_{-1}}. A

**CL12**-

**of a formula**

*proof**F*is understood as a

**CL12**-proof of the empty-antecedent sequent

*F*. Whether it be a sequent or a formula, “

**in**

*provable***CL12**”, of course, means “has a

**CL12**-proof”.

The uniform-constructive adequacy theorem stated earlier for all systems of this section extends without changes from **CL12**-formulas to **CL12**-sequents, understanding each such sequent *E*_{1},…,*E _{n}*

*F*as the (non-

**CL12**) formula

*E*

_{1}…

*E*

_{n}*F*.

**CL12** is a conservative extension of classical logic. That is, an elementary sequent *E*_{1},…,*E _{n}*

*F*is provable in

**CL12**iff the formula

*E*

_{1}…

*E*

_{n}*F*is valid in the classical sense. This is an immediate corollary of the adequacy theorem for

**CL12**. But this fact can also be easily verified directly. Indeed, assume

*E*

_{1},…,

*E*,

_{n}*F*are elementary formulas. Note that then the elementarization of

*E*

_{1},…,

*E*

_{n}*F*is

*E*

_{1}…

*E*

_{n}*F*. If the latter is classically valid, then

*E*

_{1},…,

*E*

_{n}*F*follows from the empty set of premises by Wait. And if

*E*

_{1}…

*E*

_{n}*F*is not classically valid, then

*E*

_{1},…,

*E*

_{n}*F*cannot be the conclusion of any of the rules of

**CL12**except Replicate. However, applying (bottom-up) Replicate does not take us any closer to finding a proof of the sequent, as the premise still remains an unstable elementary sequent.

**Example 6.7.1** In this example,✕ is a binary function letter and ^{3} is a unary function letter. We write *x*✕*y* and *x*^{3} instead of ✕(*x*,*y*) and ^{3}(*x*), respectively. The following sequence of sequents is a CL12-proof of its last sequent.

1. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *t*=*s*✕*s*, *r*=*t*✕*s* *r*=*s*^{3} Wait: (no premises)

2. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *t*=*s*✕*s*, *r*=*t*✕*s* *y*(*y*=*s*^{3}) -Choose: 1

3. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *t*=*s*✕*s*, *z*(*z*=*t*✕*s*) *y*(*y*=*s*^{3}) Wait: 2

4. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *t*=*s*✕*s*, *y**z*(*z*=*t*✕*y*) *y*(*y*=*s*^{3}) -Choose: 3

5. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *t*=*s*✕*s*, *x**y**z*(*z*=*x*✕*y*) *y*(*y*=*s*^{3}) -Choose: 4

6. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *z*(*z*=*s*✕*s*), *x**y**z*(*z*=*x*✕*y*) *y*(*y*=*s*^{3}) Wait: 5

7. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *y**z*(*z*=*s*✕*y*), *x**y**z*(*z*=*x*✕*y*) *y*(*y*=*s*^{3}) -Choose: 6

8. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *x**y**z*(*z*=*x*✕*y*), *x**y**z*(*z*=*x*✕*y*) *y*(*y*=*s*^{3}) -Choose: 7

9. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *x**y**z*(*z*=*x*✕*y*) *y*(*y*=*s*^{3}) Replicate: 8

10. *x* (*x*^{3}= (*x*✕*x*)✕*x*), *x**y**z*(*z*=*x*✕*y*) *x**y*(*y*=x^{3}) Wait: 9

**Exercise 6.7.2** To see the resource-consciousness of **CL12**, show that it does not prove *p**q * (*p**q*)(*p**q*), even though this formula has the form *F**F**F* of a classical tautology. Then show that, in contrast, **CL12 **proves the *sequent* *p**q * (*p**q*)(*p**q*) because, unlike the antecedent of a -combination, the antecedent of a -combination is reusable (trough Replicate).

**Exercise 6.7.3** Show that **CL12** proves *x**y* *p*(*x*,*y*) *x*(*y* *p*(*x*,*y*) *y p*(*x*,*y*)). Then observe that, on the other hand, **CL12** does not prove any of the formulas

* **x**y* *p*(*x*,*y*) *x*(*y* *p*(*x*,*y*) *y p*(*x*,*y*));

* **x**y* *p*(*x*,*y*) *x**y* *p*(*x*,*y*) *x*(*y* *p*(*x*,*y*) *y p*(*x*,*y*));

*x**y* *p*(*x*,*y*) *x**y* *p*(*x*,*y*) *x**y* *p*(*x*,*y*) *x*(*y* *p*(*x*,*y*) *y p*(*x*,*y*));

…

Intuitively, this contrast is due to the fact that, even though both *A* and *A* = *A**A**A**… *are resources allowing to reuse *A* any number of times, the “branching” form of reusage offered by *A* is substantially stronger than the “parallel” form of reusage offered by *A*. *x**y* *p*(*x*,*y*) *x*(*y* *p*(*x*,*y*) *y* *p*(*x*,*y*)) is a valid principle of CoL while *x**y* *p*(*x*,*y*) *x*(*y* *p*(*x*,*y*) *y* *p*(*x*,*y*)) is not.

The uniform-constructive adequacy theorem for **CL12,** generalized from **CL12**-formulas to **CL12**-sequents, holds in the following strong form:

1. A **CL12**-sequent is provable in **CL12** iff it is logically valid.

2. There is an effective procedure which takes an arbitrary **CL12**-proof of an arbitrary **CL12**-sequent *G**F* and constructs a linear amplitude, constant space and linear time logical solution of *G**F*.

Thus, every cirquent either has a very efficient logical solution (as efficient as it gets), or no logical solution solution at all.

We say that a **CL12**-formula *F* is a ** logical consequence** of

**CL12**-formulas

*E*

_{1},…,

*E*(

_{n}*n*≥0) iff

**CL12**proves the sequent

*E*

_{1},…,

*E*

_{n }*F*.

The following rule, which we (also) call ** Logical Consequence** (

**), will be the only logical rule of inference in**

*LC***CL12**-based applied systems:

*E*_{1},…,*E _{n}*

*F,*

*where F is a logical consequence of*

*E*

_{1},…,

*E*.

_{n}Remember that, philosophically speaking, computational *resources* are symmetric to computational problems: what is a problem for one player to solve is a resource that the other player can use. Namely, having a problem *A* as a computational resource intuitively means having the (perhaps externally provided) ability to successfully solve/win *A*. For instance, as a resource, *x**y*(*y*=*x*^{2}) means the ability to tell the square of any number. According to the following thesis, logical consequence lives up to its name:

**Thesis 6.7.5** Assume *E*_{1},…,*E _{n}* and

*F*are

**CL12**-formulas such that there is a *-independent (whatever interpretation *) intuitive description and justification of a winning strategy for

*F**, which relies on the availability and “recyclability” --- in the strongest sense possible --- of

*E*

_{1}*,…,

*E** as computational resources. Then

_{n}*F*is a logical consequence of

*E*

_{1},…,

*E*.

_{n}**Example 6.7.6** Imagine a **CL12**-based applied formal theory, in which we have already proven *x*(*x*^{3}=(*x*✕*x*)✕*x*) (the meaning of “cube” in terms of multiplication) and *x**y**z*(*z*=*x*✕*y*) (the computability of multiplication), and now we want to derive *x**y*(*y*=*x*^{3}) (the computability of “cube”). This is how we can reason to justify *x**y*(*y*=*x*^{3}):

*Consider any s (selected by Environment for x in **x**y*(*y*=*x*^{3})*). We need to find s*^{3}*. Using the resource **x**y**z*(*z*=*x*✕*y*)*,* *we first find the value t of s*✕*s, and then the value r of t*✕*s. According to **x*(*x*^{3}=(*x*✕*x*)✕*x*)*, such an r is the sought s*^{3}*.*

Thesis 6.7.5 promises that the above intuitive argument will be translatable into a **CL12**-proof of

*x*(*x*^{3}=(*x*✕*x*)✕*x*), *x**y**z*(*z*=*x*✕*y*) *x**y*(*y*=*x*^{3})

(and hence the succedent *x**y*(*y*=*x*^{3}) will be derivable in the theory by LC as the formulas of the antecedent are already proven). Such a proof indeed exists --- see Example 6.7.1.

While Thesis 6.7.5 is about the *completeness* of LC, the following Theorems 6.7.7 and 6.7.8 are about *soundness*, establishing that LC preserves computability, and does so in a certain very strong sense. It is these two theorems to which **CL12** (LC, that is) owes its appeal as a logical basis for complexity-oriented applied theories. Theorem 6.7.7 carries good news for the cases where time efficiency is of main concern, and otherwise we are willing to settle for at least linear space. Theorem 6.7.8 does the same but for the cases where the primary concern is space efficiency --- namely, when we want to keep the latter sublinear. These theorems use the term “** native magnitude**”, by which, for a sequent

*S*, we mean the greatest of all constants (here seen as the corresponding natural numbers) that appear in

*S*, or 0 is there are no constants in

*S*.

**Theorem 6.7.7** There is an effective procedure which takes an arbitrary **CL12**-proof P of an arbitrary **CL12**-sequent *E*_{1},…,*E _{n }*

*F*, arbitrary HPMs

*N*

_{1},…,

*N*and constructs an HPM

_{n}*M*such that the following holds:

Assume * is an interpretation and *a*,*s*,*t* are unary arithmetical functions such that:

- For each
*i*∈{1,…,*n*},*N*_{i}_{ }is an*a*amplitude,*s*space and*t*time solution of*E**._{i} - For any
*x*,*a*(*x*)≥max(*x*,*c*), where*c*is the native magnitude of*E*_{1},…,*E*_{n }*F*. - For any
*x*,*s*(*x*)≥*x*. - For any
*x*,*t*(*x*)≥*x*.

Then thre is a number *b* which only depends on P such that, with *R* abbreviating *a ^{b}*(

*y*),

*M*is a solution of

*F** which runs in amplitude

*R*, space O(

*s*(

*R*)) and time O(

*t*(

*R*)).

**Theorem 6.7.8** There is an effective procedure which takes an arbitrary **CL12**-proof P of an arbitrary **CL12**-sequent *E*_{1},…,*E _{n }*

*F*, arbitrary HPMs

*N*

_{1},…,

*N*and constructs an HPM

_{n}*M*such that the following holds:

Assume * is an interpretation and *a*,*s*,*t* are unary arithmetical functions such that:

- For each
*i*∈{1,…,*n*},*N*_{i}_{ }is an*a*amplitude,*s*space and*t*time solution of*E**._{i} - For any
*x*,*a*(*x*)≥max(*x*,*c*), where*c*is the native magnitude of*E*_{1},…,*E*_{n}*F*. - For any
*x*,*s*(*x*)≥log(*x*). - For any
*x*,*t*(*x*)≥*x*and*t*(*x*)≥*s*(*x*).

Then there is are numbers *b*,*d* which only depend on P such that, with *R* abbreviating *a ^{b}*(

*y*),

*M*is a solution of

*F** which runs in amplitude

*R*, space O(

*s*(

*R*)) and time O((

*t*(

*R*))

*).*

^{d}**CL12 **was introduced in** **[Jap10], and proven to be uniform-constructively adequate in [Jap12c]. Theorems 6.7.7 and 6.7.8 were proven in [Jap15].

**Open problems 6.7.9 **

- Add the sequential connectives , to the language of CL12 and adequately axiomatize the corresponding logic.
- Try to axiomatize the set of multiformly valid CL12-sequents.
- Along with elementary game letters, allow also general game letters in the language of CL12, and try to axiomatize the set of valid sequents of this extended language.