Kanger-Wang-type Sequent Calculi with Equality

We develop a proof theoretic analysis of several extensions of the G3[mic] sequent calculi with rules for equality related to those introduced by H.Wang and S.Kanger. 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 alternate semantic tableau method, strictness (which does not allow to retain the formulae that are modified) can be imposed together with the orientation of the replacement of equals provided the latter is allowed on all atomic formulae and their negations. Furthermore we prove that the result holds also for languages with function symbols provided strictness is not imposed on equalities, leaving it open whether or not strictness can be imposed on equalities as well. Finally 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.

Authors

• Franco Parlamento
• Flavio Previale

Keywords

• Sequent Calculus
• Structural Rules
• Equality
• Replacement Rules
• Admissibility