A Formal Characterization of Semantic Pollution of Modal Proof Systems

Abstract 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.