Many concepts and two logics of algorithmic reduction

DOI10.1007/S11225-009-9164-7MaRDI QIDQ1005975zbMATH OpenOpenAlexFDO

Authors Giorgi Japaridze

Publication date 17 March 2009

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0706.0103

zbMATH Keywords

affine logiccomputability logicgame semanticsinteractive computationintuitionistic logiclinear logic

Mathematics Subject Classification ID

Logic in computer science (03B70)

Abstract: Within the program of finding axiomatizations for various parts of computability logic, it was proved earlier that the logic of interactive Turing reduction is exactly the implicative fragment of Heyting's intuitionistic calculus. That sort of reduction permits unlimited reusage of the computational resource represented by the antecedent. An at least equally basic and natural sort of algorithmic reduction, however, is the one that does not allow such reusage. The present article shows that turning the logic of the first sort of reduction into the logic of the second sort of reduction takes nothing more than just deleting the contraction rule from its Gentzen-style axiomatization. The first (Turing) sort of interactive reduction is also shown to come in three natural versions. While those three versions are very different from each other, their logical behaviors (in isolation) turn out to be indistinguishable, with that common behavior being precisely captured by implicative intuitionistic logic. Among the other contributions of the present article is an informal introduction of a series of new -- finite and bounded -- versions of recurrence operations and the associated reduction operations. An online source on computability logic can be found at http://www.cis.upenn.edu/~giorgi/cl.html

Recommendations

• The logic of interactive turing reduction
• From truth to computability. I.
• The intuitionistic fragment of computability logic at the propositional level
• Introduction to computability logic
• Intuitionistic computability logic

Cites work

• A game semantics for linear logic
• Cirquent Calculus Deepened
• Computability logic: a formal theory of interaction
• Degrees of indeterminacy of games
• From truth to computability. I.
• From truth to computability. II.
• Games and full completeness for multiplicative linear logic
• scientific article; zbMATH DE number 2051381 (Why is no real title available?)
• In the beginning was game semantics
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Introduction to computability logic
• Intuitionistic computability logic
• Linear logic
• Sequential operators in computability logic
• The intuitionistic fragment of computability logic at the propositional level
• The logic of interactive turing reduction
• Towards applied theories based on computability logic

Cited in

(13)

• Reduction algorithms for solving large systems of logical equations
• The parallel versus branching recurrences in computability logic
• The taming of recurrences in computability logic through cirquent calculus. I
• The countable versus uncountable branching recurrences in computability logic
• On the toggling-branching recurrence of computability logic
• The logic of interactive turing reduction
• Towards applied theories based on computability logic
• Separating the basic logics of the basic recurrences
• Toggling operators in computability logic
• Introduction to clarithmetic. I
• A propositional cirquent calculus for computability logic.
• On abstract resource semantics and computability logic
• Sequential operators in computability logic

This page was built for publication: Many concepts and two logics of algorithmic reduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1005975)