Formalizing Ideals of Proof

Two broad observations lie at the basis of this dissertation, that finds itself at the intersection between philosophy, mathematics and proof theory. The first one is that mathematicians often prove a theorem in many different ways, even if they already believe in its validity. A specific strand of such motivations focuses on so-called ‘ideals’ of proof, which are particular conceptual properties that ‘good’ mathematical proofs are considered to possess. One main feature of this dissertation is its focus on ideals of proof. The second observation is that mathematics as well as logic deal with an inherent interplay between formal and informal notions, for which the right trade-off needs to be found. How formalization works, and what are exactly the differences between informal and formal concepts, are not well-understood. A second main feature of this dissertation is its interest in formalization of notions surrounding mathematical proofs. Bringing these two observations together, our aim is to define and compare several formalizations of ideals of proof. The main results of this dissertation concern three ideals of proof: that of purity (as opposed to impurity), explanation (concerning proofs that explain, versus proofs that do not), and semantic pollution (as opposed to syntactic purity). A first contribution of this dissertation is its relatively large-scale comparison of various models of purity and explanation (for informal proofs), relative to a case study of two particular informal proofs. Included in this comparison, and forming the second main contribution of this dissertation, is the introduction of a new model of purity to the literature, namely that of ontological purity. We define this model of purity not only on the level of informal proofs, but additionally for formalized (natural deduction) proofs. In doing this, we show that the combination of mathematical tools (such as Visser (1997)’s interpretation translation) with philosophical perspectives (like mathematical structuralism (Shapiro, 1997)) can lead to successful formalizations. Third, we introduce an elaborate conceptual and formal understanding of semantic pollution, an ideal that is mentioned widely throughout proof-theoretic literature in connection to ‘labeled’ proof systems, but has not often been considered closely. This involves a case study of proof systems for modal logic, in particular various generalizations of usual sequent calculi — as well as accompanying Kripke models and the notions of equivalence that relate them. We take a range of proof-theoretic languages as objects of study, and we report a first systematic analysis of these languages under our measures of semantic pollution (where labeled languages emerge as relatively highly semantically polluted).