Logics for computability are formulations of logic which
capture some aspect of
computability
Computability is the ability to solve a problem in an effective manner. It is a key topic of the field of computability theory within mathematical logic and the theory of computation within computer science. The computability of a problem is close ...
as a basic notion. This usually involves a mix
of special
logical connective
In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a logical constant. They can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary co ...
s as well as
semantics
Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy
Philosophy (f ...
which explains how the logic is to be interpreted in a computational way.
Probably the first formal treatment of logic for computability is the ''
realizability interpretation'' by
Stephen Kleene
Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
in 1945, who gave an interpretation of intuitionistic number theory in terms of
Turing machine
A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
computations. His motivation was to make precise the ''
Heyting-Brouwer-Kolmogorov (BHK) interpretation'' of intuitionism, according to which proofs of mathematical statements are to be viewed as constructive procedures.
With the rise of many other kinds of logic, such as
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
and
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. Although the logic has also be ...
, and novel semantic models, such as
game semantics
Game semantics (german: dialogische Logik, translated as ''dialogical logic'') is an approach to Formal semantics (logic), formal semantics that grounds the concepts of truth or Validity (logic), validity on game theory, game-theoretic concepts, su ...
, logics for computability have been formulated in several contexts. Here we mention two.
Modal logic for computability
Kleene's original realizability interpretation has received much attention among those who study connections between computability and logic. It was extended to full higher-order
intuitionistic logic
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 ...
by
Martin Hyland
(John) Martin Elliott Hyland is professor of mathematical logic at the University of Cambridge and a fellow of King's College, Cambridge. His interests include mathematical logic, category theory, and theoretical computer science.
Education
H ...
in 1982 who constructed the
effective topos In mathematics, the effective topos is a topos
In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much ...
. In 2002,
Steve Awodey
Steven M. Awodey (; born 1959) is an American mathematician and logician. He is a Professor of Philosophy and Mathematics at Carnegie Mellon University.
Biography
Awodey studied mathematics and philosophy at the University of Marburg and the Univ ...
,
Lars Birkedal, and
Dana Scott
Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, Ca ...
formulated a modal logic for computability which extended the usual realizability interpretation with two modal operators expressing the notion of being "computably true".
Japaridze's computability logic
"Computability Logic" is a proper noun referring to a research programme initiated by
Giorgi Japaridze Giorgi Japaridze (also spelled Giorgie Dzhaparidze) 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 i ...
in 2003. Its ambition is to redevelop logic from a game-theoretic semantics. Such a semantics sees games as formal equivalents of interactive computational problems, and their "truth" as existence of algorithmic winning strategies. See
Computability logic
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 G ...
See also
*
Computability logic
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 G ...
*
Game semantics
Game semantics (german: dialogische Logik, translated as ''dialogical logic'') is an approach to Formal semantics (logic), formal semantics that grounds the concepts of truth or Validity (logic), validity on game theory, game-theoretic concepts, su ...
*
Interactive computation
In computer science, interactive computation is a mathematical model for computation that involves input/output communication with the external world ''during'' computation.
Uses
Among the currently studied mathematical models of computation th ...
References
*S.C. Kleene.
On the interpretation of intuitionistic number theory'. Journal of Symbolic Logic, 10:109-124, 1945.
*J.M.E. Hyland. ''The effective topos''. In
A. S. Troelstra and D. Van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165-216. North Holland Publishing Company, 1982.
*S. Awodey, L. Birkedal, and D.S. Scott.
Local realizability toposes and a modal logic for computability'. Mathematical Structures in Computer Science, 12(3):319-334, 2002.
*G. Japaridze,
Introduction to computability logic'. Annals of Pure and Applied Logic 123 (2003), pages 1–99.
External links
Logics of Types and Computation at CMUGiorgi Japaridze
Systems of formal logic