  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.
