The power of quantifier shifts

Quantifier shifts are one of the oldest proof procedures, but they are orthogonal to the cut-free format: They can shorten proofs non-elementarily. (The proof is based on the sequence of proofs exhibiting a non-elementary difference between proofs with cuts and cut-free proofs by Orevkov.) The cost is however that those proofs are globally sound but locally unsound. (Their subderivations might be unsound in contrast to the Hilbert concept of proof.) In non-classical logics these calculi are only sound when all quantifier shifts are added. This characterizes all intermediary logics where Skolemization and the epsilon calculus is conservative (in contrast to the epsilon theorem which holds only for finitely-valued Gödel logics). This research is based on features of the epsilon calculus.