Contraction Elimination in Sequent Based Ground Equational Calculus

TL;DR

This paper investigates the eliminability of the contraction rule in two ground equational sequent calculi, demonstrating that it is not eliminable in one but is eliminable in the other, refining understanding of proof transformations.

Contribution

It proves that contraction is not eliminable in EQ_M but is eliminable in EQ', clarifying differences in proof rule eliminability between these calculi.

Findings

Contraction is not eliminable in EQ_M.

Contraction is eliminable in EQ'.

The results refine proof transformation techniques in equational sequent calculi.

Abstract

In "Cut Elimination for Gentzen's Sequent Calculus with Equality and Logic of Partial Terms" LNCS 7750,161-172(2013), we have shown that the cut rule is eliminable in two ground equational sequent calculi, to be denoted by EQ_M and EQ'. In this note we prove that the contraction rule is not eliminable in EQ_M but it is eliminable in EQ'.