Original title:
Aspekty věty o eliminovatelnosti řezů
Translated title:
Aspects of the Cut-Elimination Theorem
Authors:
Rýdl, Jiří ; Švejdar, Vítězslav (advisor) ; Bílková, Marta (referee) Document type: Bachelor's theses
Year:
2021
Language:
eng Abstract:
[eng][cze] 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].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]. Powered by TCPDF (www.tcpdf.org)
Keywords:
cut rule|sequent calculus|lengths of proofs; pravidlo řezu|sekventový kalkulus|délky důkazů
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/150414