BCK is not structurally complete

Tomasz Kowalski (La Trobe University)

An inference rule R, of the form "from p_1,..., p_n infer q", is derivable in a logic L if  whenever the premisses of R are true (in a model M on a valuation v), the conclusion of R is true (in M, on v).  A rule R is admissible in L, if whenever the premisses are theorems of L, so is q.  Admissibility of R is often expressed by saying that adjoining R to the consequence operation of L does not change the set of theorems of L.  A logic L is structurally complete if every admissible rule of L is derivable in L.
 
Two prominent examples are classical propositional logic, which is structurally complete, and intuitionistic propositional logic, which is not.  The notion of structural completeness is due to Pogorzelski and after about three decades of dormancy is undergoing something of a revival.  Some general results have been proved and the question of structural completeness settled for many non-classical logics.  In particular, Olson and Raftery proved that a substructural logic satisfiying certain conditions is not structurally complete.  Their conditions are satisfied by BCI, but not by BCK, so they asked whether BCK was structurally complete.
 
I will prove that BCK is not structurally complete using a proof-theoretical argument.