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.