# The Cut Elimination and the Nonlengthening Property for the Sequent Calculus with Equality

## TL;DR

This paper explores the extension of the sequent calculus to first order logic with equality, focusing on cut elimination and nonlengthening properties, building on Leibnitz's principle and Gentzen's work.

## Contribution

It introduces new insights into cut elimination and enhances the nonlengthening property for sequent calculus with equality.

## Key findings

- Established cut elimination for the extended calculus.
- Improved the nonlengthening property for equality logic.
- Connected Leibnitz's principle with sequent calculus extensions.

## Abstract

We show how Leibnitz.s indiscernibility principle and Gentzen's original work lead to extensions of the sequent calculus to first order logic with equality and investigate the cut elimination property. Furthermore we discuss and improve the nonlengthening property of Lifshitz and Orevkov.