Editing Computability logic (section)

==Semantics== 
The games underlying the semantics of CoL are called ''static games''. Such games have no turn order; a player can always move while the other players are "thinking". However, static games never punishes a player for "thinking" too long (delaying its own moves), so such games never become contests of speed. All elementary games are automatically static, and so are the games allowed to be interpretations of general atoms.

There are two players in static games: the ''machine'' and the ''environment''. The machine can only follow algorithmic strategies, while there are no restrictions on the behavior of the environment. Each run (play) is won by one of these players and lost by the other.

The logical operators of CoL are understood as operations on games. Here we informally survey some of those operations. For simplicity we assume that the domain of discourse is always the set of all natural numbers: {0,1,2,...}. 

The operation ¬ of ''negation'' ("not") switches the roles of the two players, turning moves and wins by the machine into those by the environment, and vice versa. For instance, if ''Chess'' is the game of chess (but with ties ruled out) from the white player's perspective, then ¬''Chess'' is the same game from the black player's perspective. 

The ''parallel conjunction'' ∧ ("pand")  and ''parallel disjunction'' ∨ ("por") combine games in a parallel fashion. A run of ''A''∧''B'' or ''A''∨''B'' is a simultaneous play in the two conjuncts. The machine wins ''A''∧''B'' if it wins both of them. The machine wins ''A''∨''B'' if it wins at least one of them. For example, ''Chess''∨¬''Chess'' is a game on two boards, one played white and one black, and where the task of the machine is to win on at least one board. Such a game can be easily won regardless who the adversary is, by copying his moves from one board to the other.

The ''parallel implication'' operator → ("pimplication") is defined by ''A''→''B'' = ¬''A''∨''B''. The intuitive meaning of this operation is ''reducing'' ''B'' to ''A'', i.e., solving ''A'' as long as the adversary solves ''B''.

The ''parallel quantifiers'' <big><big>∧</big></big> ("pall") and <big><big>∨</big></big> ("pexists") can be defined by <big><big>∧</big></big>''xA''(''x'') = ''A''(0)∧''A''(1)∧''A''(2)∧...  and  <big><big>∨</big></big>''xA''(''x'') = ''A''(0)∨''A''(1)∨''A''(2)∨.... These are thus simultaneous plays of ''A''(0),''A''(1),''A''(2),..., each on a separate board. The machine wins <big><big>∧</big></big>''xA''(''x'') if it wins all of these games, and <big><big>∨</big></big>''xA''(''x'') if it wins some.

The ''blind quantifiers'' ∀ ("blall") and ∃ ("blexists"), on the other hand, generate single-board games. A run of ∀''xA''(''x'') or ∃''xA''(''x'') is a single run of ''A''. The machine wins ∀''xA''(''x'') (respectively ∃''xA''(''x'')) if such a run is a won run of ''A''(''x'') for all (respectively at least one) possible values of ''x'', and wins ∃''xA''(''x'') if this is true for at least one. 

All of the operators characterized so far behave exactly like their classical counterparts when they are applied to elementary (moveless) games, and validate the same principles. This is why CoL uses the same symbols for those operators as classical logic does. When such operators are applied to non-elementary games, however, their behavior is no longer classical. So, for instance, if ''p'' is an elementary atom and ''P'' a general atom, ''p''→''p''∧''p'' is valid while ''P''→''P''∧''P'' is not. The principle of the excluded middle ''P''∨¬''P'', however, remains valid. The same principle is invalid with all three other sorts (choice, sequential and toggling) of disjunction.

The ''choice disjunction''  ⊔ ("chor") of games ''A'' and ''B'', written ''A''⊔''B'', is a game where, in order to win, the machine has to choose one of the two disjuncts and then win in the chosen component. The ''sequential disjunction'' ("sor") ''A''<small>ᐁ</small>''B'' starts as ''A''; it also ends as ''A'' unless the machine makes a "switch" move, in which case ''A'' is abandoned and the game restarts and continues as ''B''. In the ''toggling disjunction'' ("tor") ''A''⩛''B'', the machine may switch between ''A'' and ''B'' any finite number of times. Each disjunction operator has its dual conjunction, obtained by interchanging the roles of the two players. The corresponding quantifiers can further be defined as infinite conjunctions or disjunctions in the same way as in the case of the parallel quantifiers. Each sort of disjunction also induces a corresponding implication operation the same way as this was the case with the parallel implication →. For instance, the ''choice implication'' ("chimplication") ''A''⊐''B'' is defined as ¬''A''⊔''B''. 

The ''parallel recurrence'' ("precurrence") of ''A'' can be defined as the infinite parallel conjunction ''A''∧A∧A∧... The sequential ("srecurrence") and toggling ("trecurrence") sorts of recurrences can be defined similarly.

The ''corecurrence'' operators can be defined as infinite disjunctions. ''Branching recurrence'' ("brecurrence") <big>⫰</big>, which is the strongest sort of recurrence, does not have a corresponding conjunction. <big>⫰</big>''A'' is a game that starts and proceeds as ''A''. At any time, however, the environment is allowed to make a "replicative" move, which creates two copies of the then-current position of ''A'', thus splitting the play into two parallel threads with a common past but possibly different future developments. In the same fashion, the environment can further replicate any of positions of any thread, thus creating more and more threads of ''A''. Those threads are played in parallel, and the machine needs to win ''A'' in all threads to be the winner in <big>⫰</big>''A''. ''Branching corecurrence'' ("cobrecurrence") <big>⫯</big> is defined symmetrically by interchanging "machine" and "environment". 

Each sort of recurrence further induces a corresponding weak version of implication and weak version of negation. The former is said to be a ''rimplication'', and the latter a ''refutation''. The ''branching rimplication'' ("brimplication") ''A''<big>⟜</big>''B'' is nothing but <big>⫰</big>''A''→''B'', and the ''branching refutation'' ("brefutation") of ''A'' is ''A''<big>⟜</big>⊥, where ⊥ is the always-lost elementary game. Similarly for all other sorts of rimplication and refutation.