| dc.rights.license | CC-BY-NC-ND | |
| dc.contributor.advisor | Oosten, Jaap van | |
| dc.contributor.author | Laan, Joost van der | |
| dc.date.accessioned | 2025-04-03T14:01:06Z | |
| dc.date.available | 2025-04-03T14:01:06Z | |
| dc.date.issued | 2025 | |
| dc.identifier.uri | https://studenttheses.uu.nl/handle/20.500.12932/48778 | |
| dc.description.abstract | Normalisation and cut elimination are methods used to perform combinatoral analysis on the structure
of formal proofs, while translations between proof systems are used to analyse and interpret the meaning
of proofs. In this thesis I will introduce two systems and their respective normal forms and demonstrate
how to perform translations between the systems which will preserve these normal forms.
This thesis also serves as an introduction to proof theory, In the first chapters the systems of natural
deduction, sequent calculus and their normal forms will be introduced from scratch. I
will also demonstrate an error with the cut elimination proof in [1] and give a correction, this serves as
an alternative to the correction given in [2]. | |
| dc.description.sponsorship | Utrecht University | |
| dc.language.iso | EN | |
| dc.subject | In my thesis I give an introduction to three different proof systems: Natural deduction, Sequent Calculus and Hilbert style systems and prove their equivalence. In the last part of this thesis I will introduce normal forms for sequent calculus and Natural deduction and demonstrate a correspondence between these normal forms. | |
| dc.title | Proof Systems and the Correspondence between Cut Elimination in Sequent Calculus and Normal forms in Natural Deduction | |
| dc.type.content | Bachelor Thesis | |
| dc.rights.accessrights | Open Access | |
| dc.subject.keywords | Sequent Calculus, Natural Deduction, Normalisation, Cut Elimination, Proof Theory, Proof Trees | |
| dc.subject.courseuu | Wiskunde | |
| dc.thesis.id | 19313 | |
