Rule-Elimination Theorems - presented by Sayantan Roy | ExtenDD. Coming to Terms: Proof Theory Extended to Definite Descriptions and other Terms - presented by Prof. Andrzej Indrzejczak

Rule-Elimination Theorems

Sayantan Roy

ExtenDD. Coming to Terms: Proof Theory Extended to Definite Descriptions and other Terms

Prof. Andrzej Indrzejczak

Prof. Andrzej IndrzejczakSayantan Roy
1. Rule-Elimination Theorems
Sayantan Roy
Sayantan Roy
Indraprastha Institute of Information Technology Delhi

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.

2. ExtenDD. Coming to Terms: Proof Theory Extended to Definite Descriptions and other Terms
Prof. Andrzej Indrzejczak
Andrzej Indrzejczak
University of Łódź
No abstract was provided for this talk.
Logica Universalis logo
Logica Universalis Webinar
Logica Universalis
Cite as
A. Indrzejczak and S. Roy (2024, September 25), Rule-Elimination Theorems, ExtenDD. Coming to Terms: Proof Theory Extended to Definite Descriptions and other Terms
Share
Details
Listed seminar This seminar is open to all
Recorded Available to all
Video length 1:15:07
Q&A Now closed
Disclaimer The views expressed in this seminar are those of the speakers and not necessarily those of the journal