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

Cignoli, Roberto; Torrens Torrell, Antoni

Math. Log. Q. 50, No. 2, 111-125 (2004).

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.

Reviewer: Martin W. Bunder (Wollongong)

MSC:

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

Keywords:

Glivenko’s theorem; extension of BCK logic; intuitionistic negation; algebraic semantics; BCK algebras