Eduardo Ugalde-Reyes

Turing progressions arise by iteratedly adding consistency statements to a base theory. Different notions of consistency give rise to different Turing progressions. In this paper we present a logic that generates exactly all relations that hold between these different Turing progressions given a particular set of natural consistency notions. Thus, the presented logic is proven to be arithmetically sound and complete for a natural interpretation, named the formalized Turing progressions (FTP) interpretation.

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.