Extending intuitionistic linear logic with knotted structural rules.
R. Hori, H. Ono, Harold Schellinx · Notre Dame Journal of Formal Logic · 1994
In the present paper, extensions of the intuitionistic linear logic with knotted structural rules are discussed.Each knotted structural rule is a rule of inference in sequent calculi of the form: from T,A,... ,A (n times) -It is a restricted form of the weakening rule when n k.Our aim is to explore how they behave like (or unlike) the weakening and contraction rules, from both syntactic and semantic point of view.It is shown that when either n = 1 or k = 1, strong similarities hold between logics with the (n ~* k) rule and logics with the weakening or the contraction rule, as for the cut elimination theorems, decidability and undecidability results and the finite model property.