BCK is not structurally complete (Q2452677)

A logic is a set of formulae closed under a consequence operation given by some axioms and structural inference rules. An inference rule \(\alpha _{1},...,\alpha _{n}/\beta \) is \textit{derivable} in a logic \(L\) if \(\beta \in C(\{\alpha _{1},...,\alpha _{n}\})\) where \(C\) is the consequence operation of \(L\). And it is \textit{admissible} if \(\sigma (\alpha _{1}),...,\sigma (\alpha _{n})\in L\) implies \(\sigma (\beta )\in L\) for every substitution \(\sigma \). A logic is \textit{structurally complete} if \ every rule admissible in \(L\) is also derivable in \(L\). The logic BCK is the pure implicational logic axiomatized (together with \textit{modus ponens}) with the following axioms: (B) \((\varphi \rightarrow \psi )\rightarrow [ (\chi \rightarrow \varphi )\rightarrow (\chi \rightarrow \psi )]\); (C) \([\varphi \rightarrow (\psi \rightarrow \chi )]\rightarrow [ \psi \rightarrow (\varphi \rightarrow \chi )]\); (K) \( \varphi \rightarrow (\psi \rightarrow \varphi ).\) The author proves that BCK is not structurally complete by showing that the rule (let us call it \(\rho \) here) \((\alpha \rightarrow \beta )\rightarrow \beta /(\beta \rightarrow \alpha )\rightarrow \alpha \) is admissible but not derivable in BCK. The admissibility of \(\rho \) is proved by using a Gentzen-style sequent calculus version of BCK. This Gentzen calculus makes an essential use of \textit{split terms}, a notion introduced by the author (``split terms can be thought of as encoding cut-free proofs of provable sequents in which they occur'', p. 199). The non-derivability of \(\rho \) is proved by showing its failure in the \( \{\rightarrow ,1\}\)-reduct of the totally ordered 3-element Heyting algebra. In the last section of the paper, the author notes: ``admissible but non derivable rules describe certain properties of the free BCK-algebra that are not shared by all BCK-algebras'' (p. 203). Then, he proceeds to prove one of these special properties.