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

TL;DR

This paper introduces SBVQ, an extension of the deep inference proof system SBV, adding a self-dual quantifier that models computational reduction, and proves its consistency through cut elimination.

Contribution

It extends SBV with a self-dual quantifier Sdq, demonstrating its operational behavior and its ability to model lambda-calculus reduction within a deep inference framework.

Findings

SBVQ is consistent due to cut elimination.

Sdq acts as a binder in the proof system.

Modeling of lambda-calculus reduction within SBVQ.

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 {\beta}-reduction of linear {\lambda}-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.