Robin Martinot

This paper provides a formal characterization of the phenomenon of ‘semantic pollution’ relative to proof systems for modal logic and Kripke semantics. We propose that semantic pollution can be made precise by several properties of syntax occurring in proof systems. First, our base requirement for semantic pollution is given by the property of violating invariance results under Kripke model equivalences. On top of that, the distinction between local and global syntax, and between syntax that is dependent on and independent from the propositional valuation, induce four levels of semantic pollution: weak pollution, global pollution, local pollution and strong pollution. We analyze several main proof systems for (extensions of) modal logic in terms of these levels of pollution: the display calculus, the hybrid calculus and the labeled calculus. The results show that the display calculus is only weakly semantically polluted, while the hybrid calculus has formulas introducing several types of pollution. The only calculus that is strongly semantically polluted is the labeled calculus. These formal results are in line with general intuitions about semantic pollution. Additionally, our formal framework for semantic pollution is suitable for applications to other logics and semantics. Finally, we comment on the relation of our framework to the philosophical debate surrounding semantic pollution.

This paper systematically studies the connections between purity and explanation of mathematical proofs. We consider a well-known proof of Pythagoras’s Theorem which is considered explanatory, and Euclid’s proof of the Infinitude of Primes which is considered pure. We apply the best-known models of purity to the former proof, and the best-known models of explanation to the latter proof. Results show that, contrary to an illustrious tradition going back to Aristotle where purity and explanation are deeply interconnected, most contemporary approaches separate purity and explanation. We conclude the paper by analysing a recent approach to explanation where explanation and purity reunite.

Purity is known as an ideal of proof that restricts a proof to notions belonging to the ‘content’ of the theorem. In this paper, our main interest is to develop a conception of purity for formal (natural deduction) proofs. We develop two new notions of purity: one based on an ontological notion of the content of a theorem, and one based on the notions of surrogate ontological content and structural content. From there, we characterize which (classical) first-order natural deduction proofs of a mathematical theorem are pure. Formal proofs that refer to the ontological content of a theorem will be called ‘fully ontologically pure’. Formal proofs that refer to a surrogate ontological content of a theorem will be called ‘secondarily ontologically pure’, because they preserve the structural content of a theorem. We will use interpretations between theories to develop a proof-theoretic criterion that guarantees secondary ontological purity for formal proofs.