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.

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. 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 has been concerned with the development of deductive systems which capture at least the most natural theorems of such logics. For these deduction systems we have proved, 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.