Aspects of the Cut-Elimination Theorem
Aspekty věty o eliminovatelnosti řezů
bakalářská práce (OBHÁJENO)
Zobrazit/ otevřít
Trvalý odkaz
http://hdl.handle.net/20.500.11956/150414Identifikátory
SIS: 232267
Kolekce
- Kvalifikační práce [23279]
Autor
Vedoucí práce
Oponent práce
Bílková, Marta
Fakulta / součást
Filozofická fakulta
Obor
Logika
Katedra / ústav / klinika
Katedra logiky
Datum obhajoby
7. 9. 2021
Nakladatel
Univerzita Karlova, Filozofická fakultaJazyk
Angličtina
Známka
Výborně
Klíčová slova (česky)
pravidlo řezu|sekventový kalkulus|délky důkazůKlíčová slova (anglicky)
cut rule|sequent calculus|lengths of proofsI give a proof of the cut-elimination theorem (Gentzen's Hauptsatz) for an intuitionistic multi-succedent calculus. The proof follows the strategy of eliminating topmost maximal-rank cuts that allows for a straightforward way to measure the upper bound of the increase of derivations during the procedure. The elimination of all cut inferences generates a superexponential increase. I follow the structure of the proof for classical logic given in Švejdar's [18], modifying only the critical cases related to two restricted rules. Motivated by the diversity found in the early literature on this topic, I survey selected aspects of various formulations of sequent calculi. These are reflected in the proof of the Hauptsatz and its preliminaries. In the end I give one corollary of cut elimination, the Midsequent theorem, which is one of the three applications to be found already in Gentzen's [10]. Powered by TCPDF (www.tcpdf.org)
I give a proof of the cut-elimination theorem (Gentzen's Hauptsatz ) for an intuitionistic multi-succedent calculus. The proof follows the strategy of eliminating topmost maximal-rank cuts that allows for a straightforward way to measure the upper bound of the increase of derivations during the procedure. The elimination of all cut inferences generates a superexponential increase. I follow the structure of the proof for classical logic given in Švejdar's [18], modifying only the critical cases related to two restricted rules. Motivated by the diversity found in the early literature on this topic, I survey selected aspects of various formulations of sequent calculi. These are reflected in the proof of the Hauptsatz and its preliminaries. In the end I give one corollary of cut elimination, the Midsequent theorem, which is one of the three applications to be found already in Gentzen's [10].