On the computational complexity of cut-reduction

TL;DR

This paper explores the computational complexity of cut-reduction in proof systems, developing notation systems for Bounded Arithmetic to uniformly derive bounds and results on definable functions.

Contribution

It introduces a notation system for Bounded Arithmetic that enables uniform derivation of bounds and known results on definable functions.

Findings

Explicit bounds on cut-reduction can be obtained using the notation system.

The notation system allows rederivation of known results in a uniform manner.

The approach clarifies the complexity of cut-reduction in proof systems.

Abstract

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations, and explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.