Invitation to the Logic Seminar at the National University of Singapore
Date: Wednesday, 13 February 2019, 17:00 hrs
Room: S17#04-06, Department of Mathematics, NUS
Speaker: Matthias Baaz
Title: On the benefit of unsound rules: Henkin quantifiers and beyond
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 Hilber’s stepwise concept of proof by
useful global concepts.
We use these ideas to provide analytic calculi for Henkin quantifiers and
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