Eduardo Ugalde-Reyes

This dissertation investigates the proof-theoretic significance of normalization for intuitionistic propositional logic in the system of natural deduction with general elimination rules, NG. Its guiding idea is that logic can function as epistemology in laboratory conditions: the epistemic role of proof is best understood not through an external theory of truth, but through the internal analysis of proof construction, verification, and transformation. The central technical problem concerns the strong normalization of NG. The dissertation compares two approaches to this problem: the diagrammatic strategy developed by Negri and von Plato, and the algebraic method of Joachimski and Matthes for the corresponding λJ calculus. This comparison is used to clarify the relation between proof threads, proof terms, conversion schemes, and the computational behavior of derivations under the Curry–Howard correspondence. To this end, the dissertation develops formal machinery for the analysis of NG. It presents the relevant convertibilities—détours, permutabilities, and simplifications—compares ordinary natural deduction with NG, introduces a typed formulation of NG, and reconstructs the translation between diagrammatic derivations and λJ proof terms. This reverse engineering makes explicit how the combinatorial behavior of conversion schemes can be studied through the linearized syntax of proof terms. The dissertation contributes to structural proof theory by clarifying the normalization problem for NG, systematizing its conversion schemes, and connecting its diagrammatic presentation with the algebraic methods of the lambda calculus. It also contributes to interpretational proof theory by showing how questions about proof, verification, and mathematical practice can be pursued through concrete metatheoretical work. In this way, it offers a bridge between natural deduction, sequent-style formulations, typed proof terms, and computational interpretations of intuitionistic logic.