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/ -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logica-l@dimap.ufrn.br> --- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLDpD%2B88Luv22n3btKOyh8%3DD932ewZ4Vi632-ZoEouotPA%40mail.gmail.com.
