Many concepts and two logics of algorithmic reduction

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

To appear in Studia Logica in the Spring of 2009

References in corpus (12)

• Sequential operators in computability logic
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Propositional computability logic I
• Cirquent calculus deepened
• Computability Logic: a formal theory of interaction
• From truth to computability I
• The intuitionistic fragment of computability logic at the propositional level
• Propositional Computability Logic II
• Intuitionistic computability logic
• From truth to computability II
• The logic of interactive Turing reduction
• In the beginning was game semantics

Cited by in corpus (17)

• Sequential operators in computability logic
• The taming of recurrences in computability logic through cirquent calculus, Part I
• Toggling operators in computability logic
• From formulas to cirquents in computability logic
• Introduction to clarithmetic II
• In the beginning was game semantics
• Towards applied theories based on computability logic
• The parallel versus branching recurrences in computability logic
• On the system CL12 of computability logic
• A logical basis for constructive systems
• Introduction to clarithmetic I
• Separating the basic logics of the basic recurrences
• Elementary-base cirquent calculus I: Parallel and choice connectives
• Ptarithmetic
• The countable versus uncountable branching recurrences in computability logic
• Sequential Operations in LogicWeb
• Implementing program extraction from CL1-proofs