(CoL)

Section 1

The philosophy of CoL

1.1     Syntax vs. semantics

1.2     Why game semantics?

1.3     CoL vs. classical logic

1.4     CoL vs. linear logic

1.5     CoL vs. intuitionistic logic

1.6     CoL vs. independence-friendly logic

1.7   The ‘from semantics to syntax’ paradigm

1.1 Syntax vs. semantics

A separate question, of course, is what counts as a semantics. The model example of a semantics with a capital ‘S’ is that of classical logic. But in the logical literature this term often has a more generous meaning than what CoL is ready to settle for. As pointed out, CoL views logic as a universal-utility tool. So, a capital-‘S’-semantics should be non-specific enough, and applicable to the world in general rather than some very special and artificially selected (worse yet, artificially created) fragment of it. Often what is called a semantics is just a special-purpose apparatus designed to help analyze a given syntactic construction rather than understand and navigate the outside world. The usage of Kripke models as a derivability test for intuitionistic formulas, or as a validity criterion in various systems of modal logic is an example. An attempt to see more than a technical, syntax-serving instrument in this type of lowercase-‘s’-semantics might create a vicious circle: a deductive system L under question is “right” because it derives exactly the formulas that are valid in a such and such Kripke semantics; and then it turns out that the reason why we are considering the such and such Kripke semantics is that ... it validates exactly what L derives.

1.2 Why game semantics?

For CoL, game is not just a game.  It is a foundational mathematical concept on which a powerful enough logic (=semantics) should be based. This is so because, as noted, CoL sees logic as a “real-life navigational tool”, and it is games that appear to offer the most comprehensive, coherent, natural, adequate and convenient mathematical models for the very essence of all “navigational” activities of agents: their interactions with the surrounding world. An agent and its environment  translate into game-theoretic terms as two players; their actions as moves; situations arising in the course of interaction as  positions; and success or failure as wins or losses.

It is natural to require that the interaction strategies of the party that we have referred to as an “agent” be limited to algorithmic ones, allowing us to henceforth call that player a machine.  This is a minimum condition that any non-esoteric game semantics would have to satisfy. On the other hand, no restrictions can or should be imposed on the environment, who represents a capricious user, the blind forces of nature, or the devil himself. Algorithmic activities being synonymous to computations, games thus represent computational problems --- interactive tasks performed by computing agents, with computability meaning winnability, i.e. existence of a machine that wins the game against any possible (behavior of the) environment.

In the 1930s, in the form of the celebrated Church-Turing thesis, mankind came up with what has been perceived as an ultimate mathematical definition of the precise meaning of algorithmic solvability. Curiously or not, such a definition was set forth and embraced before really having attempted to answer the seemingly more basic question about what computational problems are --- the very entities that may or may not have algorithmic solutions in the first place. The tradition established since then in theoretical computer science by computability simply means Church-Turing computability of functions, as the task performed by every Turing machine is nothing but receiving an input x and generating the output f(x) for some function f.

Yet most tasks that computers and computer networks perform are interactive, with strategies not always allowing themselves to be adequately understood as functions. To see this, it is sufficient to just reflect on the behavior of one's personal computer. The job of your computer is to play one long game against you. Now, have you noticed your faithful servant getting slower every time you use it? Probably not. That is because the computer is smart enough to follow a non-functional strategy in this game. If its strategy was a function from positions (interaction histories) to moves, the response time would inevitably keep worsening due to the need to read the entire, continuously lengthening interaction history every time before responding. Defining strategies as functions of only the latest moves is also not a way out. The actions of your computer certainly depend on more than your last keystroke.

Two main concepts on which the semantics of CoL is based are those of static games (defined later) and their winnability. Correspondingly, the philosophy of CoL relies on two beliefs that, together, present what can be considered an interactive version of the Church-Turing thesis:

Thesis 1.2.1

      (1) The concept of static games is an adequate formal counterpart of our intuition of (“pure”, speed-independent) interactive computational problems.

      (2) The concept of winnability is an adequate formal counterpart of our intuition of algorithmic solvability of such problems.

So far games in logic have been mostly used to find models and semantical justifications for syntactically introduced popular systems such as intuitionistic logic or linear logic. For instance: Lorenzen’s [Lor61, Fel85] game semantics was created for the purpose of justifying intuitionistic logic; Hintikka’s [Hin73] game-theoretic semantics was originally meant to provide an alternative semantics for classical logic; Blass’ [Bla92] game semantics was mainly motivated by the needs of linear logic, and so were the game-semantical approaches elaborated by Abramsky, Jagadeessan [Abr94] and others. In this respect, CoL turns the tables around and views games as foundational entities in their own right.  It starts with identifying the most basic and meaningful operations on games. Understanding those operations as logical operators, it then looks at the logics induced by the corresponding concept of validity, regardless of how unusual such logics may turn out. There is no target syntactic construction to serve.

1.3 CoL vs. classical logic

Computability in the traditional Church-Turing sense is a special case of winnability --- winnability restricted to two-step (input/output, question/answer) interactive problems. So is the classical concept of truth, which is nothing but winnability restricted to propositions, viewed by CoL as zero-step problems, i.e., games with no moves that are automatically won by the machine when true and lost when false. This way, the game  semantics of CoL is a generalization, refinement and conservative extension of that of classical logic.

1.4 CoL vs. linear logic

CoL is a semantically conceived logic, and so far its syntax has only been partially  developed.  In a sense, this situation is opposite to the case with linear logic [Gir87], where a “full” syntactic construction existed right at the beginning, but where a really good formal semantics convincingly justifying the resource intuitions traditionally associated with that construction is still being looked for. (Those who want to exclaim "But what about, say, the phase or coherence space semantics?!" are kindly asked to read the rest of this subsection as well as Subsection 1.7). In fact, the semantics of CoL can be seen as such a justification, but only in a limited sense explained below.

The set of valid formulas in a certain fragment of the otherwise more expressive language of CoL forms a logic which is similar to but by no means the same as linear logic.  When no exponentials are involved, the two logics typically agree on short and simple formulas. For instance, both logics reject  P  P  P   and accept P  P  P, with classical-shape propositional connectives here and later understood as the corresponding multiplicative operators of linear logic, and square-shape operators as additives ( = “with”,  = “plus”). Similarly, both logics reject P  P and accept P  P. On the other hand, CoL disagrees with linear logic on many more evolved formulas. E.g., CoL validates the following two principles rejected even by affine logic, i.e., linear logic with the weakening rule:

(P  Q)  (R  S)     (P  R)  (Q  S)  (Blass’s [Bla92] principle);

(P  (R  S)) (Q  (R  S)) ((P  Q)  R)   ((P  Q)  S)    (P  Q)  (R  S).

With  and , which are CoL’s counterparts of the exponentials !,? of linear logic,  disagreements can be observed already at the level of very short formulas, such as P  P, accepted by CoL but rejected by affine logic. Generally, every formula provable in affine logic is valid in CoL but not vice versa.

Neither the similarities nor the discrepancies are a surprise. The philosophies of CoL and linear logic overlap in their pursuit to develop a logic of resources. But the ways this philosophy is materialized are rather different. CoL starts with a mathematically strict and intuitively convincing semantics, and only after that, as a natural second step, asks what the corresponding logic and its possible axiomatizations are. On the other hand, it would be accurate to say that linear logic started directly from the second step. Even though certain companion semantics were provided for it from the very beginning, those are not quite what we earlier agreed to call capital-‘S’. As a formal theory of resources (rather than that of phases or coherence spaces), linear logic has been introduced syntactically rather than semantically, essentially by taking classical sequent calculus and deleting the rules that seemed unacceptable from a certain intuitive, naive and never formalized "resource-semantical" point of view. In the absence of a clear formal concept of resource-semantical truth or validity, the question about whether the resulting system was complete could not even be meaningfully asked. In this process of syntactically rewriting classical logic some innocent, deeply hidden principles could have easily gotten victimized. CoL believes that this is exactly what happened, with the above-mentioned formulas separating it from linear logic, along with many other principles, viewed as babies thrown out with the bath water. Of course, many retroactive attempts have been made to find semantical (often game-semantical) justifications for linear logic. Technically it is always possible to come up with some sort of a formal semantics that matches a given target syntactic construction, but the whole question is how natural and meaningful such a semantics is in its own rights, and how adequately it corresponds to the logic’s underlying philosophy and ambitions. Unless, by good luck, the target system really is “the right logic”, the chances of a decisive success when following the odd scheme from syntax to semantics could be rather slim. The natural scheme is from semantics to syntax. It matches the way classical logic evolved and climaxed in Gödel’s completeness theorem. And, as we now know, this is exactly the scheme that computability logic, too, follows.

With the two logics in a sense competing for the same market, the main --- or perhaps only --- advantage of linear logic over CoL is its having a nice and simple syntax. In a sense, linear logic is (rather than has) a beautiful syntax; and computability logic is (rather than has) a meaningful semantics. An axiomatization of CoL in the full generality of its language has not been found yet. Only certain fragments  of it have been axiomatized, including the one corresponding to the multiplicative-additive fragment of linear logic. Such axiomatizations tend to be more involved than that of linear logic, so the syntactic simplicity advantage of linear logic will always remain. Well, CoL has one thing to say: simplicity is good, yet, if it is most important, then nothing can ever beat ... the empty logic.  The latter, just like linear logic, is sound with respect to  resource semantics, whatever  such a semantics means;  it is sound  with respect to  any semantics for that matter.

From CoL’s perspective, classical logic and (loosely understood) linear logic can be seen as two extremes within its all-unifying resource- (game-) semantical vision. Specifically, the main difference between linear logic and classical logic is that the former sees all occurrences of the same atom in a formula as different copies of the same resource, while the latter sees such occurrences as the same single copy, simply written at different places for technical reasons.  So, linear logic rejects $1$1$1 because in the antecedent we have one dollar while in the consequent two, with the possibility to buy an apple with one and an orange with the other. On the other hand, classical logic accepts this principle because it sees a single dollar in the consequent, written twice for some strange reason; if the first conjunct of the consequent is spent buying an apple, the second conjunct is also automatically spent on the same apple, with no money remaining for oranges. As for CoL, it allows us to write expressions where all occurrences of $1 stand for the same one-dollar bill, or all stand for separate bills, or we have a mixture of these two, where some occurrences stand for the same bill while some other occurrences in the same expression stand for different bills.

Blass [Bla92] was the first to attempt a game-semantical justification for linear logic. This goal was only partially achieved, as the resulting logic, just like the above-discussed fragment of CoL, turned out to validate more principles than linear logic does. It should be pointed out that the multiplicative-additive fragment of the logic induced by Blass’ semantics coincides with the corresponding fragment of CoL. This does not extend to the full language of linear logic though. For instance, Blass’ semantics validates the following principle which is invalid in CoL: ^[Jap12a]  

P  ((P  P  P)  (P  P  P))    P.

In full generality, the “linear-logic fragment” of CoL is strictly between affine linear logic and the logic induced by Blass’ semantics.^[Jap09a]

1.5 CoL vs. intuitionistic logic

From CoL’s perspective, the situation with intuitionistic logic [Hey71] is rather similar to what we had with linear logic. Intuitionistic logic is another example of a syntactically conceived logic. Despite decades of efforts, no fully convincing semantics has been found for it. Lorenzen’s [Lor61] game semantics, which has a concept of validity without having a concept of truth, has been perceived as a technical supplement to the existing syntax rather than as having independent importance. Some other semantics, such as Kleene’s realizability [Kle52] or Gödel’s Dialectica interpretation [Göd58], are closer to what we might qualify as capital-‘S’. But, unfortunately, they validate certain principles unnegotiably rejected by intuitionistic logic.

Just like this was the case with linear logic, the set of valid formulas in a certain fragment of the language of CoL forms a logic which is properly stronger^{[Mez10, Jap07b]} than Heyting’s intuitionistic logic. However, the two come “much closer” to each other than CoL and linear logic do. The shortest known formula separating intuitionistic logic from the corresponding fragment of CoL is

(P Q R)  ( P S T)  (P Q)  (P R)  ( P S)  ( P T),

where , , ,  are CoL’s counterparts of the intuitionistic implication, negation, disjunction and conjunction, respectively.

Just like the resource philosophy of CoL overlaps with that of linear logic, so does its algorithmic philosophy with the constructivistic philosophy of intuitionism. The difference, again, is in the ways this philosophy is materialized.  Intuitionistic logic has come up with a “constructive syntax” without having an adequate underlying formal semantics, such as a clear concept of truth in some constructive sense. This sort of a syntax was essentially obtained from the classical one by banning the offending law of  the excluded middle. But, as in the case of linear logic, the critical question immediately springs out: where is a guarantee that together with excluded middle some innocent principles would not be expelled just as well? The constructivistic claims of CoL, on the other hand, are based on the fact that it defines truth as algorithmic solvability. The philosophy of CoL does not find the term constructive syntax meaningful unless it is understood as soundness with respect to some constructive semantics, for only a semantics may or may not be constructive in a reasonable sense. The reason for the failure of P  P in CoL is not that this principle ... is not included in its axioms. Rather, the failure of this principle is exactly the reason why this principle, or anything else entailing it, would not be among the axioms of a sound system for CoL. Here “failure” has a precise semantical meaning. It is non-validity, i.e. existence of a problem A for which A  A is not algorithmically solvable. 

It is also worth noting that, while intuitionistic logic irreconcilably defies classical logic, computability logic comes up with a peaceful solution acceptable for everyone. The key is the expressiveness of its language, that has (at least) two versions for each traditionally controversial logical operator, and particularly the two versions  and  of disjunction. The semantical meaning of  conservatively extends --- from moveless games to all games --- its classical meaning, and the principle P  P survives as it represents  an always-algorithmically-solvable combination of problems, even if solvable in a sense that some constructivistically-minded might pretend to fail to understand. And the semantics of , on the other hand, formalizes and conservatively extends a different, stronger meaning which apparently every constructivist associates with disjunction. As expected, then P  P turns out to be semantically invalid. CoL's proposal for settlement between classical and constructivistic logics then reads: ‘If you are open (=classically) minded, take advantage of the full expressive power of CoL; and if you are constructivistically minded, just identify a collection of the operators whose meanings seem constructive enough to you, mechanically disregard everything containing the other operators, and put an end to those fruitless fights about what deductive methods or principles should be considered right and what should be deemed wrong’.

1.6 CoL vs. independence-friendly logic

Relatively late developments [Jap06c, Jap11b, Xu14] in CoL made it possible to switch from formulas to the more flexible and general means of expression termed cirquents. The main distinguishing feature of the latter is that they allow to account for various sorts of sharing between subexpressions. After such a generalization, independence-friendly (IF) logic [Hin73] became a yet another natural fragment of CoL.^{[Jap11b, Xu14, Xu16]}  As such, it is a conservative fragment, just like classical logic and unlike linear or intuitionistic logics. This is no surprise because, just like CoL and unlike linear or intuitionistic logics, IF logic is a semantically conceived logic.

In fact, for a long time, IF logic remained a pure semantics without a syntax. In its full first-order language, IF logic is simply known to be unaxiomatizable. As for the propositional fragment, there was none because the traditional approaches to IF logic had failed to offer any non-classical semantics for propositional connectives.  Under CoL’s cirquent-based approach to IF logic this is no longer so, and “independence-friendly” propositional connectives are just as meaningful as their quantifier counterparts. Based on this new treatment, a sound and complete axiomatization for propositional IF logic has been later found.^{[Xu14, Xu16]}

1.7 The ‘from semantics to syntax’ paradigm

CoL’s favorite ‘from semantics to syntax’ paradigm for developing a logic can be characterized as consisting of three main stages. The first one can be called the Informal semantics stage, at which the main intuitions are elaborated along with the underlying motivations, and the formal language of the logic is agreed upon.  The second one is the Formal semantics stage, at which those intuitions are formalized as a mathematically strict semantics for the adopted language, and definitions of truth and validity are given. Finally, the third one is the Syntax stage, at which one constructs axiomatizations for the corresponding set of valid principles,   whether in the full language of the logic or some natural fragments of it, and proves the adequacy (soundness and completeness) of such constructions. 

Figure 1.7.1: Three stages of developing a logic

CoL and classical logic went through all three stages in sequence. So did IF logic, even though for a long time it was stuck at the second stage. As for linear and intuitionistic logics, they essentially jumped from the first stage directly to the third stage, skipping the inermediary stage. It is the absence of formal rather than informal semantics that we meant when saying that the two logics were conceived syntactically rather than semantically. Why is such a jump wrong? It is impossible to directly “prove” that the proposed syntax adequately corresponds to the informal-semantical intuitions underlying the logic. After all, Syntax is mathematically well defined while Informal semantics is from the realm of philosophy or intuitions, so an adequacy claim lacks any mathematical meaning. Of course, the same is the case with Formal semantics vs. Informal semantics. But, at least, both are “semantics”, which makes it qualitatively easier to convincingly argue (albeit not prove) that one adequately corresponds to the other. Once such a correspondence claim is accepted, one can prove the adequacy of the syntax by showing that it is sound and complete with respect to the formal semantics. 

The intermediary role of Formal semantics can be compared with that of Turing machines.  Since the intuitive concept of a machine (algorithm) and the mathematical concept of a Turing machine are both about “machines”, it is relatively easy to argue in favor of the (mathematically unprovable) Church-Turing thesis, which claims an adequate correspondence between the two. Once this thesis is accepted, one can relatively easily show --- this time mathematically --- that recursive functions or lambda calculus, too, adequately correspond to our intuitions of machine-computability. Arguing in favor of such a claim directly, without having the intermediary Turing machine model, would not be easy, as recursive definitions or lambda terms do not at all resemble what our intuition perceives as machines.

Based directly on the resource intuitions associated with linear logic, can anyone tell whether, for instance, the principle P  (P  PP)  P should be accepted? An orthodox linear logician might say ‘No, because it is not provable in Girard’s canonical system’. But the whole point is that we are just trying to understand what should be provable and what should not. From similar circularity suffer the popular attempts to “semantically” justify intuitionistic provability in terms of … intuitionistic provability.