top of page

Double negation shifts as conservation criteria

Giulio Fellin

The double negation shift (DNS) is crucial for extending Glivenko’s theorem from propositional to first-order logic. It demonstrates that classical predicate logic is conservative over intuitionistic logic when combined with DNS. We discuss abstracting Glivenko’s theorem beyond double negation and provability, requiring certain closure conditions on inductively generated proof systems. Among the critical rules for obtaining such conservativity are the right rules for implication and the universal quantifier, highlighting the DNS-like criteria that enable generalizations.

bottom of page