Glivenko like theorems in natural expansions of BCK-logic. (English) Zbl 1045.03026

The authors prove the following generalisation of Glivenko’s Theorem: If \(\mathcal L\) is a logic that is an extension of BCK logic, with intuitionistic negation, that has a certain algebraic semantics and \(\mathcal{IL}\) is \(\mathcal{L}\) with the double negation axiom, then: \[ \vdash_{\mathcal L}\lnot\lnot\varphi\;\;\text{iff}\;\;\vdash_{\mathcal IL}\varphi \] if and only if \(\vdash_{\mathcal L}\lnot\lnot(\lnot\lnot\varphi\to\varphi)\). (Of course, in BCK logic with intuitionistic negation the latter is unprovable.) The proof uses extensive work on BCK algebras that corresponds to the logics.


03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03G25 Other algebras related to logic
06F35 BCK-algebras, BCI-algebras
Full Text: DOI