Expansion Trees with Cut

TL;DR

This paper introduces a novel extension of expansion trees with cuts, enabling representation of non-prenex formulas and providing a cut-elimination procedure with proven weak normalization.

Contribution

It presents a new approach to extend expansion trees with cuts, covering non-prenex formulas and establishing a natural reduction-based cut-elimination method.

Findings

Extension of expansion trees with cuts for non-prenex formulas

A natural reduction-based cut-elimination procedure

Proof of weak normalization using epsilon-calculus methods

Abstract

Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view it suggests a compact representation of proofs in classical first- and higher-order logic by recording the information which instances have been chosen for which quantifiers, known in the literature as expansion trees. Such a representation is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cut have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas. In this paper we present a new approach that directly extends expansion trees by cuts and covers also non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps. We prove that it is weakly normalizing using methods from the epsilon-calculus.