Hydra Games for Cut Elimination and Ordinal Analysis of IPL2

Abstract

Intuitionistic propositional logic with 2nd order propositional quantifiers (IPL2) was introduced by Gabbay in 1974. Since then, a substantial body of work has been written about its semantics. However, there has not been any work thoroughly exploring the proof theory of IPL2, or even defining a Gentzen style sequent calculus. We define two fragments of IPL2 that will be the focus of our efforts. First, the fragment corresponding to the absence of quantifier rule appli- cations to formulas that are later used as cut formulas. Second, the fragment corresponding to the application of at most quantifier free substitutions in quantifier rules that are applied to formulas that are later used as cut formulas. In this work, we will define such a sequent calculus, and prove that these two fragments have the property of cut elimination. In order to prove this, we will make use of 𝑛-ary multicut rules and hydra games. Our proof of cut elimination will make use of cut rewrite operations, as with the usual proof. However these will be applied to the tree structure within an application of a multicut rule, rather than to the proof trees themselves. We will use the cut rewrite operations as moves within a Büchholz hydra game. These will show that, despite the blowup in the proof size and the length of the multicut, the hydra game on its tree must terminate. Then we show that this termination property on the multicut rewrite hydra game corresponds to cut elimination for the fragment of IPL2 in question. Because of the explicit measure assigned to the multicut trees within the hydra game, we immediately obtain an upper bound for an ordinal analysis of both of the fragments from the cut elimination proof. This ordinal is 𝜔𝜔 . Finally, we discuss the failure of this method for the full IPL2 calculus.