Glivenko's theorem says that, in propositional logic, classical provability of a formula entails intuitionistic provability of double negation of that formula. We generalise Glivenko's theorem from double negation to an arbitrary nucleus, from provability in a calculus to an inductively generated abstract consequence relation, and from propositional logic to any set of objects whatsoever. The resulting conservation theorem comes with precise criteria for its validity, which allow us to instantly include G\"odel's counterpart for first-order predicate logic of Glivenko's theorem. The open nucleus gives us a form of the deduction theorem for positive logic, and the closed nucleus prompts a variant of the reduction from intuitionistic to minimal logic going back to Johansson.
翻译:格利文科的理论认为,在理论逻辑中,公式的古典可变性意味着公式的直觉可被双重否定。 我们把格利文科的理论从双重否定变成任意的核心,从微积分的可变性到感性产生的抽象后果关系,从推理逻辑到任何一组物体。 由此形成的保存理论有其有效性的精确标准,这使我们能够立即将G\“odel”的对应方纳入Glivenko理论的第一阶上游逻辑中。 开放核为我们提供了积极逻辑的推论,而封闭核则引发了从直觉到最小逻辑的递归回约翰森的变体。