On the benefit of unsound rules: Henkin quantifiers and beyond

• Matthias Baaz

• Vienna University of Technology

• homepage

We give examples of analytic sequent calculi LK+ and LK++ that extend Gentzen's sequent calculus LK by unsound quantifier rules in such a way that
i) derivations lead only to true sequents,
ii) cut free proofs may be non-elementary shorter than cut free LK proofs.
This research is based on properties of Hilbert's epsilon calculus and is part of efforts to complement Hilbert's stepwise concept of proof by useful global concepts. We use these ideas to provide analytic calculi for Henkin quantifiers demonstrate soundness, (cut free) completeness and cut elimination. Furthermore, we show, that in the case of quantifier macros such as Henkin quantifiers for a partial semantics global calculi are the only option to preserve analyticity.