Logics for computability
Encyclopedia
Logics for computability are formulations of logic which
capture some aspect of computability as a basic notion. This usually involves a mix
of special logical connective
s as well as semantics
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 in 1945, who gave an interpretation of intuitionistic number theory in terms of Turing machine
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
and linear logic
, and novel semantic models, such as game semantics
, logics for computability have been formulated in several contexts. Here we mention two.
by Martin Hyland
in 1982 who constructed the effective topos
. In 2002, Steven Awodey, Lars Birkedal, and Dana Scott
formulated a modal logic for computability which extended the usual realizability interpretation with two modal operators expressing the notion of being "computably true".
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
.
capture some aspect of computability as a basic notion. This usually involves a mix
of special logical connective
Logical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s as well as semantics
Semantics
Semantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
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 in 1945, who gave an interpretation of intuitionistic number theory in terms of Turing machine
Turing machine
A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can be adapted to simulate the logic of any computer algorithm, and is particularly useful in explaining the functions of a CPU inside a...
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
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
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...
, and novel semantic models, such as game semantics
Game semantics
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 the late 1950s Paul Lorenzen was the...
, 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 logicIntuitionistic 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...
by Martin Hyland
Martin Hyland
John Martin Elliott Hyland is professor of mathematics at King's College in the University of Cambridge, England where he is currently head of the Department of Pure Mathematics and Mathematical Statistics...
in 1982 who constructed the effective topos
Effective topos
In mathematics, the effective topos is a topos introduced by , based on Kleene's notion of recursive realizability, that captures the idea of effectivity in mathematics....
. In 2002, Steven Awodey, Lars Birkedal, and Dana Scott
Dana Scott
Dana Stewart Scott 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, California...
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 JaparidzeGiorgi Japaridze
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...
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
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...
.