This talk reflects on how logical or mathematical proofs formalized in proof systems relate to philosophical properties of proof.
Generally, the existence of a formalized proof is taken as a standard for correctness (called the standard view in the literature, see e.g. [1]). But formal proofs are conceptually still far-removed from informal proofs (proofs in the way they are actually carried out), and not much is known about their specific relation. For instance, the derivation-indicator view [2] says that a mathematical proof ‘indicates’ an underlying formalized derivation, but how exactly this should happen is unclear.

We will take a relatively high-level strategy to relate informal proofs to formalized derivations, and restrict ourselves to two case studies. The first suggests that we can zoom in on a particular philosophical property that an informal proof possesses, and see how it can be made precise in the formal setting. A case study of this approach is [3], concerning purity of proof; studies can also be found, among others, for the properties of explanation and simplicity of proof. Here, formalized proofs that satisfy a precisified requirement for purity can be taken as corresponding more closely to pure informal proofs of the same theorem.

For the second case study, we take a step back, and differentiate between the types of proof systems in which a proof can be formalized. In particular, a myriad of proof systems exist nowadays for modal logic, which extend the basic modal language in a variety of ways. We may wonder whether all such extensions can provide acceptable formalizations of modal reasoning. The phenomenon of ‘semantic pollution’ of proof systems, most intuitively described as ‘bringing Kripke semantics into the proof system’, is potentially problematic for faithful formalization. We will also consider this property more closely, and present possible formal criteria for it.

Bibliography

1. Avigad, Jeremy,Reliability of mathematical inference,Synthese,vol. 198 (2021), no. 8, pp. 7377–7399.
2. Azzouni, Jody,The derivation-indicator view of mathematical practice,Philosophia Mathematica,vol. 12 (2004), no. 2, pp. 81–106.
3. Martinot, Robin,Ontological Purity for Formal Proofs,The Review of Symbolic Logic,2023, pp. 1–40.
4. Stra{\ss}burger, Lutz,Proof nets and the identity of proofs,arXiv preprint cs/0610123,2006.