A Constructive Proof of Cut Elimination for a System of Full Second Order Logic

TL;DR

This paper provides a constructive proof of cut elimination for full second order logic, introducing a new parameter called cutweight to control cutrank growth, which can also be applied to first order logic.

Contribution

It introduces a novel constructive proof method for cut elimination in second order logic using cutweight, simplifying the process and avoiding cutrank growth.

Findings

Constructive proof of cut elimination for second order logic

Introduction of cutweight as a new induction parameter

Method applicable to first order logic

Abstract

In this paper we present a constructive proof of cut elimination for a system of full second order logic with the structural rules absorbed and using sets instead of sequences. The standard problem of the cutrank growth is avoided by using a new parameter for the induction, the cutweight. This technique can also be applied to first order logic.