A simplified version of the Sequent Calculus G3[mic]^=

TL;DR

This paper simplifies the sequent calculus G3[mic]^= by replacing the Replacement Rule with a simpler rule that avoids formula repetition, streamlining the proof system for first-order languages with equality.

Contribution

It introduces a simplified rule for G3[mic]^= that maintains soundness and completeness, reducing complexity in the sequent calculus for first-order logic with equality.

Findings

Replacement rule can be replaced with a simpler rule

Simplification does not affect the calculus's properties

Streamlined proof system for first-order logic with equality

Abstract

We show that the Replacement Rule in the sequent calculus G3[mic]}^=, for first order languages with function symbols and equality, can be replaced by the simpler rule in which the transformed formula is not repeated in the premiss.