Introduction to Cirquent Calculus and Abstract Resource Semantics

Abstract

This paper introduces a refinement of the sequent calculus approach called cirquent calculus. While in Gentzen-style proof trees sibling (or cousin, etc.) sequents are disjoint sequences of formulas, in cirquent calculus they are permitted to share elements. Explicitly allowing or disallowing shared resources and thus taking to a more subtle level the resource-awareness intuitions underlying substructural logics, cirquent calculus offers much greater flexibility and power than sequent calculus does. A need for substantially new deductive tools came with the birth of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html) - the semantically constructed formal theory of computational resources, which has stubbornly resisted any axiomatization attempts within the framework of traditional syntactic approaches. Cirquent calculus breaks the ice. Removing contraction from the full collection of its rules yields a sound and complete system for the basic fragment CL5 of computability logic. Doing the same in sequent calculus, on the other hand, throws out the baby with the bath water, resulting in the strictly weaker affine logic. An implied claim of computability logic is that it is CL5 rather than affine logic that adequately materializes the resource philosophy traditionally associated with the latter. To strengthen this claim, the paper further introduces an abstract resource semantics and shows the soundness and completeness of CL5 with respect to it.

To appear in Journal of Logic and Computation

References in corpus (5)

• Propositional computability logic I
• Computability Logic: a formal theory of interaction
• From truth to computability I
• Propositional Computability Logic II
• From truth to computability II

Cited by in corpus (32)

• Sequential operators in computability logic
• Cirquent calculus deepened
• From truth to computability I
• The intuitionistic fragment of computability logic at the propositional level
• From truth to computability II
• Many concepts and two logics of algorithmic reduction
• 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
• Towards applied theories based on computability logic
• In the beginning was game semantics
• The parallel versus branching recurrences in computability logic
• Introduction to clarithmetic I
• On the system CL12 of computability logic
• A new face of the branching recurrence of computability logic
• A logical basis for constructive systems
• Separating the basic logics of the basic recurrences
• The Computational Complexity of Propositional Cirquent Calculus
• Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs
• Elementary-base cirquent calculus I: Parallel and choice connectives
• Build your own clarithmetic I: Setup and completeness
• Ptarithmetic
• Quantifying Resource Use in Computations
• Quantifying Shannon's Work Function for Cryptanalytic Attacks
• The countable versus uncountable branching recurrences in computability logic
• Soundness and completeness of the cirquent calculus system CL6 for computability logic
• A PSPACE-Complete First Order Fragment of Computability Logic
• Implementing program extraction from CL1-proofs
• A propositional system induced by Japaridze's approach to IF logic
• Enumerating Independent Linear Inferences
• A cirquent calculus system with clustering and ranking