Expansion Trees with Cut

TL;DR

This paper introduces an extension of expansion trees with cuts, enabling a compact, analytic proof representation for non-prenex formulas in classical logic, along with a weakly normalizing cut-elimination procedure.

Contribution

It presents a new syntactic method extending Miller's expansion trees with cuts, applicable to non-prenex formulas, and provides a cut-elimination process that is weakly normalizing.

Findings

Extension of expansion trees with cuts for non-prenex formulas

A natural reduction-based cut-elimination procedure

Proof of weak normalization for the cut-elimination process

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 of which instances have been chosen for which quantifiers. This compact representation is known in the literature as Miller's expansion tree proof. It is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cuts 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 syntactic approach that directly extends Miller's 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 and show that it is weakly normalizing.