Quantifier shifts can shorten proofs but cause local unsoundness
Proof Theory of Quantifier Shifts - An Overview
Logic in Computer Science
Summary
Proofs in logic often use rules called quantifier shifts. This paper explains that using these shifts can make proofs much shorter but can create parts of the proof that seem incorrect by traditional standards. The authors show this plays out differently depending on the type of logic involved. In some logical systems, adding all quantifier shifts ensures the proofs remain reliable overall, even if parts are locally questionable. This affects how certain logical methods like Skolemization work in intermediate logics.
What this means in practice
- •For proof system designers: Decide which quantifier shift rules to include for balancing proof length and local correctness in automated theorem proving systems.
- •For formal methods engineers: Improve reasoning tools for software verification by selecting appropriate quantifier transformation techniques that preserve soundness in intermediate logics.
A theory result. No direct application yet.
Authors
Matthias Baaz, Mariami Gamsakhurdia
Abstract
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).