Editing Computability logic (section)

==As a problem specification tool== 
The language of CoL offers a systematic way to specify an infinite variety of computational problems, with or without names established in the literature. Below are some examples. 

Let ''f'' be a [[unary function]]. The problem of computing ''f'' will be written as <big><big>⊓</big></big>x<big><big>⊔</big></big>y(''y''=''f''(''x'')). According to the semantics of CoL, this is a game where the first move ("input") is by the environment, which should choose a value ''m'' for ''x''. Intuitively, this amounts to asking the machine to tell the value of ''f''(''m''). The game continues as <big><big>⊔</big></big>y(''y''=''f''(''m'')). Now the machine is expected to make a move ("output"), which should be choosing a value ''n'' for ''y''. This amounts to saying that ''n'' is the value of ''f''(m). The game is now brought down to the elementary ''n''=''f''(''m''), which is won by the machine if and only if ''n'' is indeed the value of ''f''(''m''). 

Let ''p'' be a unary [[Boolean-valued function|predicate]]. Then <big><big>⊓</big></big>''x''(''p''(''x'')⊔¬''p''(''x'')) expresses the problem of [[Decidability (logic)|deciding]] ''p'', <big><big>⊓</big></big>''x''(''p''(''x'')&<small>ᐁ</small>¬''p''(''x'')) expresses the problem of [[Recursively enumerable set|semideciding]] ''p'', and <big><big>⊓</big></big>''x''(''p''(''x'')⩛¬''p''(''x'')) the problem of [[Computation in the limit|recursively approximating]] ''p''. 

Let ''p'' and ''q'' be two unary predicates. Then  <big><big>⊓</big></big>''x''(''p''(''x'')⊔¬''p''(''x''))<big>⟜</big><big><big>⊓</big></big>''x''(''q''(''x'')⊔¬''q''(''x'')) expresses the problem of [[Turing reduction|Turing-reducing]] ''q'' to ''p'' (in the sense that ''q'' is Turing reducible to ''p'' if and only if the interactive problem  <big><big>⊓</big></big>''x''(''p''(''x'')⊔¬''p''(''x''))<big>⟜</big><big><big>⊓</big></big>''x''(''q''(''x'')⊔¬''q''(''x'')) is computable).   <big><big>⊓</big></big>''x''(''p''(''x'')⊔¬''p''(''x''))<big>→</big><big><big>⊓</big></big>''x''(''q''(''x'')⊔¬''q''(''x'')) does the same but for the stronger version of Turing reduction where the [[oracle machine|oracle]] for ''p'' can be queried only once. <big><big>⊓</big></big>x<big><big>⊔</big></big>''y''(''q''(''x'')↔''p''(''y'')) does the same for the problem of [[Many-one reduction|many-one reducing]] ''q'' to ''p''. With more complex expressions one can capture all kinds of nameless yet potentially meaningful relations and operations on computational problems, such as, for instance, "Turing-reducing the problem of semideciding ''r'' to the problem of many-one reducing ''q'' to ''p''". Imposing time or space restrictions on the work of the machine, one further gets complexity-theoretic counterparts of such relations and operations.