View Item 
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of UU Student Theses RepositoryBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

        Proof Systems and the Correspondence between Cut Elimination in Sequent Calculus and Normal forms in Natural Deduction

        Thumbnail
        View/Open
        Thesis.pdf (524.4Kb)
        Publication date
        2025
        Author
        Laan, Joost van der
        Metadata
        Show full item record
        Summary
        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].
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/48778
        Collections
        • Theses
        Utrecht university logo