Aspects of the Cut-Elimination Theorem

• Thesis title in Czech: Aspekty věty o eliminovatelnosti řezů
• Thesis title in English: Aspects of the Cut-Elimination Theorem
• Key words: pravidlo řezu|sekventový kalkulus|délky důkazů
• English key words: cut rule|sequent calculus|lengths of proofs
• Academic year of topic announcement: 2020/2021
• Thesis type: Bachelor's thesis
• Thesis language: angličtina
• Department: Department of Logic (21-KLOG)
• Supervisor: doc. RNDr. Vítězslav Švejdar, CSc.
• Author: hidden - assigned and confirmed by the Study Dept.
• Date of registration: 21.12.2020
• Date of assignment: 21.12.2020
• Administrator's approval: not processed yet
• Confirmed by Study dept. on: 21.12.2020
• Date and time of defence: 07.09.2021 10:00
• Date of electronic submission: 29.07.2021
• Date of proceeded defence: 07.09.2021
• Submitted/finalized: committed by worker on behalf on and finalized
• Opponents: Mgr. Marta Bílková, Ph.D.

Guidelines

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?

References

[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.