On the benefit of unsound rules: Henkin quantifiers and beyond

On the benefit of unsound rules: Henkin quantifiers and beyond

Matthias Baaz

Vienna University of Technology

Date: 
2019/02/26 (Tue) 13:30 to 14:30
Place: 
I-56 (Collaboration Room 7) on 5F of IS Building III at JAIST
Group: 
Logic Unit

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.

コンタクト
Nao Hirokawa