Extending a system in the calculus of structures with a self-dual quantifier

Abstract

We recall that SBV, a proof system developed under the methodology of deep inference, extends multiplicative linear logic with the self-dual non-commutative logical operator Seq. We introduce SBVQ that extends SBV by adding the self-dual quantifier Sdq. The system SBVQ is consistent because we prove that (the analogous of) cut elimination holds for it. Its new logical operator Sdq operationally behaves as a binder, in a way that the interplay between Seq, and Sdq can model β-reduction of linear λ-calculus inside the cut-free subsystem BVQ of SBVQ. The long term aim is to keep developing a programme whose goal is to give pure logical accounts of computational primitives under the proof-search-as-computation analogy, by means of minimal, and incremental extensions of SBV.

29 pages

References in corpus (1)

• Communication, and concurrency with logic-based restriction inside a calculus of structures

Cited by in corpus (5)

• Subatomic Proof Systems: Splittable Systems
• De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
• A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
• Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)
• Subatomic systems need not be subatomic