Hans Grathwohl
(ILLC)
The Computational Content of Classical Proofs
April 19th at 17:30, in Science Park 107 F1.15
Proofs in intuitionistic logics have a strong computational flavour (think e.g. about the BHK-interpretation), which has made them very useful for computer scientists. However, evidence suggests that we should not discard classical proofs as being "non-computational". In the first part of this talk I will present a proof, using Friedman's A-translation technique, of Kreisel's classical result telling us that a large class of derivations in Peano Arithmetic can be transformed into derivations of the same statements in Heyting Arithmetic, thus eliminating any use of classical reasoning. This suggests that there is a connection between computation and some subset of classical logic. In the second part of the talk, I will explain why this is potentially useful, specifically I will explain what it means to extract a program from a proof, and what benefits one could obtain by using classical logics.
If time permits, I will tell a bit about Interactive Learning-Based Realizability, a new computational semantics for classical arithmetic which hopefully can be used to clarify how and when it is possible to extract programs from classical proofs.
This presentation aims to be accessible to anyone with an understanding of basic concepts from logic.