Computability Logic

(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. Uniform-constructive soundness:   There is an effective procedure that takes an arbitrary 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 Γ,FF. And the system only has the following two rules of inference:


 

A CL7-proof of a sequent S is a sequence X1,…,Xn  of sequents, where S=Xn, and where each Xi is either an axiom or follows from some earlier sequents of the sequence  by one of the rules of inference. A CL7-proof of a formula 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(FG))((EF)(EG)). 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  (EG)((FG)(EFG)) is valid with  read as  but not as . An example of a classical tautology invalid with all three operators {,,} is Peirce’s Law ((EF)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 

  1. Does Int+ remain complete with respect to multiform (rather than uniform) validity?
  2. 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?
  3. Is the first-order (with quantifiers ,) positive (negation- and absurd-free) intuitionistic logic also adequate with respect to the CoL semantics? If not, could it be axiomatized and how?
  4. 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.
  5. If the preceding task is achieved, then try the first-order version of it as well.
  6. 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 (EF), (EF), E and E as abbreviations of EF, EF, E and E, respectively. We may as well write EF or write EF, understanding these expressions as abbreviations of EF and EF (i.e. EF), respectively.

Definition 6.4.1 A CL15-cirquent (hencefore simply “cirquent”) is a triple C=(F,U,O) where:

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 F1, F2, F3, F4, three undergroups {F1}, {F2,F3}, {F3,F4} and two overgroups {F1,F2,F3}, {F2,F4}. 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

(F1,F1,…, Fn,Fn,  {F1,F1}, …, { Fn,Fn},  {F1,F1}, …, {Fn,Fn}),

where n is any positive integer, and F1,…,Fn 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, Oformula Exchange and Overgroup 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. 

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,O)  of a cirquent as multisets rather than  sequences.   

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: Undergroup Duplication and Overgroup Duplication. The conclusion of Undergroup Duplication is the result of replacing, in the premise, some undergroup 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 FG 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 FG 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 FG (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-proof of a formula 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 FF, 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 (EF)  (GH) (EG)  (FH) (the already mentioned Blass principle), or even the special case (EE)  (EE) (EE)  (EE) 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 in [Xu13] proved that CL15 remains sound with , instead of ,. Completeness, however, is lost in this case because, as already mentioned, the formula F(FFF) F is valid while A(AAA)  A is not.

Open problems 6.4.2  

  1. Is CL15 decidable?
  2. 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.
  3. Replace , with , in the language of CL15. Is the set of valid formulas in this new language  axiomatizable (and how)? 
  4. 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.  EF is also understood as an abbreviation of its standard meaning. To define the system axiomatically, we need certain terminological conventions.

We now define CL13 by the following six rules of inference, where PF 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 ():  F, where F is a stable quasielementary formula, and H is the smallest set of formulas satisfying the following condition:

Rule ():  H  F, where F is a quasielementary formula, and H is the result of replacing in F a surface osubformula EG  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:

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

Rule ():  H  F, where H is the result of replacing in F a semisurface osubformula EG 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 (pp)  (qq) (pq)  (pq) expresses --- or rather implies --- the known fact that, if two predicates p and q are recursively approximable, then so is their intersection pq. The following sequence is a CL13-proof of this formula, re-written into its official form ((pp)  (qq))  ((pq)  (pq)):

  1. (pq)  (pq)                                       ():  (no premises)
  2. (pq)  ((pq)  (pq))                      (): 1
  3. (pq)  (pq)                                      ():  (no premises)
  4. (pq)  ((p q)  (pq))                    (): 3 
  5. (p  (qq))  ((pq)  (pq))           (): 2,4
  6. (pq)  (pq)                                       ():  (no premises)
  7. (pq)  ((pq)  (pq))                      (): 6
  8. (pq)  (pq)                                          ():  (no premises)
  9. (pq)  ((pq)  (pq))                     (): 8
  10. (p  (qq))  ((pq)  (pq))          (): 7,9
  11. ((pp)  q)  ((pq)  (pq))            (): 2,7
  12. ((pp) q)  ((pq)  (pq))          (): 4,9
  13. ((pp)  (qq))  ((pq)  (pq))   (): 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&1Q P&2Q 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 PQ PQ:

  1. pp                        ():  (no premises) 
  2. (p)  p                (): 1
  3. qq                         ():  (no premises)
  4. (pq) q              (): 3
  5. (pQ) Q             (M): 4
  6. (pQ) (pQ)      (): 2,5
  7. (PQ) (PQ)     (M): 6

On the other hand, the formula PQ PQ, i.e. (PQ)  (PQ), 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.  (PQ)  (PQ) 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  (PQ). The latter can be derived only by ()  or (M). Again, let us try (M). The premise in this subcase should be q  (Pq) for some elementary atom q. But the only way q  (Pq)  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 (PP)  (PP) (PP).

Exercise 6.5.4 For which of the four disjunctions {,,,} are the following formulas CL13-provable and for which are not?  (1) PP;   (2) PQ QP;  (3) PP P;  (4) pp p.

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

Open problems 6.5.4 

  1. Consider the first-order version of the language of CL13 with choice (to start with) quantifiers. Adequately axiomatize the corresponding logic.
  2. What is the computational complexity of (the property of provability in) CL13? (Expectation: PSPACE-complete).
  3. 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 EF is also the standard abbreviation.  An elementary CL4-formula is a CL4-formula which contains no choice operators and no general game letters. Our axiomatization of CL4 relies on the following terminology and notation.

We now define CL4 by the following four rules of inference, where PF 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[Hi F[H0H1], 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 (n0), where F is stable, and E is a set of formulas satisfying the following two conditions:

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

            2. Whenever F has the form F[xG(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(s)], where P is an n-ary (n³0) general game letter, t and s are 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 xy(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. xy(P(x)  P(y))    Wait: 3 

On the other hand, CL4 does not prove yx(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” yx(P(x)  P(y)) of  yx(P(x)  P(y)) is provable: 

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

2. yx(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, yx(P(x)  P(y))  is indeed right; and yes, yx(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, ppp is indeed right; and yes, PPP (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 EF means provability of both  EF and FE. 

1. Yes:  PP.

2.  No:  PP. Compare with 1.

3.  Yes:  PP   P.

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

5.  Yes:  P PP.

6.  Yes:  (PQ)  (PR) P  (QR).

7.  No:   P  (QR) (PQ)  (PR). Compare with 6,8.

8.  Yes:  p  (QR) (pQ)  (pR). 

9.  No:    p (QR) (pQ)  (pR). Compare with 8.

10. Yes:  (PP)  (PP)  (PP)  (PP). 

11. Yes:  (P  (RS))  (Q  (RS))  ((PQ)  R)  ((PQ)  S) (PQ)  (RS).

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:  xyP(x,y)  yxP(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:  xy(y=f(x)).

20. No:    xy(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 
  1. Is the propositional fragment of CL4 PSPACE-complete?
  2. 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?
  3. 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 E1,…,En  F where E1,…,En (n0) and F are CL12-formulas. Semantically, such a sequent is understood the same way as the (non-CL12) formula E1En  F, so for instance, when we say that the former is logically valid, we mean that so is the latter. And a logical solution of the former means a logical solution of the latter.

 

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 elementary iff all of its formulas are so. The 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 ||G1,…,Gn  F|| of a sequent G1,…,Gn  F  is the elementary formula ||G1||||Gn||  ||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,K,… will usually stand for finite sequences of formulas. The standard meaning of an expression such as G,F,K  should also be clear: this is the sequence consisting of the formulas (order respected) of G, followed by the formula F, and followed by the formulas of K.

We now define CL12 by the following six rules of inference, where PS 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[Hi]    G  F[H0H1],   where i{0,1}.

            2. -Choose:  G, E[Hi], K   F     G, E[H0H1], 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: G1F1, …, GnFn   KE   (n0),  where KE is stable and the following four conditions are satisfied:

·       Whenever the conclusion has the form KE[H0H1], both KE[H0] and KE[H1] are among the premises. 

·       Whenever the conclusion has the form L, J[H0H1], M  E,   both  L, J[H0], M  E  and  L, J[H1], M  E  are among the premises. 

·       Whenever the conclusion has the form KE[xH(x)], for some variable y not occurring in the conclusion, KE[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 S1,…,Sn of sequents, with Sn =S, such that each Si follows  by one of the rules of 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 {S1,…,Si-1}. A CL12-proof of a formula F is understood as a CL12-proof of the empty-antecedent sequent  F. Whether it be a sequent or a formula, “provable in 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 E1,…,En  F as the (non-CL12) formula E1En  F.

Just like all other logics of this section, CL12 is a conservative extension of classical logic. That is, an elementary sequent E1,…,En  F is provable in CL12 iff the formula E1En  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 E1,…,En,F are elementary formulas. Note that then the elementarization of E1,…,En  F is E1En  F. If the latter is classically valid, then E1,…,En  F follows from the empty set of premises by Wait. And if E1En  F is not classically valid, then E1,…,En  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 xy and x3 instead of (x,y) and 3(x), respectively. The following sequence of sequents is a CL12-proof of its last sequent.

1.   x (x3= (xx)x),  t=ss, r=ts   r=s3                                        Wait: (no premises)

2.   x (x3= (xx)x),  t=ss, r=ts   y(y=s3)                                  -Choose: 1

3.   x (x3= (xx)x),  t=ss,  z(z=ts)  y(y=s3)                           Wait: 2

4.   x (x3= (xx)x),  t=ss,  yz(z=ty)  y(y=s3)                        -Choose: 3

5.   x (x3= (xx)x),  t=ss, xyz(z=xy)  y(y=s3)                    -Choose: 4

6.   x (x3= (xx)x),  z(z=ss), xyz(z=xy)  y(y=s3)             Wait: 5

7.   x (x3= (xx)x),  yz(z=sy), xyz(z=xy)  y(y=s3)         -Choose: 6

8.   x (x3= (xx)x),  xyz(z=xy), xyz(z=xy)  y(y=s3)    -Choose: 7

9.   x (x3= (xx)x),  xyz(z=xy)  y(y=s3)                               Replicate: 8

10. x (x3= (xx)x),  xyz(z=xy)  xy(y=s3)                          Wait: 9


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

Exercise 6.7.3 Show that CL12 proves xy 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

                                               xy p(x,y   x(y p(x,y) y p(x,y));

                        xy p(x,y)  xy p(x,y)    x(y p(x,y) y p(x,y));

 xy p(x,y)  xy p(x,y) xy 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 = AAAare 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.  xy p(x,y)   x(y p(x,y) y p(x,y)) is a valid principle of CoL while xy 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:


Theorem 6.7.4

            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 GF and constructs a linear amplitude, constant space and linear time logical solution of GF.

 

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  E1,…,En (n0) iff CL12 proves the sequent E1,…,En  F.

The following rule, which we (also) call Logical Consequence (LC), will be the only logical rule of inference in CL12-based applied systems:

E1,…,En   F,   where F is a logical consequence of E1,…,En.

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, xy(y=x2) 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 E1,…,En 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 E1*,…,En* as computational resources.   Then F is a logical consequence of E1,…,En.

Example 6.7.6 Imagine a CL12-based applied formal theory, in which we have already proven two facts: x(x3=(xx)x) (the meaning of  “cube” in terms of multiplication) and xyz(z=xy) (the computability of multiplication), and now we want to derive xy(y=x3) (the computability of “cube”). This is how we can reason to justify xy(y=x3): 

Consider any s (selected by Environment for x in xy(y=x3)). We need to find s3. Using the resource xyz(z=xy), we first find the value t of ss, and then  the value r of ts. According to x(x3=(xx)x), such an r is the sought s3.

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

x(x3=(xx)x), xyz(z=xy)  xy(y=x3)

(and hence the succedent xy(y=x3) 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 E1,…,En  F, arbitrary HPMs  N1,…,Nn and constructs an  HPM  M such that the following holds:

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

Then thre is a number b which only depends on P such that, with R abbreviating ab(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 E1,…,En  F, arbitrary HPMs  N1,…,Nn and constructs an  HPM  M such that the following holds:

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

Then there is are numbers b,d which only depend on P such that, with R abbreviating ab(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

  1. Add the sequential connectives , to the language of CL12 and adequately axiomatize the corresponding logic.
  2. Try to axiomatize the set of  multiformly valid CL12-sequents.
  3. 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.