Schnittelimination in funktionaler Logik höherer Stufe

Abstract

It is known that there can be no elementary (reductive) proof of cut-elimination for a sequent calculus of higher-order logic, since this would provide an elementary proof of consistency of PA. Thus the cut-elimination proofs for higher-order calculi are either semantic (through Henkin semantics) or semi-semantic (through resolution, CERES). In this thesis I study a sub-logic of higher-order logic in which quantification is restricted to objects of functional type only. By functional type I mean all types of simple type theory without the occurrence of the Boolean type. Such restriction gives rise to a logic that has a manageable proof-theory and at the same time shares some interesting properties with full higher-order logic. First, I define syntax and semantics of two variants of such a logic and give the corresponding cut-elimination proofs. These are easy adaptations of the Gentzen's proof for LK: one just has to incorporate beta-eta-equality in the calculus and then repeat the argument for LK with equality. Thus, logic defined this way is proof-theoretically closer to LK than to the higher-order calculus. This becomes obvious by looking at a proof-preserving translation from functional higher-order proofs to first-order proofs that is defined in this thesis. In addition, such translation provides a new perspective on Skolemization and unification, which are both problematic in higher-order logic. Second, I study semantics of this logic: I show incompleteness wrt standard semantics and give a completeness proof wrt general semantics based on Schuütte's reduction tree method. This is a simpler and more elegant way of proving this result than a more obvious specialization of a Henkin-style completeness proof for full higher-order logic.