%0 Journal Article
%T Extending a system in the calculus of structures with a self-dual quantifier
%A Luca Roversi
%J Computer Science
%D 2012
%I arXiv
%R 10.1093/logcom/exu033
%X 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.
%U http://arxiv.org/abs/1212.4483v1