From formulas to cirquents in computability logic

Abstract

Computability logic (CoL) (see http://www.cis.upenn.edu/~giorgi/cl.html) is a recently introduced semantical platform and ambitious program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Its expressions represent interactive computational tasks seen as games played by a machine against the environment, and "truth" is understood as existence of an algorithmic winning strategy. With logical operators standing for operations on games, the formalism of CoL is open-ended, and has already undergone series of extensions. This article extends the expressive power of CoL in a qualitatively new way, generalizing formulas (to which the earlier languages of CoL were limited) to circuit-style structures termed cirquents. The latter, unlike formulas, are able to account for subgame/subtask sharing between different parts of the overall game/task. Among the many advantages offered by this ability is that it allows us to capture, refine and generalize the well known independence-friendly logic which, after the present leap forward, naturally becomes a conservative fragment of CoL, just as classical logic had been known to be a conservative fragment of the formula-based version of CoL. Technically, this paper is self-contained, and can be read without any prior familiarity with CoL.

LMCS 7 (2:1) 2011

References in corpus (18)

• 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
• Many concepts and two logics of algorithmic reduction
• From truth to computability II
• Toggling operators in computability logic
• The logic of interactive Turing reduction
• Introduction to clarithmetic II
• Towards applied theories based on computability logic
• In the beginning was game semantics
• A logical basis for constructive systems
• Introduction to clarithmetic I

Cited by in corpus (9)

• The taming of recurrences in computability logic through cirquent calculus, Part I
• The parallel versus branching recurrences in computability logic
• On the system CL12 of computability logic
• Build your own clarithmetic I: Setup and completeness
• Elementary-base cirquent calculus I: Parallel and choice connectives
• A propositional system induced by Japaridze's approach to IF logic
• The countable versus uncountable branching recurrences in computability logic
• A cirquent calculus system with clustering and ranking
• Soundness and completeness of the cirquent calculus system CL6 for computability logic