THE ELIMINATION OF ATOMIC CUTS AND THE SEMISHORTENING PROPERTY FOR GENTZEN’S SEQUENT CALCULUS WITH EQUALITY
Franco Parlamento, Flavio Previale · The Review of Symbolic Logic · 2019
Abstract We study various extensions of Gentzen’s sequent calculus obtained by adding rules for equality. One of them is singled out as particularly natural and shown to satisfy full cut elimination, namely, also atomic cuts can be eliminated. Furthermore we tell apart the extensions that satisfy full cut elimination from those that do not and establish a strengthened form of the nonlenghtening property of Lifschitz and Orevkov.