Matthias Baaz: On the benefit of unsound rules: Henkin quantifiers and beyond

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
preserve analyticity.

Leave a Reply

Your email address will not be published. Required fields are marked *

Time limit is exhausted. Please reload CAPTCHA.

This site uses Akismet to reduce spam. Learn how your comment data is processed.