Proof theory for branching quantifiers: CERES and beyond
Quantifiers "For all" and "There exists" belong to the most important features of first-order logic. However, it is impossible to express refined dependencies as "For all x there is a u, independent of y, and for all y there is a v, independent of x" using only these two quantifiers. For this aim it is necessary to introduce a class of quantifiers originally formulated by Leon Henkin and named after him, later extended to independence friendly logic. Note that the completeness theorem for first-order classical logic does not hold for first-order classical logic extended by Henkin quantifiers. This implies that - analogous to second-order logic - there is no formal system that allows to prove all true sentences.
This project is concerned with the development of deductive systems which capture at least the most natural theorems of such logics. For these deduction systems we intend to prove, among others, the cut-elimination theorem and variants of the theorem of Herbrand. The possibility to eliminate cuts is of central importance for the analysis of proofs in first-order logic, i.e. proof mining.
Using the results of this project it is intended to analyze derivations incorporating structured objects such as vectors. Vectors are expressible with Henkin quantifiers in a direct way, without detour to pairing and projection. This makes it possible to analyze proofs in e.g. affine geometry directly. In addition, the results of the project will allow to extend CERES, the up-to-date most efficient system for the elimination of cuts in first-order logic to independence friendly logic and other logics with branching quantifiers.
According to Barwise, Henkin quantifiers are essential to capture important linguistic configurations. This project intends to automate the handling of such linguistic contexts and to support the automated analysis of linguistic argumentations.
The project description is available
here.
A List of Selected Talks and Activities
- Matthias Baaz, Unsound Rules and Quantifier Macros, Seminar of the Chair of Mathematical Logic at MSU, March 6 2019, Moscow Russia
- Matthias Baaz, On the Benefit of Unsound Rules: Henkin Quantifiers and Beyond, JAIST Logic Seminar, February 2019, Kanazawa Japan
- Anela Lolic, Work in Progress on Henkin Quantifiers, Seminar of the Computational Logic Group at TU Wien, January 16 2019
- Matthias Baaz, The Concept of Proof, JAIST Logic Seminar, April 26 2018, Kanazawa Japan
- Matthias Baaz, The Concept of Proof, Computational Approaches to the Foundations of Mathematics, April 11 2018, Munich, Germany
- Matthias Baaz, Fast Cut-Elimination for Intuitionistic Logic, Second SYSMICS Workshop, February 28 2018, Vienna, Austria
- Matthias Baaz, On the Benefit of Unsound Rules, Seminar Laboratoire J.A. Dieudonne, January 31 2018, Nice, France
- Matthias Baaz, A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem, LFCS 2018, January 8 2018, Deerfield Beach, Florida, U.S.A.
Publications
Progress