Mabel Najdovski: Extracting computational content from classical proofs

Abstract: Classical logic often allows us to produce very short and elegant proofs. However, since reasoning principles like the law of excluded middle (LEM) cannot be given a direct computational intepretation, neither can proofs that employ it. Nonetheless, by a careful examination of the rules of logic, the usage of LEM can often be mechanically eliminated, yielding constructive proofs (and thus algrithms) from classical ones.

This process is often explained through the lens of Gödel's double negation translation, which we will review. However, the resulting algorhithms are implemented in a continuation passing style, making their computational behavior hard to understand.

In this talk, we will turn to a very different explanation, stemming from cut elimination in the sequent calculus. We will first present the sequent calculus in its usual form and discuss the connection between cut elimination and computation in this system. We will then present a certain one-sided infinitary sequent calculus and show how cut elimination in this system can yield a form of program extraction from classical proofs.