Admissibility of the Structural Rules in the Sequent Calculus with Equality

Abstract

On the ground of a general theorem concerning the admissibility of the structural rules in sequent calculi with additional atomic rules, we develop a proof theoretic analysis for several extensions of the ${\bf G3[mic]}$ sequent calculi with rules for equality, including the one originally proposed by H.Wang. In the classical case we relate our results with the semantic tableau method for first order logic with equality. In particular we establish that, for languages without function symbols, in Fitting's alternative semantic tableau method, strictness (which does not allow the repetition of equalities which are modified) can be imposed together with the orientation of the replacement of equals. A significant progress is made toward extending that result to languages with function symbols although whether that is possible or not remains to be settled. We also briefly consider systems that, in the classical case, are related to the semantic tableau method in which one can expand branches by adding identities at will, obtaining that also in that case strictness can be imposed. Furthermore we discuss to what extent the strengthened form of the nonlengthening property of Orevkov known to hold for the sequent calculi with the structural rules applies also to the present context.