Quantifier shifts are one of the oldest proof methods, 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 intermediate logics where Skolemization and the epsilon calculus is conservative (in contrast to the epsilon theorem which holds only for finite-valued Goedel logics).
We investigate the eliminability of the absoluteness operator Delta in Goedel logics. While Delta is not definable from the standard connectives and disrupts important proof-theoretic properties, we show that it becomes eliminable at the propositional level under a non-standard semantics in which all propositional atoms (except the truth constant 'True') are interpreted strictly below 1. Under this semantics, every formula containing Delta is equivalent to a disjunction of chain formulas, yielding a Delta-free normal form (standard and non-standard semantics coincide w.r.t. valid formulas without Delta). We further analyze the situation in the first-order setting, where Delta-elimination fails in general due to recursion-theoretic and topological constraints, but can be recovered under witnessed semantics.