A General Skolemisation Framework for Sequent Calculi and Expansion Proofs

Abstract

Many different forms of Skolemisation exist in the literature, and their effect on proof complexity has been extensively studied since its first introduction. Other approaches to handling strong quantifiers, using variables instead of skolemterms together with acyclicity conditions similar to the original eigenvariable condition in Gentzen’s LK, are also well-known in literature. This thesis aims to unify these notions within a single comprehensive framework. We introduce skolem annotations in the form of superscripts on strong quantifiers in first-order predicate formulas as a method for controlling quantifier dependencies. We work with sequent calculi and expansion tree calculi for annotated sequents, considering both skolem-based and variable-based approaches to strong quantifier introductions. For these systems, we show that one can freely switch between the different calculi, giving size-preserving translations between the use of skolemterms and the use of variables in strong quantifiers, as well as upper bounds for size when translating between sequent and expansion tree proofs. Additionally, we also show how proofs of an annotated sequent can be reconstructed from proofs of its skolemised form with an upper bound for the size increase that is linear in the number of strong quantifiers. We then explain how classical LK, LK+, Henkin quantifiers, and certain cases of Independence-Friendly Logic can be embedded into our framework by choosing suitable annotations.