User:Anaszt5/sandbox

Bounded arithmetic

Bounded arithmetic is a collective name for a family of weak subtheories of Peano arithmetic. Such theories are typically obtained by requiring that quantifiers be bounded in the induction axiom or equivalent postulates (a bounded quantifier is of the form ∀x ≤ t or ∃x ≤ t, where t is a term not containing x). The main purpose is to characterize one or another class of computational complexity in the sense that a function is provably total if and only if it belongs to a given complexity class.

The approach was initiated by Rohit Jivanlal Parikh in 1971, and later developed by Samuel Buss and a number of other logicians.

References added to Computability logic, October 7, 2016

• M. Bauer, A PSPACE-complete first order fragment of computability logic. ACM Transactions on Computational Logic 15 (2014), No 1, Article 1, 12 pages.
• M. Bauer, The computational complexity of propositional cirquent calculus. Logical Methods is Computer Science 11 (2015), Issue 1, Paper 12, pages 1-16.

• G. Japaridze, Toggling operators in computability logic. Theoretical Computer Science 412 (2011), pp.  971-1004. Prepublication
• G. Japaridze, From formulas to cirquents in computability logic. Logical Methods in Computer Science 7 (2011), Issue 2 , Paper 1, pp. 1-55.
• G. Japaridze, Introduction to clarithmetic I. Information and Computation 209 (2011), pp. 1312-1354. Prepublication
• G. Japaridze, Separating the basic logics of the basic recurrences. Annals of Pure and Applied Logic 163 (2012), pp. 377-389. Prepublication
• G. Japaridze, A logical basis for constructive systems. Journal of Logic and Computation 22 (2012), pp. 605-642.
• G. Japaridze, A new face of the branching recurrence of computability logic. Applied Mathematics Letters 25 (2012),  1585-1589. Prepublication
• G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part I. Archive for Mathematical Logic 52 (2013), pp. 173-212. Prepublication
• G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part II. Archive for Mathematical Logic 52 (2013), pp. 213-259. Prepublication
• G. Japaridze, Introduction to clarithmetic III. Annals of Pure and Applied Logic 165 (2014),  241-252. Prepublication
• G. Japaridze, On the system CL12 of computability logic . Logical Methods is Computer Science 11 (2015), Issue 3, paper 1, pp. 1-71.
• G. Japaridze, Introduction to clarithmetic II. Information and Computation 247 (2016), pp. 290-312.
• G. Japaridze, Build your own clarithmetic I: Setup and completeness. Logical Methods is Computer Science 12 (2016), Issue 3, paper 8, pp. 1-59.
• G. Japaridze, Build your own clarithmetic II: Soundness. Logical Methods is Computer Science 12 (2016), Issue 3, paper 12, pp. 1-62.
• K. Kwon, Expressing algorithms as concise as possible via computability logic. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, v. E97-A (2014), pp. 1385-1387.
• X. Li and J. Liu, Research on decidability of CoL2 in computability logic. Computer Science 42 (2015), No 7, pp. 44-46.
• I. Mezhirov and N. Vereshchagin, On abstract resource semantics and computability logic. Journal of Computer and System Sciences 76 (2010), pp. 356–372.
• M. Qu, J. Luan, D. Zhu and M. Du, On the toggling-branching recurrence of computability logic. Journal of Computer Science and Technology 28 (2013), pp. 278-284.
• N. Vereshchagin, Japaridze's computability logic and intuitionistic propositional calculus. Moscow State University, 2006.
• W. Xu and S. Liu, The countable versus uncountable branching recurrences in computability logic. Journal of Applied Logic 10 (2012), pp. 431-446.
• W. Xu and S. Liu, Soundness and completeness of the cirquent calculus system CL6 for computability logic. Logic Journal of the IGPL 20 (2012), pp. 317-330.
• W. Xu and S. Liu, The parallel versus branching recurrences in computability logic. Notre Dame Journal of Formal Logic 54 (2013), pp. 61-78.
• W. Xu, A propositional system induced by Japaridze’s approach to IF logic. Logic Journal of the IGPL 22 (2014), pp. 982-991
• W. Xu, A cirquent calculus system with clustering and ranking. Journal of Applied Logic 16 (2016), pp. 37-49.

Language

Operators of computability logic: names, symbols and readings

The full language of CoL is an extension of the language of classical first-order logic. Its logical vocabulary has several sorts of conjunctions, disjunctions, quantifiers, implications, negations and so called recurrence operators. This collection includes all connectives and quantifiers of classical logic. The language also has two sorts of nonlogical atoms: elementary and general. Elementary atoms, which are nothing but the atoms of classical logic, represent elementary problems, i.e., games with no moves that are automatically won by the machine when true and lost when false. General atoms, on the other hand, can be interpreted as any games, elementary or non-elementary. Both semantically and syntactically, classical logic is nothing but the fragment of CoL obtained by forbidding general atoms in its language, and forbidding all operators other than ¬, ∧, ∨, →, ∀, ∃.

Japaridze has repeatedly pointed out that the language of CoL is open-ended, and may undergo further extensions. Due to the expressiveness of this language, advances in CoL, such as constructing axiomatizations or building CoL-based applied theories, have usually been limited to one or another proper fragment of the language.

Semantics

The games underlying the semantics of CoL are called "static games". Such games impose no regulations on which player can or should move in a given situation, and it is generally up to the player to decide whether to move or wait for moves by its adversary. It is always a possibility that the adversary moves while a given player is "thinking" on its next step. However, static games are defined in such a way that it never hurts a player to delay 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 {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 (resp. A∨B) if it wins both (resp. at least one) of those. So, for instance, 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 ∧ ("pall") and ∨ ("pexists") can be defined by ∧xA(x) = A(0)∧A(1)∧A(2)∧... and ∨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 ∧xA(x) (resp. ∨xA(x)) if it wins all (resp. some) of these games. 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) (resp. ∃xA(x)) if such a run is a won run of A(x) for all (resp. at least one) possible values of x.

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ᐁ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 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.

Then comes the recurrence group of operators. 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 corresponding corecurrence operators, on the other hand, can be defined as infinite disjunctions instead. Branching recurrence ("brecurrence") ⫰, which is the strongest sort of recurrence, does not have a corresponding conjunction. ⫰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 ⫰A. Branching corecurrence ("cobrecurrence") ⫯ 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⟜B is nothing but ⫰A→B, and the branching refutation ("brefutation") of A is A⟜⊥, where ⊥ is the always-lost elementary game. Similarly for all other sorts of rimplication and refutation.

CoL 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 ⊓x⊔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 ⊔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 predicate. Then ⊓x(p(x)⊔¬p(x)) expresses the problem of deciding p, ⊓x(p(x)&ᐁ¬p(x)) expresses the problem of semidieciding p, and ⊓x(p(x)⩛¬p(x)) the problem of recursively approximating p.

Let p and q be two unary predicates. Then ⊓x(p(x)⊔¬p(x))⟜⊓x(q(x)⊔¬q(x)) expresses the problem of Turing-reducing q to p (in the sense that q is Turing reducible to p if and only if the interactive problem ⊓x(p(x)⊔¬p(x))⟜⊓x(q(x)⊔¬q(x)) is computable). ⊓x(p(x)⊔¬p(x))→⊓x(q(x)⊔¬q(x)) does the same but for the stronger version of Turing reduction where the oracle for p can be queried only once. ⊓x⊔y(q(x)↔p(y)) does the same for the problem of 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.

CoL as a problem solving tool

The known deductive systems for various fragments of CoL share the property that a solution (algorithm) can be automatically extracted from a proof of a problem in the system. This property is further inherited by all applied theories based on those systems. So, in order to find a solution for a given problem, it is sufficient to express it in the language of CoL and then find a proof of that expression. Another way to look at this phenomenon is to think of a formula G of CoL as program specification (goal). Then a proof of G is - more precisely, translates into - a program meeting that specification. There is no need to verify that the specification is met, because the proof itself is, in fact, such a verification.

Examples of CoL-based applied theories are the so called clarithmetics. These are number theories based on CoL in the same sense as Peano arithmetic PA is based on classical logic. Such a system is usually a conservative extension of PA. It typically includes all Peano axioms, and adds to them one or two extra-Peano axioms such as ⊓x⊔y(y=x') expressing the computability of the successor function. 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. So, such a theory can be used for finding not merely algorithmic solutions, but also efficient ones on demand, such as solutions that run in polynomial time or logarithmic space. It should be pointed out that all claritmetical theories share the same logical postulates, and only their non-logical postulates vary depending on the target complexity class. 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.