Double negation shifts as conservation criteria

Giulio Fellin

University of Verona



Abstract: Abstracting Glivenko's theorem from double negation and provability to a nucleus on an arbitrary set with an inductively generated single-succedent entailment relation requires that all generating rules of the latter remain admissible in the Kleisli extension, i.e. when applying the nucleus to the succedent of every premiss and the conclusion. This conservation criterion is automatic for every rule which is right invariant, i.e. all premisses and the conclusion of which have the very same succedent. In the single-succedent calculi for minimal propositional, infinitary and first-order predicate logic, the only rules which cannot be expressed as right invariant rules are the right rules for implication, infinite conjunction and the universal quantifier. The conservation criteria for these critical rules with respect to any nucleus on formulas are equivalent to the corresponding counterparts of Kuroda's double negation shift.

This talk is based on joint work with Peter Schuster, as well as ongoing joint work with Sara Negri and Peter Schuster.