Speaker
Robin Martinot
Utrecht University
Talks at this conference:
Friday, 14:00, J431 
Philosophically motivated restrictions on formal proofs 
This talk reflects on how logical or mathematical proofs formalized in proof systems relate to philosophical properties of proof. We will take a relatively highlevel 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
