Aspects of the Cut-Elimination Theorem

• Název práce v češtině: Aspekty věty o eliminovatelnosti řezů
• Název v anglickém jazyce: Aspects of the Cut-Elimination Theorem
• Klíčová slova: pravidlo řezu|sekventový kalkulus|délky důkazů
• Klíčová slova anglicky: cut rule|sequent calculus|lengths of proofs
• Akademický rok vypsání: 2020/2021
• Typ práce: bakalářská práce
• Jazyk práce: angličtina
• Ústav: Katedra logiky (21-KLOG)
• Vedoucí / školitel: doc. RNDr. Vítězslav Švejdar, CSc.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 21.12.2020
• Datum zadání: 21.12.2020
• Schválení administrátorem: zatím neschvalováno
• Datum potvrzení stud. oddělením: 21.12.2020
• Datum a čas obhajoby: 07.09.2021 10:00
• Datum odevzdání elektronické podoby: 29.07.2021
• Datum proběhlé obhajoby: 07.09.2021
• Odevzdaná/finalizovaná: odevzdaná pracovníkem v zastoupení a finalizovaná
• Oponenti: Mgr. Marta Bílková, Ph.D.

Zásady pro vypracování

Consider various proofs of the cut-elimination theorem existing in the literature. The proof in [Tak75] works also for intuitionistic logic. [Sch77] contains a proof that does not mention intuitionistic logic, works with a special (substantially reduced) calculus, but it also yields an upper bound for the size of the depth of the proof obtained by eliminating cuts. The two proofs differ in the definition of cut rank. Schwichtenberg's proof, including the upper bound, can be adjusted for a classical calculus close to that developed in [Tak75]. This fact was elaborated in Ivo Kylar's master's thesis and can be found in [Šve02].
Investigate the known proofs and compare the different approaches. Try to explore the differences in technicalities. Variants of calculi (whether a sequent is a pair of sequences, a pair of sets, or a pair of multisets) may be inconsequential, but the role of the different definitions of cut rank is less clear. Can the proof in [Šve02] be adjusted for intuitionistic logic? Here both single-succedent and multi-succedent calculi can be taken into account.
Optionally consider other sources and related problems. The upper bound in Buss' chapter [Bus98b] is very similar to that in [Sch77] (that is, it is superexponential as well) but it is not exactly the same. What is the cause? Are there other ways of obtaining the lower bound than that invented by Pudlák and published in [Pud98]? What are the quantitative aspects of the midsequent theorem? What is an efficient way of proving the cut-elimination theorem for provability logic?

Seznam odborné literatury

[Bus98a] S. R. Buss, editor. Handbook of Proof Theory. Number 137 in Studies in Logic and the Foundations of Mathematics. Elsevier, 1998.
[Bus98b] S. R. Buss. An introduction to proof theory. In Handbook of Proof Theory [Bus98a], chapter I, pages 1–78.
[GR08] R. Goré and R. Ramanayake. Valentini’s cut-elimination for provability logic resolved. In C. Areces and R. Goldblatt, editors, Advances in Modal Logic 7 (AiML’08 Nancy), pages 67–86. College Publications, London, 2008.
[Jur06] D. Jurenka. Věta o středním sekventu v jednotlivých variantách gentzenovského kalkulu (The Midsequent Theorem in Different Variants of Calculi). Seminar paper, School of Arts, Dept. of Logic, Charles Univ. in Prague, 2006.
[Pud98] P. Pudlák. The lengths of proofs. In Buss [Bus98a], chapter VIII, pages 547–637.
[Sch77] H. Schwichtenberg. Proof theory. In J. Barwise, editor, Handbook of Mathematical Logic, chapter D.2, pages 867–896. North-Holland, 1977.
[Šve02] V. Švejdar. Logika: neúplnost, složitost a nutnost (Logic: Incompleteness, Complexity, and Necessity). Academia, Praha, 2002.
[Tak75] G. Takeuti. Proof Theory. North-Holland, 1975.
[TS96] A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 1996.