Constructivisation through Induction and Conservation

The topic of this thesis lies in the intersection between proof theory and algebraic logic. The main object of discussion, constructive reasoning, was introduced at the beginning of the 20th century by Brouwer, who followed Kant’s explanation of human intuition of spacial forms and time points: these are constructed step by step in a finite process by certain rules, mimicking constructions with straightedge and compass and the construction of natural numbers, respectively. The aim of the present thesis is to show how classical reasoning, which admits some forms of indirect reasoning, can be made more constructive. The central tool that we are using are induction principles, methods that capture infinite collections of objects by considering their process of generation instead of the whole class. We start by studying the interplay between certain structures that satisfy induction and the calculi for some non-classical logics. We then use inductive methods to prove a few conservation theorems, which contribute to answering the question of which parts of classical logic and mathematics can be made constructive.