Link Formulas in Implication Fragments of Substructural Logics

ABSTRACT. Two well-known implication fragments of substructural logics are BCI (fragment of logic without contraction and weakening) and BCK (fragment of logic without contraction). The technique of link formulas was developed by the present author first for BCI, as a tool to solve an open problem. Then, a modification of the technique turned out to work for BCK and delivered a proof of its structural incompleteness. The technique can be used to obtain relatively easy proofs of admissibility of certain rules in BCK and BCI, yielding structural incompleteness proofs of several logics in the vicinity.

I will present the technique in a uniform way, applicable to BCI and BCK, as well as to the implication fragments of the relevant logic R and the intuitionistic logic. Some applications (old and new) will be presented to illustrate the technique.