BCK is not structurally complete
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.
- Deductive systems with multiple-conclusion rules and the disjunction property
- An abelian rule for BCI -- and variations
- Almost structural completeness; an algebraic approach
- On the linear complexity of Ding-Helleseth generalized cyclotomic binary sequences of order four and six
- scientific article; zbMATH DE number 4202236 (Why is no real title available?)
- scientific article; zbMATH DE number 2099386 (Why is no real title available?)
- scientific article; zbMATH DE number 975274 (Why is no real title available?)
- Lattice BCK logics with modus ponens as unique rule
- Hereditarily structurally complete extensions of \(\mathbf{RM}\)
This page was built for publication: BCK is not structurally complete
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2452677)
