Computability logic (CoL) is a research program and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic, which is a formal theory of truth. It was introduced and so named by Giorgi Japaridze in 2003.[1]
In classical logic, formulas represent true/false statements. In CoL, formulas represent computational problems. In classical logic, the validity of a formula depends only on its form, not on its meaning. In CoL, validity means being always computable. More generally, classical logic tells us when the truth of a given statement always follows from the truth of a given set of other statements. Similarly, CoL tells us when the computability of a given problem A always follows from the computability of other given problems B1,...,Bn. Moreover, it provides a uniform way to actually construct a solution (algorithm) for such an A from any known solutions of B1,...,Bn.
CoL formulates computational problems in their most general—interactive—sense. 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. Such a game-playing machine generalizes the Church–Turing thesis to the interactive level. The classical concept of truth turns out to be a special, zero-interactivity-degree case of computability. This makes classical logic a special fragment of CoL. Thus CoL is a conservative extension of classical logic. Computability logic is more expressive, constructive and computationally meaningful than classical logic. Besides classical logic, independence-friendly (IF) logic and certain proper extensions of linear logic and intuitionistic logic also turn out to be natural fragments of CoL.[2][3] Hence meaningful concepts of "intuitionistic truth", "linear-logic truth" and "IF-logic truth" can be derived from the semantics of CoL.
CoL systematically answers the fundamental question of what can be computed and how; thus CoL has many applications, such as constructive applied theories, knowledge base systems, systems for planning and action. 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.[6][7]
Language
Operators of computability logic: names, symbols and readings
The full language of CoL extends 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 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 reducingB 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) if it wins all of these games, and ∨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ᐁ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") ⫰, 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.
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 and q be two unary predicates. Then ⊓x(p(x)⊔¬p(x))⟜⊓x(q(x)⊔¬q(x)) expresses the problem of Turing-reducingq 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 reducingq 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.
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 first-order 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 clarithmetical 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.
In logic, disjunction, also known as logical disjunction or logical or or logical addition or inclusive disjunction, is a logical connective typically notated as and read aloud as "or". For instance, the English language sentence "it is sunny or it is warm" can be represented in logic using the disjunctive formula , assuming that abbreviates "it is sunny" and abbreviates "it is warm".
In logic, a logical connective is a logical constant. Connectives can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary connective can be used to join the two atomic formulas and , rendering the complex formula .
In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathematician. The rules allow the expression of conjunctions and disjunctions purely in terms of each other via negation.
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.
Modal logic is a kind of logic used to represent statements about necessity and possibility. It plays a major role in philosophy and related fields as a tool for understanding concepts such as knowledge, obligation, and causation. For instance, in epistemic modal logic, the formula can be used to represent the statement that is known. In deontic modal logic, that same formula can represent that is a moral obligation.
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics, as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.
Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes.
In computer science, interactive computation is a mathematical model for computation that involves input/output communication with the external world during computation.
Default logic is a non-monotonic logic proposed by Raymond Reiter to formalize reasoning with default assumptions.
Datalog is a declarative logic programming language. While it is syntactically a subset of Prolog, Datalog generally uses a bottom-up rather than top-down evaluation model. This difference yields significantly different behavior and properties from Prolog. It is often used as a query language for deductive databases. Datalog has been applied to problems in data integration, networking, program analysis, and more.
Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.
Finite model theory is a subarea of model theory. Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory to interpretations on finite structures, which have a finite universe.
Giorgi Japaridze is a Georgian-American researcher in logic and theoretical computer science. He currently holds the title of Full Professor at the Computing Sciences Department of Villanova University. Japaridze is best known for his invention of computability logic, cirquent calculus, and Japaridze's polymodal logic.
Logics for computability are formulations of logic that capture some aspect of computability as a basic notion. This usually involves a mix of special logical connectives as well as a semantics that explains how the logic is to be interpreted in a computational way.
The concept of a stable model, or answer set, is used to define a declarative semantics for logic programs with negation as failure. This is one of several standard approaches to the meaning of negation in logic programming, along with program completion and the well-founded semantics. The stable model semantics is the basis of answer set programming.
Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.
Dialogical logic was conceived as a pragmatic approach to the semantics of logic that resorts to concepts of game theory such as "winning a play" and that of "winning strategy".
Vector logic is an algebraic model of elementary logic based on matrix algebra. Vector logic assumes that the truth values map on vectors, and that the monadic and dyadic operations are executed by matrix operators. "Vector logic" has also been used to refer to the representation of classical propositional logic as a vector space, in which the unit vectors are propositional variables. Predicate logic can be represented as a vector space of the same type in which the axes represent the predicate letters and . In the vector space for propositional logic the origin represents the false, F, and the infinite periphery represents the true, T, whereas in the space for predicate logic the origin represents "nothing" and the periphery represents the flight from nothing, or "something".
Japaridze's polymodal logic (GLP) is a system of provability logic with infinitely many provability modalities. This system has played an important role in some applications of provability algebras in proof theory, and has been extensively studied since the late 1980s. It is named after Giorgi Japaridze.
Cirquent calculus is a proof calculus that manipulates graph-style constructs termed cirquents, as opposed to the traditional tree-style objects such as formulas or sequents. Cirquents come in a variety of forms, but they all share one main characteristic feature, making them different from the more traditional objects of syntactic manipulation. This feature is the ability to explicitly account for possible sharing of subcomponents between different components. For instance, it is possible to write an expression where two subexpressions F and E, while neither one is a subexpression of the other, still have a common occurrence of a subexpression G.
↑ G. Japaridze, In the beginning was game semantics?. Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp.249–350. doi:10.1007/978-1-4020-9374-6_11Prepublication
↑ G. Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), pages 187–227. doi:10.1016/j.apal.2007.05.001
This page is based on this Wikipedia article Text is available under the CC BY-SA 4.0 license; additional terms may apply. Images, videos and audio are available under their respective licenses.
