Computability logic
CoL defines a computational problem as a game played by a machine against its environment.
Such a problem is computable if there is a machine that wins the game against every possible behavior of the environment.
The classical concept of truth turns out to be a special, zero-interactivity-degree case of computability.
Out of these, only applications in constructive applied theories have been extensively explored so far: a series of CoL-based number theories, termed "clarithmetics", have been constructed[4][5] as computationally and complexity-theoretically meaningful alternatives to the classical-logic-based first-order Peano arithmetic and its variations such as systems of bounded arithmetic.
Traditional proof systems such as natural deduction and sequent calculus are insufficient for axiomatizing nontrivial fragments of CoL.
This has necessitated developing alternative, more general and flexible methods of proof, such as cirquent calculus.
Its logical vocabulary has several sorts of conjunctions, disjunctions, quantifiers, implications, negations and so called recurrence operators.
Japaridze has repeatedly pointed out that the language of CoL is open-ended, and may undergo further extensions.
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.
The blind quantifiers ∀ ("blall") and ∃ ("blexists"), on the other hand, generate single-board games.
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.
The sequential disjunction ("sor") Aᐁ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 sequential ("srecurrence") and toggling ("trecurrence") sorts of recurrences can be defined similarly.
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.
Branching corecurrence ("cobrecurrence") ⫯ is defined symmetrically by interchanging "machine" and "environment".
The language of CoL offers a systematic way to specify an infinite variety of computational problems, with or without names established in the literature.
Imposing time or space restrictions on the work of the machine, one further gets complexity-theoretic counterparts of such relations and operations.
Typically it also has one or two non-logical rules of inference, such as constructive versions of induction or comprehension.
Through routine variations in such rules one can obtain sound and complete systems characterizing one or another interactive computational complexity class C. This is in the sense that a problem belongs to C if and only if it has a proof in the theory.
Their notable distinguishing feature from other approaches with similar aspirations (such as bounded arithmetic) is that they extend rather than weaken PA, preserving the full deductive power and convenience of the latter.
