Rule-Elimination Theorems by Sayantan Roy / LUWebinar Sept 25, 2024, 4pm CET

[jean-yves beziau]

Speaker: Sayantan Roy  (Indraprastha Institute of Information Technology, Delhi, India)

Title: Rule-Elimination Theorems

Abstract: Cut-elimination theorems constitute one of the most important

classes of theorems of proof theory. Since Gentzen’s proof of the
cut-elimination theorem for the system LK, several other proofs have
been proposed. Even though the techniques of these proofs can be modified
to sequent systems other than LK, they are essentially of a very
particular nature; each of them describes an algorithm to transform a
given proof to a cut-free proof. However, due to its reliance on heavy
syntactic arguments and case distinctions, such an algorithm makes the
fundamental structure of the  argument rather opaque . We, therefore,
consider rules abstractly, within the framework of logical structures familiar
from universal logic  and aim to clarify the
essence of the so-called “elimination theorems”. To do this, we first
give a non-algorithmic proof of the cut-elimination theorem for the
propositional fragment of LK. From this proof, we abstract the essential
features of the argument and define something called normal sequent
structures relative to a particular rule. We then prove a version of the
rule-elimination theorem for these. Abstracting even more, we define
abstract sequent structures and show that for these structures, the corresponding
version of the rule-elimination theorem has a converse as well.

https://link.springer.com/journal/11787

Associate Organization

ERC (European Research Council) 

Advanced project on Proof Systems

Presented by its director  Andrzej Indrzejczak (University of Łódź, Poland)

Chair: Francesco Paoli (Editorial Board SUL)

Everybody is welcome to join, register here

https://cassyni.com/s/logica-universalis/seminars

>-----------------------------------------------------------------------

Jean-Yves Beziau

Editor-in-Chief Logica Universalis

Organizer Logica Universalis Webinar

https://www.jyb-logic.org/