Fundamentals of computability logic 2020
Giorgi Japaridze
TL;DR
This paper provides a comprehensive survey of computability logic, explaining its fundamental concepts and significance in the field of logic and computation.
Contribution
It offers an accessible overview of computability logic, including its core principles and recent developments, serving as a foundational resource.
Findings
Clarifies the core principles of computability logic
Summarizes recent advancements in the field
Provides an extended online resource for further study
Abstract
This article is a semitutorial-style survey of computability logic. An extended online version of it is maintained at http://www.csc.villanova.edu/~japaridz/CL/ .
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms
Fundamentals of computability logic 2020
Giorgi Japaridze
Villanova University and
Institute of Philosophy, Russian Academy of Sciences
Contents
1 Introduction
Not to be confused with the generic term “computational logic”, computability logic (CoL) is the proper name of a philosophical platform and mathematical framework for developing ever more expressive computationally meaningful extensions of traditional logic. The main pursuit of this ongoing long-term project is to offer a convenient language for specifying computational tasks and relations between them in a systematic way, and to provide a deductive apparatus for systematically telling what can be computed and how. This line of research was officially introduced in [14] and developed in a series [3]-[4],[14]-[43],[45],[47]-[48],[51]-[55] of subsequent papers.
Under the approach of CoL, formulas represent computational problems, logical operators stand for operations on such entities, and “truth” is seen as computability. Computational problems, in turn, are understood in their most general, interactive sense, and are mathematically construed as games played by a machine against its environment, with computability meaning existence of a machine (algorithmic strategy) that always wins.
CoL understands propositions or predicates of traditional logic as games with no moves, automatically won by the machine when true and lost when false. This naturally makes the classical concept of truth a special case of computability — computability by doing nothing. Further, all operators of classical logic are conservatively generalized from moveless games to all games, which eventually makes classical logic a conservative fragment of the otherwise much more expressive CoL. Based on the overall philosophy and intuitions associated with intuitionistic and linear logics, the latter can also be seen as special fragments of CoL, even though, unlike classical logic, “not quite” conservative ones.
A long list of related or unrelated game semantics can be found in the literature proposed by various authors. Out of those, Blass’s [6] game semantics, which in turn is a refinement of Lorenzen’s [46] dialogue semantics, is the closest precursor of the semantics of CoL, alongside with Hintikka’s [13] game-theoretic semantics. More often than not, the motivation for studying games in logic has been to achieve a better understanding of some already existing systems, such as intuitionistic ([5, 9, 46]), classical ([13]) or linear ([1, 6]) logics. In contrast, CoL’s motto is that logic should serve games rather than the other way around. For logic is meant to be the most general and universal intellectual tool for navigating real life; and it is games that offer the most adequate 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 successes or failures as wins or losses.
This chapter is a semitutorial-style introduction to the basics of CoL, containing many definitions, illustrations, claims and even exercises but no technical proofs whatsoever. It is primarily focused on the language of CoL and its semantics, paying considerably less attention to the associated proof theory or applications. A more detailed and continuously updated survey of the subject is maintained online at [44].
2 Games
Computability is a property of computational problems and, before attempting to talk about the former, we need to agree on the precise meaning of the latter. According to the mainstream understanding going back to Church [8] and Turing [50], a computational problem is a function—more precisely, the task of systematically generating the values of that function at different arguments. Such a view, however, as more and more researchers have been acknowledging [11], is too narrow. Most tasks performed by computers are interactive, far from being as simple as functional transformations from inputs to outputs. Think of the work of a network server for instance, where the task is to maintain a certain infinite process, with incoming (“input”) and outgoing (“output”) signals interleaved in some complex and probably unregulated fashion, depending on not only immediately preceding signals but also various events taken place in the past. In an attempt to advocate for the conventional view of computational problems, one might suggest to understand an interactive computational task as the task of repeatedly computing the value of a function whose argument is not just the latest input but the whole preceding interaction. This is hardly a good solution though, which becomes especially evident with computational complexity considerations in mind. If the task performed by your personal computer was like that, then you would have noticed its performance worsening after every use due to the need to read the ever longer history of interaction with you.
Instead, CoL postulates that a computational problem is a game between two agents: a machine and its environment, symbolically named and , respectively. is a mechanical device only capable of following algorithmic strategies, while there are no similar assumptions about whose behavior can be arbitrary. Computational tasks in the traditional sense now become special cases of games with only two moves, where the first move (“input”) is by and the second move (“output”) by .
The following notational and terminological conventions are adopted. A move is any finite string over the standard keyboard alphabet. A labeled move is a move prefixed with or , with such a prefix (label) indicating which player is the author of the move. We will not always be very strict about differentiating between moves and labeled moves, sometimes saying “move” where, strictly speaking, “labeled move” is meant. A run is a (finite or infinite) sequence of labeled moves, and a position is a finite run. We usually use lowercase Greek letters as metavariables for moves, and uppercase Greek letters for runs. We will be writing runs and positions as , , , etc. The meanings of such expressions should be clear. For instance, is the run consisting of the (labeled) moves of the position , followed by the move , and then by the moves of the run .
A set of runs is said to be prefix-closed iff, whenever a run is in , so are all of its initial segments. The limit-closure of a set of runs is the result of adding to every infinite run such that all finite initial segments of are in .
Definition 2.1
A game is a pair , where:
-
is a nonempty, prefix-closed set of positions. We write for the limit-closure of .
is a mapping from to .
Intuitively, in the context of a given game , is the set of legal positions and is the set of legal runs. Note that, since is required to be nonempty and prefix-closed, the empty position , being an initial segment of all runs, is always legal. With here and elsewhere standing for either player and for its adversary , a legal move by in a position is a move such that . We say that a run is -legal iff either is legal, or else, where is the shortest illegal initial segment of , the last move of is -labeled. Intuitively, such a is a run where has not made any illegal moves unless its adversary has done so first. In all cases, we shall say “illegal” for “not legal” and “lost” for “not won”. For each legal run, tells us which of the two players has won the run. The following definition extends this meaning of the word “won” from legal runs to all runs by stipulating that an illegal run is always lost by the player that has made the first illegal move:
Definition 2.2
For a game , run and player , we say that is a -won (or won by ) run of iff is
-
either a legal run of with , or
-
a -illegal run of .
Games—at least when they are finite—can be visualized as trees in the style of Figure 1. Each complete or incomplete branch of such a tree represents a legal run, namely, the sequence of the labels of the edges of the branch. The nodes represent positions, where the label or of a node indicates which player is the winner if the play ends in the corresponding position.
\bot$$\top$$\alpha$$\bot$$\beta$$\bot$$\gamma$$\top$$\bot$$\beta$$\bot$$\gamma$$\top$$\top$$\alpha$$\bot$$\top$$\alpha$$\top$$\beta$$\top$$\gamma$$\top$$\bot$$\top$$\beta$$\top$$\gamma$$\top$$\bot$$\top$$\beta$$\top$$\gamma$$\top$$\top$$\alpha$$\bot$$\top$$\alpha$$\top$$\bot$$\top$$\bot$$\top$$\botFigure 1:A game
A distinguishing feature of CoL games is the absence of rules governing the order in which (legal) moves can or should be made. In some situations, such as in the root position of the game of Figure 1, both players may have legal moves, and which if any player moves first depends on which one wants or can act faster. Imagine a simultaneous play of chess on two boards, where you play white on both boards. At the beginning, only you have legal moves. But once you make an opening move—say, on board #1—the situation changes. Now both you and your environment have legal moves: the environment may respond on board #1, while you can make another opening move on board #2. It would be unnatural to impose rules determining the next player to move in this case, especially if your environment consists of two independent and non-communicating adversaries. The relaxed nature of our games makes them more direct and adequate tools for modeling real-life interactions like this and beyond than stricter games would be.
But how are such loose games played and, most importantly, what does an algorithmic winning strategy mean? Below is an example of such a strategy. It is left to the reader to convince himself or herself that following it guarantees a win in the game of Figure 1:
*Regardless of what the adversary is doing or has done, go ahead and make move ; make as your second move if and when you see that the adversary has made move , no matter whether this happened before or after your first move. *
Formally, ’s algorithmic strategies can be understood as what CoL, for historical reasons, calls HPMs (“hard-play machines”). An HPM is a Turing machine with the capability of making moves. This is just like the capability of generating an output, with the only difference that, while an ordinary Turing machine halts after generating an output, an HPM generally does not halt after making a move, so it can continue its work and make more moves later. Also, an HPM is equipped with an additional, read-only tape called the run tape, initially empty. Every time the HPM makes a move , the string is automatically appended to the content of this tape. At any time, any -labeled move may also be nondeterministically appended to the content of the run tape. This event is interpreted as that the environment has just made move . This way, at any step of the process, the run tape spells the current position of the play. It is hardly necessary to define HPMs in full detail here, for the Church-Turing thesis extends from ordinary Turing machines to HPMs, according to which HPMs adequately correspond to what we intuitively perceive as algorithmic strategies. So, rather than attempting to formally describe an HPM playing a given game, we can simply describe its work in relaxed, informal terms in the style of the earlier-displayed strategy for the game of Figure 1. There is also no need to anyhow define ’s strategies: all possible behaviors by are accounted for by the above-mentioned different nondeterministic updates of the run tape, including ’s relative speed because there are no restrictions on when or with what frequency the updates can take place.
Depending on what nondeterministic events (’s moves) occur in the course of the work of an HPM and when, different runs will be eventually (in the limit) spelled on ’s run tape. We call any such run a run generated by .
Definition 2.3
We say that an HPM computes a game iff every run generated by is -won run of . Such an is said to be a solution (or an algorithmic winning strategy for) .
By the depth of a game we mean the (possibly infinite) length of its longest legal run. Computational problems in the traditional sense, i.e. functions, are games of depth 2 of the kind seen in Figure 2. In such a game, the upper level edges represent possible inputs provided by the environment. This explains why their labels are -prefixed. The lower level edges represent possible outputs generated by the machine, so their labels are -prefixed. The root is -labeled because it corresponds to the situation where nothing happened, namely, no input was provided by the environment. The machine has nothing to answer for in this case, so it wins. The middle level nodes are -labeled because they correspond to situations where there was an input but the machine failed to generate an output, so the machine loses. Each group of the bottom level nodes has exactly one -labeled node, because a function has exactly one (correct) value at each argument.
Input\top$$\bot 0$$\bot 1$$\bot 2…Output\bot$$\top 0$$\top 1$$\top 2$$\top 3…\bot$$\top$$\bot$$\bot$$\bot$$\top 0$$\top 1$$\top 2$$\top 3…\bot$$\bot$$\top$$\bot$$\bot$$\top 0$$\top 1$$\top 2$$\top 3…\bot$$\bot$$\bot$$\topFigure 2:The successor function as a game
But why limit ourselves only to trees of the above sort? First of all, we may want to allow branches to be longer than , or even infinite to be able to model long or infinite tasks performed by computers. And why not allow any other sorts of arrangements of and in nodes or on edges? For instance, consider the task of computing the function . It would be natural to make the node to which the input [math] takes us not -labeled, but -labeled. For the function is not defined at [math], and the machine cannot be held responsible for failing to generate an output on such an input.
It makes sense to generalize computational problems not only in the direction of increasing their depths, but also decreasing. Games of depth [math], i.e., games that have no nonempty legal runs, are said to be elementary. There are exactly two elementary games, for which we use the same symbols as for the two players. Namely, is the elementary game with , and is the elementary game with . Intuitively, and are moveless games, with (the only legal run of) automatically won by the machine and won by the environment. While the game has no solution, the “do nothing” strategy is a solution of .
Extensionally, true propositions of classical logic such as “snow is white” are understood in CoL as the game , and false propositions such as “” as the game . Propositions are thus special—elementary—cases of our games. This allows us to say that games are generalized propositions.
3 Gameframes
This section is devoted to the basic concepts necessary for lifting CoL from the propositional level to the first-order level. What we call gameframes are generalized predicates in the same sense as games are generalized propositions.
We fix an infinite set of variables. As usual, lowercase letters near the end of the Latin alphabet will be used as metavariables for variables. We further fix the set of decimal numerals, and call its elements constants.
A universe (of discourse) is a pair , where , called the domain of , is a nonempty set, and , called the denotator of , is a total function of the type . Elements of will be referred to as individuals. The intuitive meaning of is that the individual is the denotat of the constant and thus is a name of .
A nice natural example of a universe is the arithmetical universe, whose domain is the set of natural numbers and whose denotator is the bijective function that sends each constant to the number it represents in standard decimal notation. Generally, however, the denotator is required to be neither injective nor surjective, meaning that some individuals may have multiple names, and some no names at all. For instance, in the informal universe of astronomy, most individuals—celestial bodies—have no names while some have several names (Morning Star = Evening Star = Venus). A natural example of a mathematical universe with an intrinsically non-surjective denotator would be one whose domain is the set of real numbers. Even if the set of constants was not fixed, the denotator here could not be surjective for the simple reason that, while there are uncountably many real numbers, there can only be countably many names. This is so because names, by their very nature and purpose, have to be finite objects.
Many properties of common interest, such as computability or decidability, are sensitive with respect to how objects (individuals) are named, as they deal with the names of those objects rather than the objects themselves. For instance, strictly speaking, computing a function means the ability to tell, after seeing a (the) name of an arbitrary individual , a (the) name of the individual with . Similarly, an algorithm deciding a predicate on a set , strictly speaking, takes as inputs not elements of —which may be abstract objects such as numbers or graphs—but rather names of those elements, such as decimal codes. It is not hard to come up with a nonstandard naming of the natural numbers via decimal numerals where the predicate “ is even” is undecidable. On the other hand, for any undecidable arithmetical predicate , one can come up with a naming such that becomes decidable—for instance, one that assigns even-length names to all satisfying and assigns odd-length names to all with . Classical logic exclusively deals with individuals of a universe without a need to also consider names for them, as it is not concerned with decidability or computability. CoL, on the other hand, with its computational semantics, inherently calls for being more careful about differentiating between individuals and their names, and hence for explicitly considering universes in the form rather than just as classical logic does.
For a set of variables and a domain , by a -valuation we mean a total function of the type . When is finite, such a valuation can be simply written as an -tuple of individuals, meaning that , where are the variables of listed lexicographically.
Definition 3.1
Let be a natural number. An -ary gameframe is a quadruple , where is a universe, is a set of distinct variables, and is a mapping that sends every -valuation to a game .
Given a gameframe , we refer to as the domain of , to as the denotator of , to as the universe of , to the elements of as the variables on which depends (or simply the variables of ), and to as the extension of . For a gameframe we customarily use the same name as for its extension. This never causes ambiguity, as it is usually clear from the context whether refers to the gameframe itself or just its extension. In informal contexts where a universe is either fixed or irrelevant, we think of games as special—nullary—cases of gameframes. Namely, a nullary gameframe will be understood as the game , usually simply written as .
In classical logic, under an intensional (variable-sensitive) understanding, the definition of the concept of an -ary predicate would look exactly like our definition of an -ary gameframe after omitting the redundant denotator component, with the only difference that there the extension function would return propositions rather than games. And, just like propositions are nothing but [math]-ary predicates, games are nothing but [math]-ary gameframes. Thus, gameframes generalize games in the same way as predicates generalize propositions.
In formal contexts, we choose a similar intensional approach to functions. The definition of a function given below is literally the same as our definition of a gameframe, with the only difference that the extension component now maps valuations to individuals rather than games.
Definition 3.2
Let be a natural number. An -ary function is a tuple , where is a universe, is a set of distinct variables, and is a mapping that sends every -valuation to an element of .
Just as in the case of gameframes, we customarily use the same name for a function as for its last component. We refer to the elements of as the variables on which the function depends, refer to as the domain of , etc.
Given a gameframe , a set of variables with and an -valuation , we write to mean the game , where is the restriction of to (i.e., the -valuation that agrees with on all variables from ). Such a game is said to be an instance of , and the operation that generates from and is said to be the instantiation operation. For readability, we usually write , and instead of , and . Similarly, given a function , a set of variables with and an -valuation , we write to denote the individual to which maps , where is the restriction of to .
We say that a gameframe is elementary iff so are all of its instances. Thus, gameframes generalize elementary gameframes in the same sense as games generalize elementary games. In turn, elementary gameframes generalize elementary games in the same sense as predicates generalize propositions in classical logic. So, just as we identify elementary games with propositions, we will identify elementary gameframes with predicates. Specifically, in the context of a given universe , we understand a predicate on as the elementary gameframe , where is the set of variables on which depends, and is such that, for any -valuation , iff is true at . And vice versa: an elementary gameframe will be understood as the predicate that depends on the same variables as does and is true at a given valuation iff .
Convention 3.3
Assume is a universe, , , and . We shall write to mean the nullary (constant) function such that . We shall write to mean the nullary function such that . And we shall write to mean the unary function such that, for any , .
Convention 3.4
Assume is a function (resp. gameframe). Following the standard readability-improving practice established in the literature for functions and predicates, we may fix a tuple of pairwise distinct variables for when first mentioning it, and write as . When doing so, we do not necessarily mean that . Representing as sets a context in which, for whatever functions , we can write to mean the function (resp. gameframe) such that:
- •
.
- •
For any -valuation , , where is the -valuation such that and agrees with on all other variables from .
Further, we allow for any of the above to be (written as) just an individual , just a constant or just a variable . In such cases, should be correspondingly understood as the function , or , where . So, for instance, is our lazy way to write .
4 The operator zoo of computability logic
Logical operators in CoL stand for operations on gameframes. With games seen as nullary gameframes, such operations are automatically also operations on games. There is an open-ended pool of operations of potential interest, and which of those to study may depend on particular needs and taste. Below is an incomplete list of the operations that have been officially introduced so far.
- •
Negation: .
- •
Conjunctions: (parallel); (choice); (sequential); (toggling).
- •
Disjunctions: (parallel); (choice); (sequential); (toggling).
- •
Implications: (parallel); (choice); (sequential); (toggling).
- •
Universal quantifiers: (blind); (parallel); (choice); (sequential); (toggling).
- •
Existential quantifiers: (blind); (parallel); (choice); (sequential); (toggling).
- •
Recurrences: \circ$$\mid (branching); \wedge$$\mid (parallel); -$$\wedge$$\mid (sequential); \wedge$$\mid (toggling).
- •
Corecurrences: \circ$$\mid (branching); \vee$$\mid (parallel); -$$\vee$$\mid (sequential); \vee$$\mid (toggling).
- •
Rimplications: – (branching); – (parallel); – (sequential); – (toggling).
- •
Repudiations: (branching); >$$\neg (parallel); \triangleright$$\neg (sequential); - (toggling).
Among the symbolic names for the above operations we see all operators of classical logic, and our choice of the classical notation for them is no accident: classical first-order logic is nothing but the result of discarding all other operators in CoL and forbidding all but elementary gameframes. Indeed, after analyzing the relevant definitions, each of the classically-shaped operators, when restricted to elementary gameframes, can be easily seen to be virtually the same as the corresponding operator of classical logic. For instance, if and are elementary games or gameframes, then so is , and the latter is exactly the classical conjunction of and understood as propositions or predicates. In the nonelementary case, however, the logical behavior of , , , becomes more reminiscent of—yet not the same as—that of the corresponding operators of multiplicative linear logic.
This section contains formal definitions of all of the above-listed operations. We agree that, throughout those definitions, ranges over positions, over runs and over -valuations, where is the domain of the gameframe that is being defined and is the set of variables on which that gameframe depends. All such metavariables should be considered universally quantified in the corresponding clause(s) of the definition unless otherwise implied by the context. Each definition has two clauses, one defining and the other . The second clause, telling us who wins a given run of , always implicitly assumes that such a run is in .
This section also contains many examples and informal explanations. For clarity let us agree that in all such cases, unless otherwise implied by the context, we have the arithmetical universe (cf. Section 3) in mind. This is so even if we talk about seemingly non-number individuals such as people, Turing machines, etc. The latter should simply be understood as the natural numbers that encode the corresponding objects in some fixed encoding, and the (non-numeral) names of such objects understood as the corresponding decimal numerals. Fixing the universe allows us to understand games as nullary gameframes as explained in Section 3. The informal discussions found in this section sometimes use the word “valid”, which, intuitively, should be understood as “always computable”. The precise meaning(s) of this concept will only be defined later in Section 6. When describing machine’s winning strategies, we usually assume implicitly that the environment never makes illegal moves, for, if it does, the machine automatically wins regardless of what happens afterwards.
From our formal definitions of propositional (non-quantifier) operations it can be seen immediately that instantiation commutes with all such operations: , , etc. So, in order to understand the meanings of the propositional operations, it would be sufficient to just understand how they modify nullary gameframes. For this reason, in the corresponding informal explanations we always implicitly assume that the gameframes that we talk about are nullary, and call them simply “games”. For similar reasons, when informally explaining the meaning of where is one of our quantifiers, it will be implicitly assumed that is a unary gameframe that only depends on and (hence) is nullary.
When omitting parentheses in compound expressions, we assume that all unary operators (negation, repudiations, recurrences, corecurrences and quantifiers) take precedence over all binary operators (conjunctions, disjunctions, implications, rimplications), among which implications and rimplications have the lowest precedence. So, for instance, should be understood as A\rightarrow\bigl{(}(\neg B)\vee C\bigr{)}.
4.1 Prefixation and negation
Unlike the operations listed in the preceding outline, the operation of prefixation is not meant here to act as a logical operator in the formal language of CoL. Yet, it is very useful in characterizing and analyzing games, and we want to start our tour of the zoo with it.
Definition 4.1
Assume is a gameframe and is a legal position of every instance of (otherwise the operation is undefined). The -prefixation of , denoted , is defined as the gameframe such that:
- •
;
- •
.
Intuitively, is a game playing which means playing starting (continuing) from position . That is, is the game to which evolves (is brought down) after the moves of have been made. Visualized as a tree, is nothing but the subtree of rooted at the node corresponding to position .
To define the negation operation , read as “not ”, let us agree that, for a run , means the result of changing the label to and vice versa in each move of .
Definition 4.2
Assume is a gameframe. is defined as the gameframe such that:
- •
;
- •
iff .
Intuitively, is with the roles of the two players interchanged: ’s (legal) moves and wins become ’s moves and wins, and vice versa. Let Chess, here and later, be the game of chess from the point of view of White, with draws ruled out (say, by declaring them to be wins for Black). Then is the same game but as seen by Black.
Obviously the double negation principle holds: interchanging the players’ roles twice restores the original roles of the players. It is also easy to see that we always have . So, for instance, if is ’s legal move in the empty position of that brings down to , then the same is ’s legal move in the empty position of , and it brings down to .
4.2 Choice operations
This group of operations consists of (choice conjunction, read as “chand ”), (choice disjunction, read as “chor ”), (choice implication, read as “chimplication ”), (choice universal quantifier, read as “chall ”) and (choice existential quantifier, read as “chexists ”).
is a game where, in the initial (empty) position, only the environment has legal moves. Such a move should be either “[math]” or “”. If the environment moves [math], the game continues as , meaning that ; if it moves , then the game continues as , meaning that; and if it fails to make either move (“choice”), then it loses. is similar, with the difference that here it is the machine who has initial moves and who loses if no such move is made. Formally, we have:
Definition 4.3
Assume and are gameframes.
(a)
is defined as the gameframe such that:
- •
.
- •
; .
(b)
is defined as the gameframe such that:
- •
.
- •
; .
(c)
.
The symbol is seldom used in this chapter: instead of , we often prefer to write the intuitively more transparent .
Note the perfect symmetry between the first two clauses of the above definition: clause (b) is nothing but clause (a) with and interchanged everywhere, and vice versa. Such symmetry is called duality:
Terminology 4.4
We say that a concept is dual to a concept iff the definition of can be obtained from the definition of by interchanging and . For instance, (or ) is dual to (or ), and vice versa.
It is not hard to see that, due to duality, the De Morgan laws go through for : we always have and . Together with the earlier observed double negation principle, this means that and . Similarly for the quantifier counterparts and of and . And similarly for all other sorts of conjunctions, disjunctions, recurrences, corecurrences and quantifiers defined in this section.
\hskip 1.0pt\mbox{\Large\sqcap}xA(x) can be understood as the infinite conjunction , and \hskip 1.0pt\mbox{\Large\sqcup}xA(x) as the infinite disjunction . Specifically, \hskip 1.0pt\mbox{\Large\sqcap}xA(x) is a game where, in the initial position, only the environment has legal moves, and such a move should be one of the constants. If the environment moves , then the game continues as , and if the environment fails to make an initial move/choice, then it loses. \hskip 1.0pt\mbox{\Large\sqcup}xA(x) is similar, with the difference that here it is the machine who has initial moves and who loses if no such move is made. So, we always have \langle\bot c\rangle\hskip 1.0pt\mbox{\Large\sqcap}xA(x)=A(c) and \langle\top c\rangle\hskip 1.0pt\mbox{\Large\sqcup}xA(x)=A(c). Below is a formal definition of the choice quantifiers:
Definition 4.5
Assume is a gameframe.
(a)
\hskip 1.0pt\mbox{\Large\sqcap}xA(x) is defined as the gameframe such that:
- •
.
- •
; .
(b)
\hskip 1.0pt\mbox{\Large\sqcup}xA(x) is dual to \hskip 1.0pt\mbox{\Large\sqcap}xA(x).
With choice operators we can easily express the most common sorts of computational problems, such as the problem of computing a function or the problem of deciding a predicate . The former can be written as \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=f(x)\bigr{)}, and the latter as \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\sqsupset p(x)\bigr{)}. That is, is computable in the standard sense iff \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=f(x)\bigr{)} is computable in our sense, and is decidable in the standard sense iff \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\sqsupset p(x)\bigr{)} is computable in our sense. So, the game of Figure 2 is nothing but \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x+1). Every run of this game can be seen as a short dialogue between the machine and its environment. The first move—say, —is by , and intuitively it amounts to asking “what is the successor of ?”. It brings the game down to \hskip 1.0pt\mbox{\Large\sqcup}y(y=2+1). In order win, has to make the move , amounting to saying that is the successor of . Any other move, or no move at all, would be a loss for .
Classical logic has been repeatedly criticized for its operators not being constructive. Consider, for example, \mbox{\large\forall}x\mbox{\large\exists}y\bigl{(}y=f(x)\bigr{)}. It is always true in the classical sense (as long as is a total function). Yet its truth has no practical import, for “\mbox{\large\exists}y” merely signifies existence of , without implying that such a can actually be found. And, indeed, if is an incomputable function, there is no method for finding . On the other hand, the choice operations of CoL are constructive. Computability (“truth”) of \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=f(x)\bigr{)} means more than just existence of ; it means the possibility to actually find (compute, construct) the corresponding for every .
Similarly, let be the predicate “Turing machine halts on input ”. Consider the statement \mbox{\large\forall}x\mbox{\large\forall}y\bigl{(}\neg\mbox{\em Halts}(x,y)\vee\mbox{\em Halts}(x,y)\bigr{)}. It is true in classical logic, yet not in a constructive sense. Its truth means that, for all and , either or is true, but it does not imply existence of an actual way to tell which of these two is true after all. And such a way does not really exist, as the halting problem is undecidable. This means that \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y(\neg\mbox{\em Halts}(x,y)\sqcup\mbox{\em Halts}(x,y)\bigr{)} is not computable. Generally, the law of excluded middle , validated by classical logic and causing the indignation of the constructivistically-minded, is not valid in computability logic with OR understood as choice disjunction. The following is an example of a game of the form with no algorithmic solution (why, by the way?):
[TABLE]
4.3 Parallel operations
This group of operations consists of (parallel conjunction, read as “pand ”), (parallel disjunction, read as “por ”), (parallel implication, read as “pimplication ”), (parallel universal quantifier, read as “pall ”), (parallel existential quantifier, read as “pexists ”), \wedge$$\mid (parallel recurrence, read as “precurrence ”), \vee$$\mid (parallel corecurrence, read as “coprecurrence ”), – (parallel rimplication, read as “primplication ”) and >$$\neg (parallel repudiation, read as “prepudiation ”).
and are games playing which means playing the two games simultaneously. In order to win in (resp. ), needs to win in both (resp. at least one) of the components . For instance, is a two-board game, where plays black on the left board and white on the right board, and where it needs to win in at least one of the two parallel sessions of chess. A win can be easily achieved here by just mimicking in Chess the moves that the adversary is making in , and vice versa. This copycat strategy guarantees that the positions on the two boards always remain symmetric (“synchronized”), and thus eventually loses on one board but wins on the other. This is very different from . In the latter needs to choose between the two components and then win the chosen one-board game, which makes essentially as hard to win as either or Chess. A game of the form is generally easier (at least, not harder) to win than , the latter is easier to win than , and the latter in turn is easier to win than .
Technically, a move in the left (resp. right) -conjunct or -disjunct is made by prefixing with “” (resp. “”). For instance, in the initial position of , the move “” is legal for , meaning choosing the left -conjunct in the right -disjunct of the game. If such a move is made, the game continues as . The player , too, has initial legal moves in , which are “” and “”.
The rest of this chapter will rely on the following important notational convention:
Notation 4.6
For a run and string , means the result of removing from all moves except those of the form , and then deleting the prefix “” in the remaining moves. For instance, .
Definition 4.7
Assume and are gameframes.
(a)
is defined as the gameframe such that:
- •
iff every move of has the prefix “” or “” and, for both , .
- •
iff, for both , .
(b)
is dual to .
(c)
.
Example 4.8
is a legal run of the game A=\hskip 1.0pt\mbox{\Large\sqcup}x\hskip 1.0pt\mbox{\Large\sqcap}y(y\not=x^{2})\vee\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{2}). It induces the following what we call evolution sequence, showing how things evolve as runs, i.e., how the moves of affect/modify the game that is being played:
[TABLE]
The run hits the true proposition , and hence is won by the machine.
As one may guess, \hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxA(x) is nothing but , and \mbox{{\Large\vee}}xA(x) is nothing but . Formally these two quantifiers are defined as follows:
Definition 4.9
Assume is a gameframe.
(a)
\hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxA(x) is defined as the gameframe such that:
- •
iff every move of has the prefix “” for some and, for all such , .
- •
iff, for all , .
(b)
\mbox{{\Large\vee}}xA(x) is dual to \hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxA(x).
The next group of parallel operators are \wedge$$\mid and its dual \vee$$\mid . Intuitively, playing \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptA means simultaneously playing in infinitely many “copies” of , and is the winner iff it wins in all copies. \hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0ptA is similar, with the only difference that here winning in just one copy is sufficient. So, \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptA is nothing but the infinite parallel conjunction , and \hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0ptA is . Equivalently, \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptA and \hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0ptA can be respectively understood as \hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxA and \mbox{{\Large\vee}}xA, where is a dummy variable on which does not depend. The following definition formalizes these intuitions:
Definition 4.10
Assume is a gameframe.
(a)
\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptA is defined as the gameframe such that:
- •
iff every move of has the prefix “” for some and, for all such , .
- •
iff, for all , .
(b)
\hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0ptA is dual to \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptA.
The prefix “r” in the qualification “rimplication” stands for “recurrence”. Generally, a rimplication of one or another sort is a weak (recurrence-based) implication, and a repudiation is a weak negation. The parallel versions – and >$$\neg of such operations are defined as follows.
Definition 4.11
(a) A\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0ptB\ =_{def}\ \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptA\rightarrow B. (b) \mbox{\raisebox{1.1pt}{\tiny>}{\scriptsize\neg}}A\ =_{def}\ \hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0pt\neg A.
Just like negation and unlike choice operations, parallel operations preserve the elementary property of games. When restricted to elementary games, the meanings of , and coincide with those of classical conjunction, disjunction and implication. Further, as long as all individuals of the universe have naming constants, the meanings of and coincide with those of classical universal quantifier and existential quantifier. The same conservation of classical meaning (but without any conditions on the universe) is going to be the case with the blind quantifiers \mbox{\large\forall},\mbox{\large\exists} defined later; so, at the elementary level, when all individuals of the universe have naming constants, and are indistinguishable from and and , respectively. As for the parallel recurrence and corecurrence, for an elementary we simply have A=\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptA=\hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0ptA.
While all classical tautologies automatically remain valid when parallel operators are applied to elementary games, in the general case the class of valid (in the strict sense of either sort of validity defined in Section 6) principles shrinks. For example, , i.e. , is not valid. Back to our chess example, one can see that the earlier copycat strategy successful for would be inapplicable to . The best that can do in this three-board game is to synchronize with one of the two conjuncts of . It is possible that then and the unmatched Chess are both lost, in which case the whole game will be lost as well.
The principle is valid in classical logic because the latter sees no difference between and . On the other hand, in virtue of its semantics, CoL is resource-conscious, and in it is by no means the same as or . Unlike , P\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0ptP\wedge P is a valid principle. Here, in the antecedent, we have infinitely many “copies” of . Pick any two copies and, via copycat, synchronize them with the two conjuncts of the consequent. A win is guaranteed. The principle can also be seen to be valid.
This talk about resource-consciousness immediately reminds us of linear logic [10]. The latter, for instance, also rejects while accepting both and \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptP\rightarrow P\wedge P with understood as multiplicatives, as additives and \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt,\hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0pt as exponentials. Together with similarities, there are also considerable discrepancies though. The class of principles provable in linear logic or even its extension known as affine logic forms a proper subclass of the principles validated by the semantics of CoL. An example of a purely multiplicative formula separating the two classes is Blass’s [6] principle
[TABLE]
Other examples include \hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0pt\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptP\rightarrow\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt\hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0ptP. On the other hand, it is believed (but never has been officially proven) that the class of CoL’s valid principles in the signature \{\neg,\wedge,\vee,\sqcap,\sqcup,\hskip 1.0pt\mbox{\Large\sqcap},\hskip 1.0pt\mbox{\Large\sqcup}\} is indistinguishable from the class of principles validated by Blass’s [6] game semantics. This, however, stops being the case if \wedge$$\mid —or any later-defined sort of recurrence for that matter—is added to the signature as a purported counterpart of Blass’s repetition operator. For instance, \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt(P\sqcup Q)\rightarrow\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptP\sqcup\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptQ is valid in Blass’s sense but it is not a valid principle of CoL; on the other hand, CoL validates P\wedge\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt(P\rightarrow Q\wedge P)\rightarrow\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptP (cf. [33]) which is not valid in Blass’s sense.
4.4 Reduction
The operator deserves a separate subsection. The intuition associated with is that this is the problem of reducing to : solving means solving while having as a computational resource. Specifically, may observe how is being solved by its adversary, and utilize this information in its own solving . Resources are symmetric to problems: what is a problem to solve for one player is a resource that the other player can use, and vice versa. Since is negated in and negation means switching the players’ roles, (as opposed to ) comes as a resource rather than problem to in . Our copycat strategy for was an example of reducing Chess to Chess. The same strategy was underlying Example 4.8, where \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{2}) was reduced to itself.
Let us look at a more meaningful example: reducing the acceptance problem to the halting problem. The former, as a decision problem, will be written as \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\bigl{(}\neg\mbox{\em Accepts}(x,y)\sqcup\mbox{\em Accepts}(x,y)\bigr{)}, where is the predicate “Turing machine accepts input ”. Similarly, as we already agreed, the halting problem is written as \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\bigl{(}\neg\mbox{\em Halts}(x,y)\sqcup\mbox{\em Halts}(x,y)\bigr{)}. Neither problem has an algorithmic solution, yet the following implication does:
[TABLE]
Here is ’s winning strategy for (1). Wait till makes the moves and for some and . Making these moves essentially means asking the question “Does machine accept input ?”. If such moves are never made, you (the machine) win. Otherwise, the moves bring the game down to
[TABLE]
Make the moves and , thus asking the counterquestion “Does machine halt on input ?”. Your moves further bring the game down to
[TABLE]
will have to answer this counterquestion, or else it loses (why?). If it answers by (“No, does not halt on ”), you make the move (say “ does not accept ”). The game will be brought down to . You win, because this is a true proposition: if does not halt on , then it does not accept , either. Otherwise, if answers by (“Yes, halts on ”), start simulating on until halts. If you see that accepted , make the move (say “ accepts ”); otherwise make the move (say “ does not accept ”). Of course, it is a possibility that this simulation goes on forever. But then has lied when saying “ halts on ”; in other words, the antecedent is false, and you win regardless of what happens in the consequent. Note that what the machine did when following this strategy was indeed reducing the acceptance problem to the halting problem: it solved the former using an external (environment-provided) solution of the latter.
There are many natural concepts of reduction, and a strong case can be made that pimplicative reduction, i.e. the reduction captured by , is the most basic one. For this reason we agree that, if we simply say “reduction”, it always means pimplicative reduction. A great variety of other reasonable concepts of reduction is expressible in terms of . Among those is Turing reduction. Remember that a predicate is said to be Turing reducible to a predicate if can be decided by a Turing machine equipped with an oracle for . For a positive integer , -bounded Turing reducibility is defined the same way, with the only difference that here the oracle is allowed to be used only times. It turns out that – is a conservative generalization of Turing reduction. Namely, when and are elementary games (i.e. predicates), is Turing reducible to if and only if the problem \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg p(x)\sqcup p(x)\bigr{)}\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0pt\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg q(x)\sqcup q(x)\bigr{)} has an algorithmic solution. If here we change – back to , we get the same result for 1-bounded Turing reducibility. More generally, as one might guess, -bounded Turing reduction will be captured by
[TABLE]
If, instead, we write
[TABLE]
then we get what is called -bounded weak truth-table reduction. The latter differs from -bounded Turing reduction in that here all oracle queries should be made at once, before seeing responses to any of those queries. What is called mapping (or many-one) reducibility of to is nothing but computability of \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}q(x)\leftrightarrow p(y)\bigr{)}, where abbreviates . One could go on and on with this list.
And yet many other natural concepts of reduction expressible in the language of CoL may have no established names in the literature. For example, from the previous discussion it can be seen that a certain reducibility-style relation holds between the predicates and in an even stronger sense than computability of (1). In fact, not only (1) has an algorithmic solution, but also the generally harder-to-solve problem
[TABLE]
Among the merits of CoL is that it offers a formalism and deductive machinery for systematically expressing and studying computation-theoretic relations such as reducibility, decidability, enumerability, etc., and all kinds of variations of such concepts.
Back to reducibility, while the standard approaches only allow us to talk about (a whatever sort of) reducibility as a relation between problems, in our approach reduction becomes an operation on problems, with reducibility as a relation simply meaning computability of the corresponding combination of games, such as for pimplicative reducibility. Similarly for other relations or properties such as the property of decidability. The latter becomes the operation of deciding if we define the problem of deciding a predicate as the game \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg p(x)\sqcup p(x)\bigr{)}. So, now we can meaningfully ask questions such as “Is the reduction of the problem of deciding to the problem of deciding always reducible to the mapping reduction of to ? ”. This question would be equivalent to whether the following formula is valid in CoL:
[TABLE]
The answer turns out to be “Yes”, meaning that mapping reduction is at least as strong as pimplicative reduction. Here is a strategy that wins this game no matter what particular predicates and are. At first, wait till, for some , the environment brings the game down to
[TABLE]
Respond by bringing the game down to
[TABLE]
Wait again till, for some , the environment further brings the above game down to
[TABLE]
Bring this game down to \bigl{(}q(m)\leftrightarrow p(n)\bigr{)}\rightarrow\bigl{(}\neg p(n)\sqcup p(n)\rightarrow\neg q(m)\sqcup q(m)\bigr{)}, after which wait till the environment further brings the game down to either \bigl{(}q(m)\leftrightarrow p(n)\bigr{)}\rightarrow\bigl{(}\neg p(n)\rightarrow\neg q(m)\sqcup q(m)\bigr{)} or \bigl{(}q(m)\leftrightarrow p(n)\bigr{)}\rightarrow\bigl{(}p(n)\rightarrow\neg q(m)\sqcup q(m)\bigr{)}. In the former case, bring the game down to \bigl{(}q(m)\leftrightarrow p(n)\bigr{)}\rightarrow\bigl{(}\neg p(n)\rightarrow\neg q(m)\bigr{)}, and you have won; in the latter case, bring the game down to \bigl{(}q(m)\leftrightarrow p(n)\bigr{)}\rightarrow\bigl{(}p(n)\rightarrow q(m)\bigr{)}, and you have won, again.
One could also ask: “Is the mapping reduction of to always reducible to the reduction of the problem of deciding to the problem of deciding ? ”. This question would be equivalent to whether the following formula is valid:
[TABLE]
The answer here turns out to be “No”, meaning that mapping reduction is properly stronger than pimplicative reduction. This negative answer can be obtained by showing that the above formula is not provable in one of the sound and complete deductive systems for CoL whose language allows to write (3), such as system CL12 found later in Section 7.3. Similarly, had our ad hoc attempt to come up with a strategy for (2) failed, its validity could have been easily established by finding a proof of it in such a system.
To summarize, CoL offers not only a convenient language for specifying computational problems and relations or operations on them, but also a systematic tool for asking and answering questions in the above style and beyond.
4.5 Blind operations
This group only includes (blind universal quantifier, read as “blall ”) and (blind existential quantifier, read as “blexists ”), with no propositional counterparts. Our definition of \mbox{\large\forall}xA(x) and \mbox{\large\exists}xA(x) below assumes that the gameframe is “unistructural” in . Intuitively, unistructurality in means that the Lp component of the gameframe does not depend on the (value of the) variable . Formally, we say that a gameframe is unistructural in iff, for any -valuation and any , we have . All nullary or elementary gameframes are unistructural in (whatever variable) . And all operations of CoL are known to preserve this property.
Definition 4.12
Assume is a gameframe unistructural in .
(a)
\mbox{\large\forall}xA(x) is defined as the gameframe such that:
- •
.
- •
iff, for all , .
(b)
\mbox{\large\exists}xA(x) is dual to \mbox{\large\forall}xA(x).
Intuitively, playing \mbox{\large\forall}xA(x) or \mbox{\large\exists}xA(x) means playing “blindly”, without knowing the value of . In \mbox{\large\forall}xA(x), the machine wins iff the play it generates is successful for every possible value of from the domain, while in \mbox{\large\exists}xA(x) being successful for just one value is sufficient. When applied to elementary games, the blind quantifiers act exactly like the corresponding quantifiers of classical logic.
Unlike \hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxA(x) which is a game on infinitely many boards, both \mbox{\large\forall}xA(x) and \hskip 1.0pt\mbox{\Large\sqcap}xA(x) are one-board games. Yet, they are very different from each other. To see this difference, compare the problems \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\mbox{\em Even}(x)\sqcup\mbox{\em Odd}(x)\bigr{)} and \mbox{\large\forall}x\bigl{(}\mbox{\em Even}(x)\sqcup\mbox{\em Odd}(x)\bigr{)}. The former is an easily winnable game of depth 2: the environment selects a number, and the machine tells whether that number is even or odd. The latter, on the other hand, is a game which is impossible to win. This is a game of depth 1, where the value of is not specified by either player, and only the machine moves—tells whether (the unknown) is even or odd. Whatever the machine says, it loses, because there is always a value for that makes the answer wrong.
This should not suggest that nontrivial -games can never be won. For instance, the problem
[TABLE]
has an easy solution. The idea of a winning strategy here is that, for any given , in order to tell the parity of , it is not really necessary to know the value of . Rather, just knowing the parity of is sufficient. And such knowledge can be obtained from the antecedent. In other words, for any known and unknown , the problem of telling whether is even or odd is reducible to the problem of telling whether is even or odd. Specifically, if both and are even or both are odd, then is even; otherwise is odd. Below is the evolution sequence (cf. Exercise 4.8) induced by the run where the machine has used such a strategy.
[TABLE]
The machine won because the play hit the true \mbox{\large\forall}x\bigl{(}\mbox{\em Even}(x)\rightarrow\mbox{\em Odd}(x+7)\bigr{)}. Notice how \mbox{\large\forall}x persisted throughout the sequence. Generally, the (\mbox{\large\forall},\mbox{\large\exists})-structure of a game will remain unchanged in such sequences. The same is the case with parallel operations such as in the present case.
To help us appreciate the contrast between the logical behaviors of , and , the following list shows some valid () and invalid () principles of CoL, where validity (“always computability”) can be understood in either sense defined later in Section 6.
-
\mbox{\vdash\vdash}\ \mbox{\large\forall}xP(x)\rightarrow\hskip 1.0pt\mbox{\Large\sqcap}xP(x)
-
\mbox{\vdash\not\vdash}\ \hskip 1.0pt\mbox{\Large\sqcap}xP(x)\rightarrow\mbox{\large\forall}xP(x)
-
\mbox{\vdash\not\vdash}\ \mbox{\large\forall}xP(x)\rightarrow\hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxP(x)
-
\mbox{\vdash\not\vdash}\ \hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxP(x)\rightarrow\mbox{\large\forall}xP(x)
-
\mbox{\vdash\vdash}\ \hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxP(x)\rightarrow\hskip 1.0pt\mbox{\Large\sqcap}xP(x)
-
\mbox{\vdash\not\vdash}\ \hskip 1.0pt\mbox{\Large\sqcap}xP(x)\rightarrow\hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxP(x)
-
\mbox{\vdash\vdash}\ \mathbb{Q}xP(x)\wedge\mathbb{Q}xR(x)\rightarrow\mathbb{Q}x\bigl{(}P(x)\wedge R(x)\bigr{)} for all three \mathbb{Q}\in\{\mbox{\large\forall},\hskip 1.0pt\mbox{\Large\sqcap},\hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0pt\}
-
\mbox{\vdash\vdash}\ \mbox{\large\forall}x\bigl{(}P(x)\wedge R(x)\bigr{)}\rightarrow\mbox{\large\forall}xP(x)\wedge\mbox{\large\forall}xR(x)
-
\mbox{\vdash\not\vdash}\ \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}P(x)\wedge R(x)\bigr{)}\rightarrow\hskip 1.0pt\mbox{\Large\sqcap}xP(x)\wedge\hskip 1.0pt\mbox{\Large\sqcap}xR(x)
-
\mbox{\vdash\vdash}\ \hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptx\bigl{(}P(x)\wedge R(x)\bigr{)}\rightarrow\hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxP(x)\wedge\hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptxR(x)
4.6 Branching operations
This group consists of \circ$$\mid (branching recurrence, read as “brecurrence ”), \circ$$\mid (branching corecurrence, read as “cobrecurrence ”), – (branching rimplication, read as “brimplication ”) and (branching repudiation, read as “brepudiation ”). Let us talk about \circ$$\mid first, as all other branching operations are definable in terms of it.
What is common for the members of the family of game operations called recurrences is that, when applied to a game , they turn it into a game playing which means repeatedly playing . In terms of resources, recurrence operations generate multiple “copies” of , thus making a reusable/recyclable resource. In classical logic, recurrence-style operations would be meaningless, because classical logic is resource-blind and thus sees no difference between one and multiple copies of . In the resource-conscious CoL, however, recurrence operations are not only meaningful, but also necessary to achieve a satisfactory level of expressiveness and realize its potential and ambitions. Hardly any computer program is used only once; rather, it is run over and over again. Loops within such programs also assume multiple repetitions of the same subroutine. In general, the tasks performed in real life by computers, robots or humans are typically recurring ones or involve recurring subtasks.
There is more than one naturally emerging recurrence operation. The differences between various recurrence operations are related to how “repetition” or “reusage” is exactly understood. Imagine a computer with a chess-playing program. The resource that such a computer provides is obviously something stronger than just our old friend Chess (as long as it always wins), for it permits to play Chess as many times as the user wishes, while Chess, as such, only assumes one play. The simplest operating system would allow to start a session of Chess, then—after finishing or abandoning and destroying it—start a new play again, and so on. The game that such a system plays—i.e. the resource that it supports/provides—is -$$\wedge$$\mid Chess, which assumes an unbounded number of plays of Chess in a sequential fashion. A formal definition of the operation -$$\wedge$$\mid , called sequential recurrence, will be given later is Section 4.7.
A more advanced operating system, however, would not require to destroy the old sessions before starting new ones; rather, it would allow to run as many parallel sessions as the user wants. This is what is captured by \wedge$$\mid Chess, meaning nothing but the infinite parallel conjunction . As we remember from Section 4.3, \wedge$$\mid is called parallel recurrence.
Yet a really good operating system would not only allow the user to start new sessions of Chess without destroying old ones; it would also make it possible to branch/replicate any particular stage of any particular session, i.e., create any number of “copies” of any already reached position of the multiple parallel plays of Chess, thus giving the user the possibility to try different continuations from the same position. What corresponds to this intuition is the branching recurrence \circ$$\mid Chess of Chess.
At the intuitive level, the difference between \circ$$\mid and \wedge$$\mid is that in \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptA, unlike \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptA, the environment does not have to restart from the very beginning every time it wants to reuse it (as a resource); rather, it is allowed to backtrack to any of the previous—not necessarily starting—positions and try a new continuation from there, thus depriving the adversary of the possibility to reconsider the moves it has already made in that position. This is in fact the type of reusage every purely software resource allows or would allow in the presence of an advanced operating system and unlimited memory: one can start running a process (task, game); then fork it at any stage thus creating two threads that have a common past but possibly diverging futures (with the possibility to treat one of the threads as a “backup copy” and preserve it for backtracking purposes); then further fork any of the branches at any time; and so on.
The less flexible type of reusage of assumed by \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptA, on the other hand, is closer to what infinitely many autonomous physical resources would naturally offer, such as an unlimited number of independently acting robots each performing task , or an unlimited number of computers with limited memories, each one only capable of and responsible for running a single thread of process . Here the effect of forking an advanced stage of cannot be achieved unless, by good luck, there are two identical copies of the stage, meaning that the corresponding two robots or computers have so far acted in precisely the same ways.
In early papers [14, 26] on CoL, the formal definitions of \circ$$\mid and its dual \circ$$\mid were direct formalizations of the above intuitions, with an explicit presence of “replicative” moves used by players to fork a given thread of and create two threads out of one. Later, in [32], another definition was found which was proven to be equivalent to the old one in the sense of mutual reducibility of the old and the new versions of \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptA. The new definition less directly corresponds to the above intuitions, but is technically simpler, and we choose it as our “canonical” definition of branching (co)recurrence. To be able to state it, we agree on the following:
Notation 4.13
Where is a run and is a bitstring (finite or infinite sequence of [math]s and s), means the result of deleting from all moves except those that look like for some initial segment of , and then further deleting the prefix “” from such moves. E.g., .
Definition 4.14
Assume is a gameframe.
(a)
\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptA is defined as the gameframe such that:
- •
iff every move of has the prefix “” for some finite bitstring and, for every infinite bitstring , ;
- •
iff, for every infinite bitstring , .
(b)
\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptA is dual to \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptA.
The direct intuitions underlying this definition are as follows. To play \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptA or \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptA means to simultaneously play in multiple parallel copies/threads of . Each infinite bitstring denotes one such thread (so, there are in fact uncountably many threads, even if some of them coincide). Every legal move by either player looks like for some finite bitstring , and the effect/meaning of such a move is simultaneously making the move in all threads such that is an initial segment of . So, where is the overall run of \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptA or \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptA, the run in a given thread of is . In order to win \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptA, the machine needs to win in all threads, while for winning \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptA it is sufficient to win in just one thread.
\circ$$\mid can be shown to be stronger than its parallel counterpart \wedge$$\mid , in the sense that the principle \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptP\rightarrow\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptP is valid while \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptP\rightarrow\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptP is not. The two operators, in isolation from each other, also validate different principles. For instance, P\wedge\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt(P\rightarrow Q\wedge P)\rightarrow\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptQ is valid while P\wedge\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt(P\rightarrow Q\wedge P)\rightarrow\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptQ is not; \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt(P\sqcup Q)\rightarrow\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptP\sqcup\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptQ is valid while \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt(P\sqcup Q)\rightarrow\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptP\sqcup\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptQ is not. In its overall spirit, the earlier mentioned Blass’s repetition operator is much closer to \circ$$\mid than \wedge$$\mid , yet Blass’s semantics validates a different set of principles with than CoL does with \circ$$\mid . For instance, the following formula is invalid [33] in CoL but valid in Blass’s semantics with in the role of \circ$$\mid : P\wedge\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt(P\rightarrow Q\wedge P)\wedge\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt(R\vee Q\rightarrow R)\rightarrow\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptR.
The branching sorts of rimplication and repudiation are defined in terms of and \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt,\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt the same way as the parallel sorts of rimplication and repudiation are defined in terms of and \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt,\hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0pt:
Definition 4.15
(a) A\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptB\ =_{def}\ \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptA\rightarrow B. (b) \mbox{\circ \raisebox{0.2pt}{\scriptsize\neg}}A\ =_{def}\ \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\neg A.
Similarly to the earlier defined pimplicative reducibility, for games we say that is brimplicatively (resp. primplicatively, etc.) reducible to iff A\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptB (resp. A\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0ptB, etc.) is computable.
Exercise 4.16
The Kolmogorov complexity of a natural number is the size of a smallest Turing machine that outputs on input [math]. The Kolmogorov complexity problem \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=k(x)\bigr{)} has no algorithmic solution. Nor is it pimplicatively reducible to the halting problem. It, however, is reducible to the halting problem in the weaker sense of brimplicative reducibility, meaning that has a winning strategy for \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\bigl{(}\neg\mbox{\em Halts}(x,y)\sqcup\mbox{\em Halts}(x,y)\bigr{)}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=k(x)\bigr{)}. Describe such a strategy, informally.
Both brimplicative and primplicative reducibilities are conservative generalizations of Turing reducibility: for any predicates and , \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg p(x)\sqcup p(x)\bigr{)}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg q(x)\sqcup q(x)\bigr{)} is computable iff is Turing reducible to iff \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg p(x)\sqcup p(x)\bigr{)}\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0pt\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg q(x)\sqcup q(x)\bigr{)} is computable. Generally, when restricted to traditional sorts of problems such as problems of deciding a predicate or computing a function as in Exercise 4.16, – and – are extensionally indistinguishable. This, however, stops being the case when these operators are applied to problems with higher degrees of interactivity. For instance, the following problem is computable, but becomes incomputable with – instead of – :
[TABLE]
Generally, (P\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0ptQ)\rightarrow(P\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptQ) is valid but (P\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptQ)\rightarrow(P\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0ptQ) is not.
While both – and – are weaker than and hence more general than the latter, – is still a more interesting operation of weak reduction than – . What makes it special is the belief stated in Thesis 4.17 below. The latter, in turn, is based on the belief that \circ$$\mid (and by no means \wedge$$\mid ) is the operation allowing to reuse its argument in the strongest algorithmic sense possible.
Thesis 4.17
Brimplicative reducibility is an adequate mathematical counterpart of our intuition of reducibility in the weakest—and thus most general—algorithmic sense possible. Specifically:
(a) Whenever a problem is brimplicatively reducible to a problem , is also algorithmically reducible to according to anyone’s reasonable intuition.
(b) Whenever a problem is algorithmically reducible to a problem according to anyone’s reasonable intuition, is also brimplicatively reducible to .
The above is pretty much in the same sense as, by the Church-Turing thesis, a function is computable by a Turing machine iff has an algorithmic solution according to anyone’s reasonable intuition.
Understanding the intuitionistic negation, implication, conjunction, disjunction and quantifiers as , – , , , , , respectively, Heyting’s system for intuitionistic logic has been shown [23] to be sound with respect to the semantics of CoL. It is also “almost complete”, as the following formula of an imposing length is among the shortest known propositional formulas valid in CoL but unprovable in Heyting’s calculus:
[TABLE]
4.7 Sequential operations
This group consists of (sequential conjunction, read as “sand ”), (sequential disjunction, read as “sor ”), (sequential implication, read as “simplication ”), (sequential universal quantifier, read as “sall ”), (sequential existential quantifier, read as “sexists ”), -$$\wedge$$\mid (sequential recurrence, read as “srecurrence ”), -$$\vee$$\mid (sequential corecurrence, read as “cosrecurrence ”), – (sequential rimplication, read as “srimplication ”) and \triangleright$$\neg (sequential repudiation, read as “srepudiation ”).
The game A\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptB starts and proceeds as . It will also end as unless, at some point, the environment decides to switch to the next component, in which case is abandoned, and the game restarts, continues and ends as . A\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptB is similar, with the difference that here it is the machine who decides whether and when to switch from to .
The original formal definition of A\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptB and A\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptB found in [25] was a direct formalization of the above description. Definition 4.18 given below, while less direct, still faithfully formalizes the above intuitions, and we opt for it because it is technically simpler. Specifically, Definition 4.18 allows either player to continue making moves in even after a switch takes place; such moves are meaningless but harmless. Similarly, it allows either player to make moves in without waiting for a switch to take place, even though a smart player would only start making such moves if and when a switch happens.
Definition 4.18
Assume and are gameframes.
(a)
A_{0}\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptA_{1} is defined as the gameframe such that:
- •
iff has the form or , where every move of has the prefix “” or “” and, for both , .
- •
If does not contain a (“switch”) move , ; otherwise
(b)
A_{0}\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptA_{1} is dual to A_{0}\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptA_{1}.
(c)
A_{0}\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptA_{1}\ =_{def}\ \neg A_{0}\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptA_{1}.
Recall that, for a predicate , \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\sqsupset p(x)\bigr{)} is the problem of deciding . The similar-looking \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptp(x)\bigr{)}, on the other hand, can be seen to be the problem of semideciding : the machine has a winning strategy in this game if and only if is semidecidable, i.e., recursively enumerable. Indeed, if is recursively enumerable, a winning strategy by is to wait until brings the game down to p(n)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptp(n), i.e., \neg p(n)\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptp(n), for some particular . After that, starts looking for a certificate of ’s being true. If and when such a certificate is found (meaning that is indeed true), makes a switch move turning \neg p(n)\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptp(n) into the true ; and if no certificate exists (meaning that is false), then keeps looking for a non-existent certificate forever and thus never makes any moves, so the game ends as , which, again, is true. And vice versa: any effective winning strategy for \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg p(x)\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptp(x)\bigr{)} can obviously be seen as a semidecision procedure for , which accepts an input iff the strategy ever makes a switch move in the scenario where ’s initial choice of a value for is .
As we remember from Section 4.4, Turing reducibility of a predicate to a predicate means nothing but computability of \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}q(x)\sqsupset q(x)\bigr{)}\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0pt\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\sqsupset p(x)\bigr{)} (the same holds with – instead of – ). One can show that changing to here yields another known concept of reducibility, called enumeration reducibility (cf. [49]). That is, is enumeration reducible to iff \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}q(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptq(x)\bigr{)}\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0pt\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptp(x)\bigr{)} is computable in our sense. Similarly, the formula \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}q(x)\sqsupset q(x)\bigr{)}\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0pt\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptp(x)\bigr{)} captures relative computable enumerability (again, cf. [49]). And so on and so forth.
Existence of effective winning strategies for games is known [14] to be closed under “from and conclude ”, “from and conclude ”, “from conclude \hskip 1.0pt\mbox{\Large\sqcap}xA”, “from conclude \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptA” and similar rules. In view of such closures, the validity of the principles discussed below implies certain known facts from the theory of computation. Those examples once again demonstrate how CoL can be used as a systematic tool for defining new interesting properties and relations between computational problems, and not only reproducing already known theorems but also discovering an infinite variety of new facts.
The valid formula \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptp(x)\bigr{)}\wedge\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg p(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0pt\neg p(x)\bigr{)}\rightarrow\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\sqsupset p(x)\bigr{)} “expresses” the well known fact that, if a predicate and its complement are both recursively enumerable, then is decidable. Actually, the validity of this formula means something more: it means that the problem of deciding is reducible to (the -conjunction of) the problems of semideciding and . In fact, reducibility in an even stronger sense—a sense that has no name—holds, expressed by the formula \hskip 1.0pt\mbox{\Large\sqcap}x\Bigl{(}\bigl{(}p(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptp(x)\bigr{)}\wedge\bigl{(}\neg p(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0pt\neg p(x)\bigr{)}\rightarrow\bigl{(}p(x)\sqsupset p(x)\bigr{)}\Bigr{)}.
The formula \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}q(x)\leftrightarrow p(y)\bigr{)}\wedge\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptp(x)\bigr{)}\rightarrow\hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}q(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptq(x)\bigr{)} is also valid, which implies the known fact that, if a predicate is mapping reducible to a predicate and is recursively enumerable, then is also recursively enumerable. Again, the validity of this formula, in fact, means something even more: it means that the problem of semideciding is reducible to the problems of mapping reducing to and semideciding .
Certain other reducibilities hold only in the sense of rimplications rather than implications. Here is an example. Two Turing machines are said to be equivalent iff they accept exactly the same inputs. Let be the predicate “Turing machines and are not equivalent”. This predicate is neither semidecidable nor co-semidecidable. However, the problem of its semideciding primplicatively (and hence also brimplicatively) reduces to the halting problem. Specifically, has an effective winning strategy for the game
[TABLE]
in terms of [49] meaning that is computably enumerable relative to . The strategy is to wait till the environment specifies some values and for and . Then, create a variable , initialize it to and do the following. Specify and as and in one yet-unused copy of the antecedent, and as and in another yet-unused copy. That is, ask the environment whether halts on input and whether halts on the same input. The environment will have to provide the correct pair of answers, or else it loses. (1) If the answers are “No,No”, increment to and repeat the step. (2) If the answers are “Yes,Yes”, simulate both and on input until they halt. If both machines accept or both reject, increment to and repeat the step. Otherwise, if one accepts and one rejects, make a switch move in the consequent and celebrate victory. (3) If the answers are “Yes,No”, simulate on until it halts. If rejects , increment to and repeat the step. Otherwise, if accepts , make a switch move in the consequent and you win. (4) Finally, if the answers are “No,Yes”, simulate on until it halts. If rejects , increment to and repeat the step. Otherwise, if accepts , make a switch move in the consequent and you win.
As expected, \mbox{\large\raisebox{0.0pt}{\bigtriangleup}}xA(x) is essentially the infinite sequential conjunction A(0)\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptA(1)\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptA(2)\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt\cdots, \mbox{\large\raisebox{1.9919pt}{\bigtriangledown}}xA(x) is A(0)\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptA(1)\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptA(2)\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt\cdots, \mbox{\raisebox{-1.9919pt}{\scriptsize-}\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}}\hskip 2.0ptA is A\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptA\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptA\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt\cdots and \mbox{\raisebox{5.69046pt}{\scriptsize-}\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}}\hskip 2.0ptA is A\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptA\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptA\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt\cdots. Formally, we have:
Definition 4.19
Assume is a gameframe.
(a)
\mbox{\large\raisebox{0.0pt}{\bigtriangleup}}xA(x) is defined as the gameframe such that:
- •
iff has the form (), where every move of has the prefix “” for some and, for every such , .
- •
Call switch moves. If does not contain a switch move, then ; if contains infinitely many switch moves, then ; otherwise, where is the last switch move of , .
(b)
\mbox{\large\raisebox{1.9919pt}{\bigtriangledown}}xA(x) is dual to \mbox{\large\raisebox{0.0pt}{\bigtriangleup}}xA(x).
Definition 4.20
Assume is a gameframe.
(a)
\mbox{\raisebox{-1.9919pt}{\scriptsize-}\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}}\hskip 2.0ptA is defined as the gameframe such that:
- •
iff has the form (), where every move of has the prefix “” for some and, for every such , .
- •
Call switch moves. If does not contain a switch move, then ; if contains infinitely many switch moves, then ; otherwise, where is the last switch move of , .
(b)
\mbox{\raisebox{5.69046pt}{\scriptsize-}\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}}\hskip 2.0ptA is dual to \mbox{\raisebox{-1.9919pt}{\scriptsize-}\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}}\hskip 2.0ptA.
For insights into the above-defined operations, remember the Kolmogorov complexity function from Exercise 4.16. It is known that the value of is always smaller than (in fact, logarithmically smaller). While \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=k(x)\bigr{)} is not computable, does have an algorithmic winning strategy for the problem \hskip 1.0pt\mbox{\Large\sqcap}x\mbox{\raisebox{5.69046pt}{\scriptsize-}\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}}\hskip 2.0pt\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=k(x)\bigr{)}. It goes like this: Wait till specifies a value for , thus asking “what is the Kolmogorov complexity of ?” and bringing the game down to \mbox{\raisebox{5.69046pt}{\scriptsize-}\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}}\hskip 2.0pt\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=k(m)\bigr{)}. Answer (generously) that the complexity is , i.e. specify as . After that, start simulating, in parallel, all machines of sizes smaller than on input [math]. Whenever you find a machine that returns on input [math] and is smaller than any of the previously found such machines, make a switch move and, in the new copy of \hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=k(m)\bigr{)}, specify as the size of . This obviously guarantees success: sooner or later the real Kolmogorov complexity of will be reached and named; and, even though the strategy will never be sure that is not something yet smaller than , it will never really find a reason to further reconsider its latest claim that .
Exercise 4.21
Describe a winning strategy for \hskip 1.0pt\mbox{\Large\sqcap}x\mbox{\large\raisebox{1.9919pt}{\bigtriangledown}}y\bigl{(}k(x)=x-y\bigr{)}.
Definition 4.22
(a) A\hskip 3.0pt\mbox{\mbox{\raisebox{0.1pt}{\small\triangleright}} \raisebox{-0.8pt}{\large--}}\hskip 3.0ptB\ =_{def}\ \mbox{\raisebox{-1.9919pt}{\scriptsize-}\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}}\hskip 2.0ptA\rightarrow B. (b) \hskip 1.0pt\mbox{\raisebox{0.1pt}{\small\triangleright}{\scriptsize\neg}}A\ =_{def}\ \mbox{\raisebox{5.69046pt}{\scriptsize-}\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}}\hskip 2.0pt\neg A.
4.8 Toggling operations
This group consists of (toggling conjunction, read as “tand ”), (toggling disjunction, read as “tor ”), (toggling implication, read as “timplication ”), (toggling universal quantifier, read as “tall ”), (toggling existential quantifier, read as “texists ”), \wedge$$\mid (toggling recurrence, read as “trecurrence ”), \vee$$\mid (toggling corecurrence, read as “cotrecurrence ”), – (toggling rimplication, read as “trimplication ”) and - (toggling repudiation, read as “trepudiation ”).
Let us for now focus on . One of the ways to characterize A\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}B is the following. This game starts and proceeds as a play of . It will also end as an ordinary play of unless, at some point, decides to switch to , after which the game becomes and continues as such. It will also end as unless, at some point, “changes its mind” and switches back to . In such a case the game again becomes , where resumes from the position in which it was abandoned (rather than from its start position, as would be the case, e.g., in A\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptB\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptA). Later may again switch to the abandoned position of , and so on. wins the overall play iff it switches from one component to another at most finitely many times and wins in its final choice, i.e., in the component which was chosen last to switch to.
An alternative characterization A\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}B, on which our formal definition of is directly based, is to say that it is played just like , with the only difference that is allowed to make a “choose ” or “choose ” move any number of times. If infinitely many choices are made, loses. Otherwise, the winner in the play will be the player who wins in the component that was chosen last (“the eventual choice”). The case of having made no choices at all is treated as if it had chosen . Thus, as in A\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptB, the left component is the “default”, or “automatically made”, initial choice. It is important to note that ’s adversary—or perhaps even itself—never knows whether a given choice of a component of A\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}B is the last choice or not.
What would happen if we did not require that can change its mind only finitely many times? There would be no “final choice” in this case. So, the only natural winning condition in the case of infinitely many choices would be to say that wins iff it simply wins in one of the components. But then the resulting operation would be essentially the same as , as a smart would always opt for keeping switching between components forever. That is, allowing infinitely many choices would amount to not requiring any choices at all, as is the case with .
The very weak sort of choice captured by is the kind of choice that, in real life, one would ordinarily call choice after trial and error. Indeed, a problem is generally considered to be solved after trial and error (a correct choice/solution/answer found) if, after perhaps coming up with several wrong solutions, a true solution is eventually found. That is, mistakes are tolerated and forgotten as long as they are eventually corrected. It is however necessary that new solutions stop coming at some point, so that there is a last solution whose correctness determines the success of the effort. Otherwise, if answers have kept changing all the time, no answer has really been given after all.
As we remember, for a predicate , \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\sqsupset p(x)\bigr{)} is the problem of deciding , and \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptp(x)\bigr{)} is the weaker (easier to solve) problem of semideciding . Not surprisingly, \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}p(x)>-\hskip 2.0ptp(x)\bigr{)}—which abbreviates \hskip 1.0pt\mbox{\Large\sqcap}x\bigl{(}\neg p(x)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}p(x)\bigr{)}—is also a decision-style problem, but still weaker than the problem of semideciding . This problem has been studied in the literature under several names, the most common of which is recursively approximating . It means telling whether is true or not, but doing so in the same style as semideciding does in negative cases: by correctly saying “Yes” or “No” at some point (after perhaps taking back previous answers several times) and never reconsidering this answer afterwards. In similar terms, semideciding can be seen as always saying (the default) “No” at the beginning and then, if this answer is incorrect, changing it to “Yes” at some later time; so, when the answer is negative, this will be expressed by saying “No” and never taking back this answer, yet without ever indicating that the answer is final and will not change. Thus, the difference between semideciding and recursively approximating is that, unlike a semidecision procedure, a recursive approximation procedure can reconsider both negative and positive answers, and do so several times rather than only once.
As an example of a predicate which is recursively approximable but neither semidecidable nor co-semidecidable, consider the predicate , saying that number is simpler than number in the sense of Kolmogorov complexity. As noted earlier, (the Kolmogorov complexity of ) is always smaller than . Here is an algorithm that recursively approximates the predicate , i.e., solves the problem \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\bigl{(}k(x)\geq k(y)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}k(x)<k(y)\bigr{)}. Wait till the environment brings the game down to k(m)\geq k(n)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}k(m)<k(n) for some and . Then start simulating, in parallel, all Turing machines of sizes less than on input [math]. Whenever you see that a machine returns and the size of is smaller than that of any other previously found machine that returns or on input [math], choose . Quite similarly, whenever you see that a machine returns and the size of is smaller than that of any other previously found machine that returns on input [math], as well as smaller or equal to the size of any other previously found machine that returns on input [math], choose . Obviously, the correct choice between and will be made sooner or later and never reconsidered afterwards. This will happen when the procedure hits a smallest-size machine that returns either or on input [math].
Anyway, here is our formal definition of , and :
Definition 4.23
Assume and are gameframes.
(a)
A_{0}\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptA_{1} is defined as the gameframe such that:
- •
iff has the form (), where , every move of has the prefix “” or “” and, for both , .
- •
Call and switch moves. If does not contain a switch move, then ; if contains infinitely many switch moves, then ; otherwise, where is the last switch move of , .
(b)
A_{0}\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}A_{1} is dual to A_{0}\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptA_{1}.
(c)
A_{0}>-\hskip 2.0ptA_{1}\ =_{def}\ \neg A_{0}\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}A_{1}.
From the formal definitions that follow one can see that, as expected, \mbox{\hskip 1.0pt\Large\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{8.53581pt}}\hskip 6.0pt}xA(x) is essentially A(0)\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptA(1)\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt A(2)\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt\cdots, \hskip 1.0pt\mbox{\Large\vee\raisebox{0.28453pt}{\rule{0.36989pt}{8.53581pt}}\hskip 5.0pt}xA(x) is A(0)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}A(1)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}A(2)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\cdots, \mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{1.70709pt}{\small\mid}\hskip 2.0pt}A is A\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptA\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptA\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt\cdots and \mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{1.13791pt}{\small\mid}\hskip 2.0pt}xA(x) is A\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}A\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}A\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\cdots.
Definition 4.24
Assume is a gameframe.
(a)
\mbox{\hskip 1.0pt\Large\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{8.53581pt}}\hskip 6.0pt}xA(x) is defined as the gameframe such that:
- •
iff has the form (), where , every move of has the prefix “” for some and, for every such , .
- •
Call the above switch moves. If does not contain a switch move, then ; if contains infinitely many switch moves, then ; otherwise, where is the last switch move of , .
(b)
\hskip 1.0pt\mbox{\Large\vee\raisebox{0.28453pt}{\rule{0.36989pt}{8.53581pt}}\hskip 5.0pt}xA(x) is dual to \mbox{\hskip 1.0pt\Large\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{8.53581pt}}\hskip 6.0pt}xA(x).
Definition 4.25
Assume is a gameframe.
(a)
\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{1.70709pt}{\small\mid}\hskip 2.0pt}A is defined as the gameframe such that:
- •
iff has the form (), where , every move of has the prefix “” for some and, for every such , .
- •
Call the above switch moves. If does not contain a switch move, then ; if contains infinitely many switch moves, then ; otherwise, where is the last switch move of , .
(b)
\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{1.13791pt}{\small\mid}\hskip 2.0pt}A is dual to \mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{1.70709pt}{\small\mid}\hskip 2.0pt}A.
To see toggling quantifiers at work, remember that Kolmogorov complexity is not a computable function, i.e., the problem \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=k(x)\bigr{)} has no algorithmic solution. However, replacing \hskip 1.0pt\mbox{\Large\sqcup}y with \hskip 1.0pt\mbox{\Large\vee\raisebox{0.28453pt}{\rule{0.36989pt}{8.53581pt}}\hskip 5.0pt}y in it yields an algorithmically solvable problem. A solution for \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\vee\raisebox{0.28453pt}{\rule{0.36989pt}{8.53581pt}}\hskip 5.0pt}y\bigl{(}y=k(x)\bigr{)} goes like this. Wait till the environment chooses a number for , thus bringing the game down to \hskip 1.0pt\mbox{\Large\vee\raisebox{0.28453pt}{\rule{0.36989pt}{8.53581pt}}\hskip 5.0pt}y\bigl{(}y=k(m)\bigr{)}, which is essentially nothing but 0=k(m)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}1=k(m)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}2=k(m)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\cdots. Create a variable initialized to , and perform the following routine: Switch to the disjunct of 0=k(m)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}1=k(m)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}2=k(m)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\cdots and then start simulating on input [math], in parallel, all Turing machines whose sizes are smaller than ; if and when you see that one of such machines returns , update to the size of that machine, and repeat the present routine.
Definition 4.26
(a) A\mbox{\hskip 2.0pt\raisebox{0.93907pt}{\tiny>} \raisebox{-2.4pt}{\LARGE--}\hskip 2.0pt}B\ =_{def}\ \mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{1.70709pt}{\small\mid}\hskip 2.0pt}A\rightarrow B. (b) \mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-0.5pt}{\large-}{\scriptsize\neg}}A\ =_{def}\ \mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{1.13791pt}{\small\mid}\hskip 2.0pt}\neg A.
4.9 Cirquents
The constructs called cirquents take the expressive power of CoL to a qualitatively higher level, allowing us to form, in a systematic way, an infinite variety of game operations. Each cirquent is—or can be seen as—an independent operation on games, generally not expressible via composing operations taken from some fixed finite pool of primitives, such as the operations seen in the preceding subsections of the present section.
Cirquents come in a variety of versions, but common to all them is having mechanisms for explicitly accounting for possible sharing of subcomponents between different components. Sharing is the main distinguishing feature of cirquents from more traditional means of expression such as formulas, sequents, hypersequents [2], or structures of the calculus of structures [12]. While the latter can be drawn as (their parse) trees, cirquents more naturally call for circuit- or graph-style constructs. The earliest cirquents [17] were intuitively conceived as collections of one-sided sequents (sequences of formulas) that could share some formulas and, as such, could be drawn like circuits rather than linear expressions. This explains the etimology of the word: CIRcuit+seQUENT. All Boolean circuits are cirquents, but not all cirquents are Boolean circuits. Firstly, because cirquents may have various additional sorts of gates (-gates, -gates, -gates, etc.). Secondly, because cirquents may often have more evolved sharing mechanisms than just child- (input-) sharing between different gates. For instance, a “cluster” [29] of -gates may share choices associated with in game-playing: if the machine chooses the left or the right child for one gate of the cluster, then the same left or right choice automatically extends to all gates of the cluster regardless of whether they share children or not.
We are not going to introduce cirquents and their semantics in full generality or formal detail here. For intuitive insights, let us only focus on cirquents that look like Boolean circuits with - and -gates. Every such cirquent can be seen as an -ary parallel operation on games, where is the number of inputs of .
P$$Q$$R$$\wedge$$\wedge$$\wedge$$\veeFigure 3:The two-out-of-three combination of resourcesP$$P$$P$$\wedge$$\wedge$$\wedge$$\vee
The left cirquent of Figure 3 represents the 3-ary game operation informally defined as follows. Playing , as is the case with all parallel operations, means playing simultaneously in all components of it. In order to win, needs to win in at least two out of the three components. Any attempt to express this operation in terms of or other already defined operations is going to fail. For instance, the natural candidate is very far from being adequate. The latter is a game on six rather than three boards, with played on boards #1 and #3, on boards #2 and #5, and on boards #4 and #6. Similarly, the formula is not an adequate representation of the right cirquent of Figure 3. It fails to indicate for instance that the 1st and the 3rd occurrences of stand for the same copy of while the 2nd occurrence for a different copy in which a different run can be generated.
Cirquents are thus properly more expressive than formulas even at the most basic level. It is this added expressiveness and flexibility that, for some fragments of CoL, makes a difference between axiomatizability and unaxiomatizability: even if one is only trying to set up a deductive system for proving valid formulas, intermediate steps in proofs of such formulas still inherently require using cirquents that cannot be written as formulas. An example is the system CL15 found in Section 7.1.
The present article is exclusively focused on the formula-based version of CoL, seeing cirquents (in Section 7.1) only as technical servants to formulas. This explains why we do not attempt to define the semantics of cirquents formally. It should however be noted that cirquents are naturally called for not only within the specific formal framework of CoL, but also in the framework of all resource-sensitive approaches in logic, like linear logic. Such approaches may intrinsically require the ability to account for the ubiquitous phenomenon of resource sharing. The insufficient expressiveness of linear logic is due to the inability of formulas to explicitly show (sub)resource sharing or the absence thereof. The right cirquent of Figure 3 stands for a multiplicative-style disjunction of three resources, with each disjunct, in turn, being a conjunction of two subresources of type . However, altogether there are three rather than six such subresources, each one being shared between two different disjuncts of the main resource. From the abstract resource-philosophical point of view of cirquent-based CoL, classical logic and linear logic are two imperfect extremes. In the former, all occurrences of a same subformula mean the same (represent the same resource), i.e., everything is shared that can be shared; and in the latter, each occurrence stands for a separate resource, i.e., nothing is shared at all. Neither approach does thus permit to account for mixed cases where certain occurrences are meant to represent the same resource while some other occurrences stand for different resources of the same type.
5 Static games
While games in the sense of Definition 2.1 are apparently general enough to model anything one would call an interactive computational problem, they are a little bit too general. Consider a game Bad whose only nonempty legal runs are , won by , and , won by . Whichever player is fast enough to make the move first will thus be the winner. Since there are no natural, robust assumptions regarding the relative speeds of the players, obviously Bad is not something that could qualify as a meaningful computational problem. For such reasons, CoL limits its focus on a natural proper subclass of all games in the sense of Definition 2.1 called static. Intuitively, static games are games where speed is irrelevant because, using Blass’s words, “it never hurts a player to postpone making moves”.
In order to define static games, recall that, for a player , means “the other player”. Further recall the concepts of a -legal and -won runs from Section 2. Given a run , we let denote the subsequence of (all and only) -labeled moves of ; similarly for . We say that a run is a -delay of a run iff the following two conditions are satisfied:
- •
and ;
- •
For any , if the th -labeled move is made earlier than the th -labeled move in , then so is it in .
The above , in other words, is the result of possibly shifting to the right (“delaying”) some -labeled moves in without otherwise violating the order of moves by either player.
Definition 5.1
We say that a game is static iff, for either player and for any runs where is a -delay of , the following conditions are satisfied:
If is a -legal run of , then so is . 2. 2.
If is a -won run of , then so is .
A gameframe is said to be static iff so are all of its instances.
Exercise 5.2
Verify that the game of Figure 1 is static.
The class of static games or gameframes is very broad. Suffice it to say that all elementary gameframes are static, and that all operations defined in the preceding long section preserve the static property of gameframes. Thus, the closure of elementary gameframes under those operations is one natural subclass of the class of all static games.
6 The formal language of computability logic and its semantics
It is not quite accurate to say “the language” of CoL because, as pointed out earlier, CoL has an open-ended formalism. Yet, in the present article, by “the language of CoL” we will mean the particular language defined below. It extends the language of first-order classical logic by adding to it all operators defined in Section 4, and differentiating between two—elementary and general—sorts of atoms.
The set Variables of variables and the set Constants of constants of the language are those fixed in Section 3. Per each natural number , we also have infinitely many -ary extralogical function letters, elementary gameframe letters and general gameframe letters. We usually use as metavariables for function letters, for elementary gameframe letters, and for general gameframe letters. Other than these extralogical letters, there are three logical gameframe letters, all elementary: (nullary), (nullary) and (binary).
Terms are defined inductively as follows:
- •
All variables and constants are terms.
- •
If are terms () and is an -ary function letter, then is a term.
Atoms are defined by:
- •
and are atoms. These two atoms are said to be logical, and all other atoms extralogical.
- •
If and are terms, then is an atom.
- •
If are terms () and is an extralogical -ary game letter, then is an atom. Such an extralogical atom is said to be elementary or general iff is so.
Finally, formulas are defined by:
- •
All atoms are formulas.
- •
If is a formula, then so are , \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt(E), \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt(E), \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt(E), \hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0pt(E), \mbox{\raisebox{-1.9919pt}{\scriptsize-}\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}}\hskip 2.0pt(E), \mbox{\raisebox{5.69046pt}{\scriptsize-}\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}}\hskip 2.0pt(E), \mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{1.70709pt}{\small\mid}\hskip 2.0pt}(E), \mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{1.13791pt}{\small\mid}\hskip 2.0pt}(E), \mbox{\circ \raisebox{0.2pt}{\scriptsize\neg}}(E), \mbox{\raisebox{1.1pt}{\tiny>}{\scriptsize\neg}}(E), \hskip 1.0pt\mbox{\raisebox{0.1pt}{\small\triangleright}{\scriptsize\neg}}(E), \mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-0.5pt}{\large-}{\scriptsize\neg}}(E).
- •
If and are formulas, then so are , , , , (E)\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt(F), (E)\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt(F), (E)\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt(F), (E)\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}(F), , , (E)\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0pt(F), , (E)\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt(F), (E)\hskip 2.0pt\mbox{\raisebox{0.93907pt}{\tiny>} \raisebox{-1.22343pt}{\large--}}\hskip 2.0pt(F), (E)\hskip 3.0pt\mbox{\mbox{\raisebox{0.1pt}{\small\triangleright}} \raisebox{-0.8pt}{\large--}}\hskip 3.0pt(F), (E)\mbox{\hskip 2.0pt\raisebox{0.93907pt}{\tiny>} \raisebox{-2.4pt}{\LARGE--}\hskip 2.0pt}(F).
- •
If is a formula and is a variable, then \mbox{\large\forall}x(E), \mbox{\large\exists}x(E), \hskip 1.0pt\mbox{{\Large\wedge}}\hskip 1.0ptx(E), \mbox{{\Large\vee}}x(E), \hskip 1.0pt\mbox{\Large\sqcap}x(E), \hskip 1.0pt\mbox{\Large\sqcup}x(E), \mbox{\large\raisebox{0.0pt}{\bigtriangleup}}x(E), \mbox{\large\raisebox{1.9919pt}{\bigtriangledown}}x(E), \mbox{\hskip 1.0pt\Large\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{8.53581pt}}\hskip 6.0pt}x(E), \hskip 1.0pt\mbox{\Large\vee\raisebox{0.28453pt}{\rule{0.36989pt}{8.53581pt}}\hskip 5.0pt}x(E) are formulas.
Unnecessary parentheses will be usually omitted in formulas according to the standard conventions, with partial precedence order as agreed upon earlier for the corresponding game operations. The notions of free and bound occurrences of variables are also standard, with the only adjustment that now we have eight rather than two quantifiers. A sentence, or a closed formula, is a formula with no free occurrences of variables. While officially is a binary operator, we may still write for a possibly unspecified . This should be understood as when , as just when , and as when . Similarly for all other sorts of conjunctions. And similarly for all disjunctions, with the difference that an empty disjunction of whatever sort is understood as rather than .
For the following definitions, recall Conventions 3.3 and 3.4. Also recall that are the first variables from the lexicographic list of all variables.
Definition 6.1
An interpretation is a mapping ∗ such that, for some fixed universe called the universe of ∗, we have:
- •
∗ sends every -ary function letter to an -ary function whose universe is and whose variables are the first variables of Variables.
- •
∗ sends every -ary extralogical game letter to an -ary static gameframe whose universe is and whose variables are the first variables of Variables; besides, if the letter is elementary, then so is the gameframe .
Such a ∗ is said to be admissible for a formula (or -admissible) iff, whenever has an occurrence of a general atom in the scope of \mbox{\large\forall}x or \mbox{\large\exists}x and one of the terms () contains the variable , is unistructural in . We uniquely extend ∗ to a mapping that sends each term to a function , and each formula for which it is admissible to a game , by stipulating the following:
- •
Where is a constant, is (the nullary function) .
- •
Where is a variable, is (the unary function) .
- •
Where is an -ary function letter and are terms, \bigl{(}f(t_{1},\cdots,t_{n})\bigr{)}^{*} is .
- •
is and is .
- •
Where and are terms, is .
- •
Where is an -ary gameframe letter and are terms, \bigl{(}L(t_{1},\cdots,t_{n})\bigr{)}^{*} is .
- •
∗ commutes with all logical operators, seeing them as the corresponding game operations: is , (\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptE)^{*} is \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt(E^{*}), is , (\hskip 1.0pt\mbox{\Large\sqcap}xE)^{*} is \hskip 1.0pt\mbox{\Large\sqcap}x(E^{*}), etc.
When is a function letter, gameframe letter, term or formula and , we refer to as “ under interpretation ∗”.
Definition 6.2
For a sentence we say that:
-
is logically valid iff there is an HPM such that, for every -admissible interpretation ∗, computes . Such an is said to be a logical solution of .
-
is extralogically valid iff for every -admissible interpretation ∗ there is an HPM such that computes .
Convention 6.3
When is a formula but not a sentence, its validity is understood as that of the -closure of , i.e., of the sentence \hskip 1.0pt\mbox{\Large\sqcap}x_{1}\cdots\hskip 1.0pt\mbox{\Large\sqcap}x_{n}S, where are all free variables of listed lexicographically.
Every logically valid formula is, of course, also extralogically valid. But some extralogically valid formulas may not necessarily be also logically valid. For instance, where is a [math]-ary elementary gameframe letter, the formula is valid extralogically but not logically. It is extralogically valid for a trivial reason: given an interpretation ∗, either or is true under ∗. If is true, then the strategy that chooses the first disjunct wins; and if is true, then the strategy that chooses the second disjunct wins. The trouble is that, even though we know that one of these two strategies succeeds, generally we have no way to tell which one does. And this is why fails to be logically valid.
Extralogical validity is not only a non-constructive, but also a fragile sort of validity: this property, unlike logical validity, is not closed under substitution of extralogical atoms. For instance, where is as before and is a unary extralogical elementary gameframe letter, the formula , while having the same form as , is no longer extralogically valid. The papers on CoL written prior to 2016 had a more relaxed understanding of interpretations than our present understanding. Namely, there was no requirement that an interpretation should respect the arity of a gameframe letter. In such a case, as it turns out, the extensional difference between logical and extralogical validity disappears: while the class of logically valid principles remains the same, the class of extralogically valid principles shrinks down to that of logically valid ones.
Intuitively, a logical solution for a sentence is an interpretation-independent winning strategy: since the intended interpretation is not known to the machine, has to play in some standard, uniform way that would be successful for any possible interpretation of . It is logical rather than extralogical validity that is of interest in all applied systems based on CoL (cf. Section 8). In such applications we want a logic that could be built into a universal problem-solving machine. Such a machine should be able to solve problems represented by logical formulas without any specific knowledge of the meanings of their atoms, other than the knowledge explicitly provided in the knowledgebase (extralogical axioms) of the system. Otherwise the machine would be special-purpose rather than universal. For such reasons, in the subsequent sections we will only be focused on the logical sort of validity, which will be the default meaning of the word “valid”.
Definition 6.4
We say that a sentence is a logical consequence of a set of sentences iff, for some , the sentence E_{1}\wedge\cdots\wedge E_{n}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF is logically valid.
Remember the symmetry between computational resources and computational problems: a problem for one player is a resource for the other. Having a problem as a computational resource intuitively means having the (perhaps externally provided) ability to successfully solve/win . For instance, as a resource, \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{2}) means the ability to tell the square of any number. According to Thesis 6.5 below, the relation of logical consequence lives up to its name. The main utility of this thesis, as will be illustrated in Section 7.3, is that it allows us to rely on informal, intuitive arguments instead of formal proofs when reasoning within CoL-based applied theories.
Thesis 6.5
Consider sentences () and an admissible interpretation ∗ for them. Assume there is a winning strategy for that relies on availability and “recyclability”—in the strongest sense possible—of as computational resources but no other knowledge or assumptions about ∗ (see Example 7.10 for an instance of such a strategy). Then is a logical consequence of .
7 Axiomatizations
While a semantical setup for CoL in the language of Section 6 is complete, a corresponding proof theory is still at earlier stages of development. Due to the inordinate expressive power of the language, successful axiomatization attempts have only been made for various fragments of CoL obtained by moderating its language in one way or another. It should be pointed out that every conceivable application of CoL will only need some fragment of CoL rather than the “whole” CoL anyway.
As of 2020 there are seventeen deductive systems for various fragments of CoL, named CL1 through CL17. Based on their languages, these systems can be divided into three groups: elementary-base, general-base and mixed-base. Of the extralogical gameframe letters, the languages of elementary-base systems only allow elementary ones, the languages of general-base systems only allow general ones, and the languages of mixed-base system allow both sorts of letters. Based on the style of the underlying proof theory, the systems can be further subdivided into two groups: cirquent calculus systems and brute force systems. Either sort is rather unusual, not seen elsewhere in proof theory. The cirquent calculus systems operate with cirquents rather than formulas, with formulas understood as special cases of cirquents. The brute force systems operate with formulas (sometimes referred to as sequents for technical reasons), but in an unusual way, with their inference rules being relatively directly derived from the underlying game semantics and hence somewhat resembling games themselves.
Theorem 7.1
Each of the above-mentioned systems is adequate in the sense that, for any sentence of the language of S, we have:
(a) Soundness:
If is provable in , then it is logically valid and, furthermore, a logical solution for can be automatically extracted from a proof of .
(b) Completeness:
If is logically valid, then it is provable in S.
In this article we shall take a look at only three of the systems: the general-base cirquent calculus system CL15 in the logical signature \{\neg,\wedge,\vee,\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt,\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\}, the mixed-base brute force system CL13 in the signature \{\neg,\wedge,\vee,\sqcap,\sqcup,\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt,\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt,\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt,\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\}, and the elementary-base brute force system CL12 in the signature \{\neg,\wedge,\vee,\sqcap,\sqcup,\mbox{\large\forall},\mbox{\large\exists},\hskip 1.0pt\mbox{\Large\sqcap},\hskip 1.0pt\mbox{\Large\sqcup},\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\} (with – only allowed to be applied externally). Their adequacy proofs can respectively be found in [34, 35], [28] and [37].
7.1 The cirquent calculus system CL15
CL15-formulas—or just formulas in this subsection—are formulas of the language of CoL that do not contain any function letters, do not contain any gameframe letters other than [math]-ary general gameframe letters, and do not contain any operators other than \neg,\wedge,\vee,\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt,\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt. Besides, is only allowed to be applied to atoms. Shall we still write for a nonatomic , it is to be understood as the standard DeMorgan abbreviation defined by , , , \neg\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptF=\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\neg F, \neg\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF=\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt\neg F. Similarly, , F\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptG and \mbox{\circ \raisebox{0.2pt}{\scriptsize\neg}}F should be understood as , \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\neg F\vee G and \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\neg F, respectively.
Definition 7.2
A CL15-cirquent (henceforth simply “cirquent”) is a triple where:
-
is a nonempty finite sequence of CL15-formulas, whose elements are said to be the oformulas of . 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 , then the cirquent has three oformulas even if only two formulas.
-
Both and are nonempty finite sequences of nonempty sets of oformulas of . The elements of are said to be the undergroups of , and the elements of are said to be the overgroups of . As in the case of oformulas, it is possible that two undergroups or two overgroups are identical as sets (have identical contents), yet they count as different undergroups or overgroups because they occur at different places in the sequence or . Simply “group” will be used as a common name for undergroups and overgroups.
-
Additionally, every oformula is required to be in 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 ” if it is clear from the context which of the possibly many occurrences of 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:
F_{1}$$F_{2}$$F_{3}$$F_{4}
This diagram represents the cirquent with four oformulas , three undergroups and two overgroups , . Each (under- or over-) group is represented by a , where the arcs (lines connecting the ’s with oformulas) are pointing to the oformulas that the given group contains.
CL15 has ten rules of inference. The first one takes no premises, which qualifies it as an axiom. All other rules take a single premise. 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 7.2, while possible, is hardly necessary.
Axiom (A): The conclusion of this premiseless rule looks like an array of () “diamonds” as seen below for the case of , where the oformulas within each diamond are and for some formula .
A\neg F_{1}$$F_{1}$$\neg F_{2}$$F_{2}$$\neg F_{3}$$F_{3}
Exchange (E): 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, one per each sort of Exchange. In all cases, of course, the upper cirquent is the premise and the lower cirquent is the conclusion of an application of the rule.
F$$G$$HEF$$G$$HEF$$H$$G$$F$$G$$HEF$$G$$H$$F$$G$$H
The presence of Exchange essentially allows us to treat all three components of a cirquent as multisets rather than sequences.
Weakening (W): The premise of this rule is obtained from the conclusion by deleting an arc between some undergroup with elements and some oformula ; if was the only undergroup containing , then should also be deleted (to satisfy condition 3 of Definition 7.2), together with all arcs between and overgroups; if such a deletion makes some overgroups empty, then they should also be deleted (to satisfy condition 2 of Definition 7.2). Below are three examples:
E$$FWE$$F$$FWE$$F$$FWE$$F
Contraction (C): The premise of this rule is obtained from the conclusion through replacing an oformula \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF by two adjacent oformulas \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF,\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF, and including them in exactly the same undergroups and overgroups in which the original oformula was contained. Example:
H$$\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF$$\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF$$GCH$$\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF$$G
Duplication (D): 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 with two adjacent undergroups whose contents are identical to that of . Similarly for Overgroup Duplication. Examples:
F$$G$$HDF$$G$$H$$F$$G$$HDF$$G$$H
Merging (M): In the top-down view, this rule merges any two adjacent overgroups, as illustrated below.
F$$GMF$$G$$F$$GMF$$G$$F$$GMF$$G$$F$$G$$HMF$$G$$H
Disjunction Introduction (): The premise of this rule is obtained from the conclusion through replacing an oformula by two adjacent oformulas , and including both of them in exactly the same undergroups and overgroups in which the original oformula was contained, as illustrated below:
E$$F$$\vee$$E\vee F$$H$$F$$G$$E$$\vee$$H$$F\vee G$$E
Conjunction Introduction (): The premise of this rule is obtained from the conclusion by picking an arbitrary oformula and applying the following two steps:
- •
Replace by two adjacent oformulas , and include both of them in exactly the same undergroups and overgroups in which the original oformula was contained.
- •
Replace each undergroup originally containing (and now containing instead) by the two adjacent undergroups and .
Below we see three examples.
E$$F$$\wedge$$E\wedge F$$E$$F$$G$$\wedge$$E$$F\wedge G$$E$$F$$G$$H$$\wedge$$E$$F\wedge G$$H
Recurrence Introduction (\circ$$\mid ): The premise of this rule is obtained from the conclusion through replacing an oformula \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptF by (while preserving all arcs), and inserting, anywhere in the cirquent, a new overgroup that contains as its only oformula. Examples:
G$$\circ.....\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptG$$F$$G$$H$$\circ.....F$$G$$\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptH
Corecurrence Introduction (\circ$$\mid ): The premise of this rule is obtained from the conclusion through replacing an oformula \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF by , and including in any (possibly zero) number of the already existing overgroups in addition to those in which the original oformula \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF was already present. Examples:
F$$G$$H$$\circ.....F$$G$$\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptH$$F$$G$$H$$\circ.....F$$G$$\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptH$$F$$G$$H$$\circ.....F$$G$$\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptH
A proof (in CL15) of a cirquent is a sequence of cirquents ending in such that the first cirquent is the conclusion of (an instance of) Axiom, and every subsequent cirquent follows from the immediately preceding cirquent by one of the rules of CL15. A proof of a formula is understood as a proof of the cirquent .
As an example, below is a proof of the formula \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptF\rightarrow\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF, i.e., \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\neg F\vee\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF. To save space, the cirquents in it have been arranged horizontally, separated with ’s together with the symbolic names of the rules used; if such a name is duplicated as in DD, it means that the rule was applied twice rather than once.
A\Longrightarrow$$\neg F$$FDD\Longrightarrow$$\neg F$$F$$\circ..........\Longrightarrow$$\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\neg F$$\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF$$\circ..........\Longrightarrow$$\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\neg F$$\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF$$\vee$$\Longrightarrow$$\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\neg F\vee\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5ptF
Exercise 7.3
Prove the following formulas in CL15:
- •
F\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF (i.e. \mbox{\circ \raisebox{0.2pt}{\scriptsize\neg}}F\vee F, i.e. \mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt\neg F\vee F).
- •
.
- •
F\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptF\wedge\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptF.
- •
F\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptF.
- •
\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptE\vee\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptF\rightarrow\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt(E\vee F).
- •
.
W. Xu and S. Liu [53] showed that CL15 remains sound with \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt,\hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0pt instead of \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt,\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt. Completeness, however, is lost in this case because, for instance, as shown in [33], the formula F\wedge\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt(F\rightarrow F\wedge F)\rightarrow\hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0ptF is logically valid while F\wedge\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt(F\rightarrow F\wedge F)\rightarrow\mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5ptF is not.
Open Problem 7.4
Is (the problem of provability in) CL15 decidable? 2. 2.
Extend the language of CL15 by including and axiomatize (if possible) the set of logically valid formulas in this extended language. 3. 3.
Replace \mbox{\raisebox{-1.42271pt}{\circ}\raisebox{3.9pt}{\tiny\mid}}\hskip 1.5pt,\mbox{\raisebox{3.41418pt}{\circ}\raisebox{0.56917pt}{\tiny\mid}}\hskip 1.5pt with \hskip 1.0pt\mbox{\raisebox{-0.28436pt}{\scriptsize\wedge}\raisebox{4.55254pt}{\tiny\mid}}\hskip 2.0pt,\hskip 1.0pt\mbox{\raisebox{3.41418pt}{\scriptsize\vee}\raisebox{0.56917pt}{\tiny\mid}}\hskip 2.0pt in the language of CL15. Is the set of logically valid formulas in this new language axiomatizable and, if yes, how? 4. 4.
Does CL15 remain complete with respect to extralogical (as opposed to logical) validity?
7.2 The brute force system CL13
CL13-formulas—or just formulas in this subsection—are formulas of the language of CoL that do not contain any function letters or non-nullary gameframe letters, and do not contain any operators other than \neg,\wedge,\vee,\sqcap,\sqcup,\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt,\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt,\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt,\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}. As in the case of CL15, officially is only allowed to be applied to extralogical atoms, otherwise understood as the corresponding DeMorgan abbreviation, including understanding as and as . Each of the implication operators \rightarrow,\sqsupset,\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0pt,>-\hskip 2.0pt should also be understood as an abbreviation of its standard meaning in terms of negation and the corresponding sort of disjunction. To define the system axiomatically, we need certain terminological conventions.
- •
A literal means an atom with or without negation . Such a literal is said to be elementary or general iff is so.
- •
As in Section 7.1, we often need to differentiate between subformulas as such, and particular occurrences of subformulas. We will be using the term osubformula to mean a subformula together with a particular occurrence. The prefix “o” will be used with a similar meaning in terms such as oatom, oliteral, etc.
- •
An osubformula is positive iff it is not in the scope of . Otherwise it is negative. According to our conventions regarding the usage of , only oatoms may be negative.
- •
A politeral is a positive oliteral.
- •
A -(sub)formula is a (sub)formula of the form . Similarly for the other connectives.
- •
A sequential (sub)formula is one of the form E\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptF or E\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptF. We say that is the head of such a (sub)formula, and is its tail.
- •
Similarly, a parallel (sub)formula is one of the form or , a choice (sub)formula is one of the form or , and a toggling (sub)formula is one of the form E\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptF or E\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}F.
- •
A formula is said to be quasielementary iff it contains no general atoms and no operators other than \neg,\wedge,\vee,\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt,\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}.
- •
A formula is said to be elementary iff it is a formula of classical propositional logic, i.e., contains no general atoms and no operators other than .
- •
A semisurface osubformula (or occurrence) is an osubformula (or occurrence) which is not in the scope of a choice connective.
- •
A surface osubformula (or occurrence) is an osubformula (or occurrence) which is not in the scope of any connectives other than .
- •
The quasielementarization of a formula , denoted by , is the result of replacing in 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, the quasielementarization of \bigl{(}(P\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}q)\vee\bigl{(}(p\wedge\neg P)\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt(Q\wedge R)\bigr{)}\bigr{)}\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt\bigl{(}q\sqcap(r\sqcup s)\bigr{)} is \bigl{(}(\bot\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}q)\vee(p\wedge\bot)\bigr{)}\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt\top.
- •
The elementarization of a quasielementary formula , denoted by , is the result of replacing in every -osubformula by and every -osubformula by (again, the order of these replacements does not matter). For instance, \|\bigl{(}s\wedge\bigl{(}p\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt(q\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}r)\bigr{)}\bigr{)}\vee\bigl{(}\neg s\vee(p\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}r)\bigr{)}\|=(s\wedge\top)\vee(\neg s\vee\bot).
- •
A quasielementary formula is said to be stable iff its elementarization is a tautology of classical logic.
We now define CL13 by the following six rules of inference, where means “from premise(s) conclude ”. Axioms are not explicitly stated, but the set of premises of the (\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt) rule can be empty, in which case (the conclusion of) this rule acts like an axiom.
Rule (\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt):
, where is a stable quasielementary formula, and is the smallest set of formulas satisfying the following condition:
- •
Whenever has a surface osubformula E_{0}\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptE_{1}, for both , contains the result of replacing in that osubformula by .
Rule (\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}):
, where is a quasielementary formula, and is the result of replacing in a surface osubformula E\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}G by or .
Rule (\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt\sqcap):
, where is a non-quasielementary formula (note that otherwise ), and is the smallest set of formulas satisfying the following two conditions:
- •
Whenever has a semisurface osubformula , for both , contains the result of replacing in that osubformula by .
- •
Whenever has a semisurface osubformula E\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptG, contains the result of replacing in that osubformula by .
Rule :
, where is the result of replacing in a semisurface osubformula by or .
Rule (\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt):
, where is the result of replacing in a semisurface osubformula E\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0ptG by .
Rule :
, where is the result of replacing in two—one positive and one negative—semisurface occurrences of some general atom by an extralogical elementary atom which does not occur in .
A proof (in CL13) of a formula is a sequence of formulas ending in such that every formula follows from some (possibly empty) set of earlier formulas by one of the rules of the system.
Example 7.5
Pick any two distinct connectives and from the list \wedge,\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt,\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt,\sqcap. Then CL13 proves the formula if and only if is to the left of in the list. Similarly for the list \sqcup,\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt,\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt},\vee. Here we verify this fact only for the case \{\&_{1},\&_{2}\}=\{\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt,\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt\}. The reader may want to try some other combinations as exercises. Below is a proof of P\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptQ\rightarrow P\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptQ together with step justifications:
From no premises by (\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt). 2. 2.
(\neg p\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\bot)\vee p From 1 by (\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}) 3. 3.
From no premises by (\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt) 4. 4.
(\neg p\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\neg q)\vee q From 3 by (\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}) 5. 5.
(\neg p\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\neg Q)\vee Q From 4 by (M) 6. 6.
(\neg p\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\neg Q)\vee(p\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptQ) From 2,5 by (\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt\sqcap) 7. 7.
(\neg P\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\neg Q)\vee(P\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptQ) From 6 by (M)
On the other hand, the formula P\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0ptQ\rightarrow P\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptQ, i.e. (\neg P\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt\neg Q)\vee(P\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptQ), has no proof in CL13. This can be shown through attempting and failing to construct, bottom-up, a purported proof of the formula. Here we explore one of the branches of a proof-search tree. (\neg P\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt\neg Q)\vee(P\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptQ) is not quasielementary, so it could not be derived by (be the conclusion of) the (\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}) or (\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt) rule. The rule does not apply either, as there is no in the formula. This leaves us with one of the rules (\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt), (\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt\sqcap) and (M). Let us see what happens if our target formula is derived by (\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt). In this case the premise should be \neg Q\vee(P\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptQ). The latter can be derived only by (\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt\sqcap) or (M). Again, let us try (M). The premise in this case should be \neg q\vee(P\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptq) for some elementary atom . But the only way \neg q\vee(P\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptq) can be derived is by (\hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt\sqcap) from the premise \neg q\vee(\bot\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0ptq). This formula, in turn, could only be derived by (\mbox{\hskip 2.0pt\wedge\raisebox{0.05692pt}{\rule{0.36989pt}{5.69054pt}}}\hskip 5.0pt), in which case is one of the premises. Now we are obviously stuck, as 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 7.6
-
Construct a proof of (P\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0ptP)\wedge(\neg P\hskip 3.0pt\mbox{\Large\triangleright}\hskip 3.0pt\neg P)\rightarrow P\sqsupset P.
-
For which of the four disjunctions \cup\in\{\vee,\sqcup,\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt,\mbox{\hskip 2.0pt\vee\raisebox{0.28453pt}{\rule{0.36989pt}{5.69054pt}}\hskip 5.0pt}\} are the following formulas provable and for which are not? (a) ; (b) ; (c) ; (d) .
Open Problem 7.7
-
Consider the first-order version of the language of CL13 with choice (to start with) quantifiers. Adequately axiomatize the set of logically valid formulas in this language.
-
Consider the set of the theorems of CL13 that do not contain extralogical elementary letters. Does this set remain complete with respect to extralogical validity?
7.3 The brute force system CL12
CL12-formulas—or just formulas in this subsection—are formulas of the language of CoL that do not contain any general gameframe letters, and do not contain any operators other than \neg,\wedge,\vee,\sqcap,\sqcup,\hskip 1.0pt\mbox{\Large\sqcap},\hskip 1.0pt\mbox{\Large\sqcup},\mbox{\large\forall},\mbox{\large\exists}. As in the preceding two sections, applied to formulas other than extralogical atoms is understood as the corresponding DeMorgan abbreviation, is understood as an abbreviation of , and as an abbreviation of .
CL12-sequents—or just sequents in this subsection—are expressions of the form E_{1},\cdots,E_{n}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF, where () and are CL12-formulas; for simplicity and safety, we require that no variable has both free and bound occurrences in the (not necessarily the same) formulas of the sequent. The sequence is said to be the antecedent of the sequent, and its succedent. Semantically, such a sequent is identified with the (non-CL12) formula E_{1}\wedge\cdots\wedge E_{n}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF. 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. Each CL12-formula , in turn, can be identified with the empty-antecedent sequent \hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF. A CL12-sequent is closed iff so is its succedent as well as all formulas of the antecedent. When applied to CL12, the word “sentence” in Theorem 7.1 should be interpreted as “closed CL12-sequent” rather than (merely) “closed CL12-formula”.
Note that the language of CL12 is an extension of the full language of classical first-order logic. Due to this fact, together with the presence of \sqcap,\sqcup,\hskip 1.0pt\mbox{\Large\sqcap},\hskip 1.0pt\mbox{\Large\sqcup},\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt in the language, CL12 is a very powerful tool for constructing CoL-based applied theories (see Section 8), and has been repeatedly [27, 30, 36, 37, 38, 39, 40, 41] used as such with significant advantages over the less expressive and computationally less meaningful classical logic. Below is some terminology employed in our axiomatization of CL12.
- •
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 of a formula is the result of replacing in all surface occurrences of - and -subformulas by , and all surface occurrences of - and -subformulas by . Note that is (indeed) an elementary formula. The elementarization \|E_{1},\cdots,E_{n}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF\| of a sequent E_{1},\cdots,E_{n}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF is the elementary formula .
- •
A sequent is said to be stable iff its elementarization is classically valid (i.e., provable in some standard version of classical first-order calculus with constants, function letters and ).
- •
We will be using the notation to mean a formula together with some fixed surface occurrence of a subformula . Using this notation sets a context, in which will mean the result of replacing in that occurrence of by .
- •
stand for finite sequences of formulas.
We now define CL12 by the following six rules of inference, where means “from premise(s) conclude ”. 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. In each rule, is assumed to be either [math] or , is either a constant or a variable with no bound occurrences in the premise, and is a variable not occurring in the conclusion; (resp. ) is the result of replacing in the formula all free occurrences of the variable by (resp. ).
-Choose:
\vec{G}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF[H_{i}]\ \Longrightarrow\ \vec{G}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF[H_{0}\sqcup H_{1}], for either .
-Choose:
\vec{G},E[H_{i}]\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF\Longrightarrow\ \vec{G},E[H_{0}\sqcap H_{1}]\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF, for either .
****-Choose:
\vec{G}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF\bigl{[}H(t)\bigr{]}\ \Longrightarrow\ \vec{G}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF\bigl{[}\hskip 1.0pt\mbox{\Large\sqcup}xH(x)\bigr{]}, for any .
****-Choose:
\vec{G},E\bigl{[}H(t)\bigr{]},\vec{K}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF\ \Longrightarrow\ \vec{G},E\bigl{[}\hskip 1.0pt\mbox{\Large\sqcap}xH(x)\bigr{]},\vec{K}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF, for any .
Replicate:
\vec{G},E,\vec{K},E\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF\ \Longrightarrow\ \vec{G},E,\vec{K}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF.
Wait:
(), where is stable and the following four conditions are satisfied:
- •
Whenever has the form \vec{K}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE[H_{0}\sqcap H_{1}], both \vec{K}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE[H_{0}] and \vec{K}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE[H_{1}] are among .
- •
Whenever has the form \vec{L},J[H_{0}\sqcup H_{1}],\vec{M}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE, both \vec{L},J[H_{0}],\vec{M}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE and \vec{L},J[H_{1}],\vec{M}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE are among .
- •
Whenever has the form \vec{K}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE\bigl{[}\hskip 1.0pt\mbox{\Large\sqcap}xH(x)\bigr{]}, for some , \vec{K}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE\bigl{[}H(y)\bigr{]} is among .
- •
Whenever has the form \vec{L},J\bigl{[}\hskip 1.0pt\mbox{\Large\sqcup}xH(x)\bigr{]},\vec{M}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE, for some , \vec{L},J\bigl{[}H(y)\bigr{]},\vec{M}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptE is among .
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 use the name “Replicate” for one of the rules rather than the more standard “Contraction”.
A proof (in CL12) of a sequent is a sequence of sequents, with , such that each follows by one of the rules of CL12 from some (possibly empty in the case of Wait, and certainly empty in the case of ) set of premises such that . A proof of a formula is understood as a proof of the empty-antecedent sequent \hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF.
Example 7.8
Here is a binary function letter and 3 is a unary function letter. We write and instead of and . The following sequence is a proof of its last sequent.
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},t=s\times s,r=t\times s\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptr=s^{3} Wait: (no premises)
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},t=s\times s,r=t\times s\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcup}y(y=s^{3}) -Choose: 1
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},t=s\times s,\hskip 1.0pt\mbox{\Large\sqcup}z(z=t\times s)\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcup}y(y=s^{3}) Wait: 2
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},t=s\times s,\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=t\times y)\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcup}y(y=s^{3}) -Choose: 3
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},t=s\times s,\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y)\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcup}y(y=s^{3}) -Choose: 4
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},\hskip 1.0pt\mbox{\Large\sqcup}z(z=s\times s),\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y)\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcup}y(y=s^{3}) Wait: 5
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=s\times y),\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y)\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcup}y(y=s^{3}) -Choose: 6
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y),\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y)\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcup}y(y=s^{3}) -Choose: 7
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y)\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcup}y(y=s^{3}) Replicate: 8
-
\mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)},\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y)\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{3}) Wait: 9
Exercise 7.9
To see the resource-consciousness of CL12, show that it does not prove , even though this formula has the form of a classical tautology. Then show that, in contrast, CL12 proves the sequent p\sqcap q\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0pt(p\sqcap q)\wedge(p\sqcap q) because, unlike the antecedent of a pimplication, the antecedent of a brimplication is reusable (trough Replicate).
For any closed sequent E_{1},\cdots,E_{n}\hskip 3.0pt\mbox{\circ \raisebox{-1.22343pt}{\Large--}}\hskip 3.0ptF, following holds due to the adequacy Theorem 7.1:
[TABLE]
This explains why we call the following rule of inference Logical Consequence:
[TABLE]
Logical Consequence is the only logical rule of inference in all CL12-based applied theories briefly discussed in Section 8. To appreciate the convenience that Thesis 6.5 offers when reasoning in such theories, let us look at the following example.
Example 7.10
Imagine a CL12-based applied formal theory, in which we have proven or postulated \mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)} (the meaning of “cube” in terms of multiplication) and \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y) (the computability of multiplication), and now we want to derive \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{3}) (the computability of “cube”). This is how we can reason to justify \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{3}):
Consider any (selected by the environment for in \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{3})). We need to find . Using the resource \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y) twice, we first find the value of , and then the value of . According to \mbox{\large\forall}x\bigl{(}x^{3}=(x\times x)\times x\bigr{)}, such an is the sought .
Thesis 6.5, in view of (4), promises that the above intuitive argument will be translatable into a proof of
[TABLE]
in CL12, and hence the succedent \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{3}) will be derivable in the theory by Logical Consequence as the formulas of the antecedent are already proven. Such a proof indeed exists—see Example 7.8.
Open Problem 7.11
-
Add the sequential connectives \hskip 2.0pt\mbox{\small\raisebox{0.0pt}{\bigtriangleup}}\hskip 2.0pt,\hskip 2.0pt\mbox{\small\raisebox{1.39406pt}{\bigtriangledown}}\hskip 2.0pt to the language of CL12 and adequately axiomatize the corresponding logic.
-
Axiomatize (if possible) the set of extralogically valid CL12-sequents.
-
Along with elementary gameframe letters, allow also general gameframe letters in the language of CL12, and axiomatize (if possible) the set of valid sequents of this extended language.
8 Applied systems based on computability logic
The main utility of CoL, actual or potential, is related to the benefits of using it as a logical basis for applied systems, such as axiomatic theories or knowledgebase systems.
The most common logical basis for applied systems is classical first-order logic (CFOL). This is due to the fact that CFOL is universal: its language allows one to say anything one could say, and its proof system allows one to justify anything one could justify logically. But when it comes to expressing tasks (as opposed to facts) and reasoning about them, such as the task/problem expressed by \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{2}), using CFOL can be an extremely circuitous and awkward way. Asking why we need CoL if everything can be done with CFOL is akin to asking, for instance, why we study modal logics if anything one can express or reason about in modal logic can just as well be expressed or reasoned about using CFOL.
For specificity, let us imagine what a typical applied system based on the already axiomatized fragment CL12 of CoL would look like. The construction of such a system would start from building its extralogical basis , with some fixed interpretation ∗ in mind. In what follows, for readability, we omit explicit references to this ∗ and, terminologically, identify each sentence with the game . Depending on the context or traditions, would generally be referred to as the knowledgebase, or the set of axioms, of . It would be a collection of relevant (to the purposes of the system) sentences expressing computational problems with already known, fixed solutions. Those can be atomic elementary sentences expressing true facts such as or ; nonatomic elementary sentences expressing general or conceptual knowledge such as \mbox{\large\forall}x\mbox{\large\forall}y\bigl{(}y=MotherOf(x)\rightarrow Female(y)\bigr{)} or \mbox{\large\forall}x(x^{2}=x\times x); nonatomic nonelementary sentences such as \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y\bigl{(}y=DateOfBirth(x)\bigr{)} expressing the ability to tell any person’s date of birth (perhaps due to having access to an external database), \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\hskip 1.0pt\mbox{\Large\sqcup}z(z=x\times y) expressing the ability to compute multiplication, or \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\bigl{(}\neg\mbox{\em Halts}(x,y)\sqcup\mbox{\em Halts}(x,y)\bigr{)}\rightarrow\hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcap}y\bigl{(}\neg\mbox{\em Accepts}(x,y)\sqcup\mbox{\em Accepts}(x,y)\bigr{)} expressing the ability to reduce the acceptance problem to the halting problem. The only logical rule of inference in would be Logical Consequence defined in Section 7.3.
A proof of a sentence in such a system will be defined in a standard way, with the elements of acting as axioms. The rule of Logical Consequence preserves computability in the sense that, as long as all sentences of the antecedent of a CL12-sequent are computable under a given interpretation, so is the succedent and, furthermore, a solution of the latter can be extracted from solutions of the sentences of the antecedent. Since solutions of all axioms are already known, thus automatically translates into a solution of . Think of as a declarative programming language, as a program written in that language, the sentence as a specification of (the goal of) such a program, the mechanism extracting solutions from proofs as a compiler, and the above as a machine-language-level translation of the high-level program . Note that the notoriously hard problem of program verification is fully neutralized in this paradigm: being a proof of the sentence , automatically also serves as a formal verification of the fact that the program meets its specification . Further, is a program commented in an extreme sense, with every line/sentence in this program being its own, best possible, comment.
A relevant question, of course, is how efficient the above solution would be in terms of computational complexity. Here come more pieces of positive news. The traditional complexity-theoretic concepts such as time or space complexities find in CoL natural and conservative generalizations from the traditional sorts of problems to all games (cf. [37]). The Logical Consequence rule is complexity-theoretically well behaved, with the time (resp. space) complexity of its conclusion guaranteed to be at most linearly (resp. logarithmically) different from the time (resp. space) complexities of the solutions of the premises. So, how efficient the solutions extracted from proofs in are, is eventually determined by how efficient the solutions of the axioms comprising are. If, for instance, all axioms have linear time and/or logarithmic space solutions, then so do all theorems of as well.
In some cases, the extralogical postulates of would consist of not only the axioms , but also certain extralogical rules of inference such as some versions of induction or comprehension. Depending on the version, such a rule may less closely preserve computational complexity than Logical Consequence does. For instance, each application of induction may increase the time complexity quadratically rather than linearly. By limiting the number of such applications or imposing certain other restrictions, we can still get a system all of whose theorems are problems with low-order polynomial time complexities as long as all axioms are so.
By now CoL has found applications in a series CLA1-CLA11 of formal number theories dubbed “clarithmetics”. All of these theories are based on CL12, and differ between each other only in their extralogical postulates. The language of each theory has the same extralogical vocabulary (where means “the successor of ”) as the language of first-order Peano arithmetic. Unlike other approaches with similar aspirations such as that of bounded arithmetic [7], this approach avoids a need for adding more extralogical primitives to the language as, due to extending rather than restricting traditional Peano arithmetic, all arithmetical functions or predicates remain expressible in standard ways. The extralogical postulates of clarithmetical systems are also remarkably simple, with their sets of axioms consisting of all axioms of Peano arithmetic plus the single nonelementary sentence \hskip 1.0pt\mbox{\Large\sqcap}x\hskip 1.0pt\mbox{\Large\sqcup}y(y=x^{\prime}) or just a few similarly innocuous-looking axioms, and the set of extralogical inference rules consisting of induction and perhaps one more rule such as comprehension. Different clarithmetics serve different computational complexity classes, which explains their multiplicity. Each system has been proven to be sound and complete with respect to its target complexity class . Sound in the sense that every theorem of the system expresses an arithmetical problem with a complexity solution and, furthermore, such a solution can be automatically obtained from the proof of . And complete in the sense that every arithmetical problem with a complexity solution is expressed by some theorem of the system. Furthermore, if one adds all true sentences of Peano arithmetic to the set of axioms, then this extensional completeness result strengthens to intensional completeness, according to which every (rather than just some) sentence expressing such an is a theorem of the system.
Among CLA1-CLA11, the system CLA11 stands out in that it is a scheme of clarithmetical theories rather than a particular theory, taking three parameters and correspondingly written as CLA11. These parameters range over sets of terms or pseudoterms used as bounds for \hskip 1.0pt\mbox{\Large\sqcap},\hskip 1.0pt\mbox{\Large\sqcup} in certain postulates. determines the time complexity of all theorems of the system, determines space complexity and the so called amplitude complexity (the complexity measure concerned with the sizes of ’s moves relative to the sizes of ’s moves). By tuning these three parameters in an essentially mechanical, brute force fashion, one immediately gets a system sound and complete with respect to one or another combination of time, space and amplitude complexities. For instance, for Linear amplitude + Logarithmic space + Polynomial time, it is sufficient to choose to be the canonical set of terms expressing all linear functions (i.e. terms built from variables, [math], and ′), the canonical set of terms for all polynomial functions (namely, terms built from variables, [math], , and ′), and the set of canonical pseudoterms for all logarithmic functions. This way one can obtain a system for essentially all natural (whatever this means) combinations of time, space and amplitude complexities. See the introductory section of [39] for a more detailed account.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Samson Abramsky, Radha Jagadeesan Games and full completeness of multiplicative linear logic , The Journal of Symbolic Logic 59 (2) 1994, pp. 543-574.
- 2[2] Arnon Avron A constructive analysis of RM , The Journal of Symbolic Logic 52 (4) 1987, pp. 939-951.
- 3[3] Matthew Bauer A PSPACE-complete first order fragment of computability logic , ACM Transactions on Computational Logic 15 (1:1), 2014, pp. 1-12.
- 4[4] Matthew Bauer The computational complexity of propositional cirquent calculus , Logical Methods is Computer Science 11 (1:12), 2015, pp. 1-16.
- 5[5] Andreas Blass Degrees of indeterminacy of games , Fundamenta Mathematicae 77 (2), 1972, pp. 151-166.
- 6[6] Andreas Blass A game semantics for linear logic , Annals of Pure and Applied Logic 56 , (1-3) 1992, pp. 183-220.
- 7[7] Samuel Buss Bounded Arithmetic , Bibliopolis, Naples 1986. (Revised version of Ph D thesis.)
- 8[8] Alonzo Church An unsolvable problem of elementary number theory , American Journal of Mathematics 58 (2), 1936, pp. 345-363.