Seminario di Logica: Admissibility of the Structural Rules in the Sequent Calculus for Logic with Equality

Giovedì 30 Settembre 2015, ore 15:00 - Aula 2AB45 - Franco Parlamento


Seminario di Logica

Giovedì 30 Settembre 2015 alle ore 15:00 in Aula 2AB45, Franco Parlamento (Università di Udine) terrà un seminario dal titolo "Admissibility of the Structural Rules in the Sequent Calculus for Logic with Equality".

In the case of first order logic the transition from the natural deduction calculus with equality, to the sequent calculus, leads to a calculus for which the cut elimination theorem holds, i.e. the cut rule is admissible in the calculus that omits it. If (and only if) the cut rule is context sharing, the contraction rule is admissible too, in the purely equational part of the calculus. Furthermore all the structural rules are admissible in the calculus introduced by Kanger in his classic "A simplified Proof Method for Elementary Logic". A crucial role for the proof of the above results is played by the pure and simple transcription in sequent form of (one of) the natural deduction elimination rules for equality, that, by itself, it would seem devoid of interest, as far as cut elimination and its consequences are concerned. The proofs are purely syntactic and apply both to the classic and intuitionistic case.