Algorithmic introduction of π2-cuts

Abstract

One of the crucial results in proof theory is Gentzens Hauptsatz, also known as the cut-elimination theorem. Cut-elimination is a technique to incorporate only the necessary content of lemmas within a formal proof into the proof while eliminating the additional structure of the lemma. The resulting object, a cut-free proof, gives insights about the computational content of a proof and is of major interest for subjects such as proof mining and automated theorem proving. Such proofs show an analytic behaviour mainly discernible in the subformula property which tells us that within the proof only subformulas of the statement are used. A drawback is the large size of cut-free proofs, due to missing structure expressible by lemmas. In this thesis, we propose an inversion of the cut-elimination method based on a connection of formal grammars and proof theory. We specify characteristic grammars for cut formulas according to the arithmetical hierarchy up to 2 formulas and discuss whether the existence of such a grammar allows us to rewrite a given cut-free proof, now with 2-cut formulas, in order to reduce the proof size. Thereby, we revisit 1-cut introduction, present an algorithm to introduce 2 cuts which is shown to be complete for a fragment, and discuss the decidability of the problem whether 2 cuts exist for a given grammar. Moreover, we show that our method of 2-cut introduction achieves an exponential compression of the proof size.