Giorgi Japaridze
Encyclopedia
Giorgi Japaridze is a logician, at Villanova University
in Villanova, Pennsylvania
. In the past his contributions were primarily into the areas of provability logic
and interpretability logic
. Currently he is best known for his work on computability logic
(CL).
Technically CL is a game logic: it understands interactive computational problems as games played by a machine against the environment, their computability as existence of a machine that always wins the game, logical operators as operations on computational problems, and validity
of a logical formula as being a scheme of "always computable" problems.
Classical logic
, intuitionistic logic
, and linear logic
(in a broad sense), turn out to be three natural fragments of CL.
The classical concept of truth is a special case of computability, – computability restricted to problems of zero interactivity degree. Correspondingly, classical logic is a special fragment of CL. One of the main intuitions associated with intuitionistic logic is that it must be a logic of problems (Kolmogorov 1932); this is exactly what CL is, but in a more expressive language than intuitionistic logic. And one of the main claims of linear logic is that it is a logic of resources. Reversing of the roles of the machine and its environment turns computational problems into computational resources, which makes CL a logic of resources, only, again, in a more expressive language than that of linear logic, and based on an intuitively convincing and mathematically strict resource semantics.
Villanova University
Villanova University is a private university located in Radnor Township, a suburb northwest of Philadelphia, Pennsylvania, in the United States...
in Villanova, Pennsylvania
Villanova, Pennsylvania
Villanova is a community in the United States Commonwealth of Pennsylvania. It straddles Lower Merion Township of Montgomery County and Radnor Township of Delaware County. It is located at the center of the Pennsylvania Main Line, a series of highly affluent Philadelphia suburban towns located...
. In the past his contributions were primarily into the areas of provability logic
Provability logic
Provability logic is a modal logic, in which the box operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic....
and interpretability logic
Interpretability logic
Interpretability logics comprise a family of modal logics that extend provability logic to describe interpretability and/or various related metamathematical properties and relations such as weak interpretability, Π1-conservativity, cointerpretability, tolerance, cotolerance and arithmetic...
. Currently he is best known for his work on computability logic
Computability logic
Introduced by Giorgi Japaridze in 2003, computability logic is a research programme 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...
(CL).
Technically CL is a game logic: it understands interactive computational problems as games played by a machine against the environment, their computability as existence of a machine that always wins the game, logical operators as operations on computational problems, and validity
Validity
In logic, argument is valid if and only if its conclusion is entailed by its premises, a formula is valid if and only if it is true under every interpretation, and an argument form is valid if and only if every argument of that logical form is valid....
of a logical formula as being a scheme of "always computable" problems.
Classical logic
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
, intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
, and linear logic
Linear logic
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...
(in a broad sense), turn out to be three natural fragments of CL.
The classical concept of truth is a special case of computability, – computability restricted to problems of zero interactivity degree. Correspondingly, classical logic is a special fragment of CL. One of the main intuitions associated with intuitionistic logic is that it must be a logic of problems (Kolmogorov 1932); this is exactly what CL is, but in a more expressive language than intuitionistic logic. And one of the main claims of linear logic is that it is a logic of resources. Reversing of the roles of the machine and its environment turns computational problems into computational resources, which makes CL a logic of resources, only, again, in a more expressive language than that of linear logic, and based on an intuitively convincing and mathematically strict resource semantics.