Programming with Classical Proofs
Hans Bugge Grathwohl
Abstract:
This thesis is about extracting programs from classical proofs. In the
first part, we show conservativity of Peano arithmetic over Heyting
arithmetic for Π02-sentences, an old result of Kreisel, using
Friedman’s A-translation technique. Then we present some extensions by
Parigot and Krebbers of the lambda-calculus with control mechanisms,
that allow for some amount of classical reasoning via the Curry–Howard
correspondence.
In the second part of the thesis, we present a new system by Aschieri
and Berardi, HA + EM1 , a Curry–Howard system for an arithmetic with a
limited amount of classical reasoning that is based on ideas from
their Interactive Realizability semantics for classical arithmetic. We
show Aschieri’s recent proof of strong normalization of HA + EM1 that
uses a new technique based on non-deterministic choice.
Two non-trivial examples of proof terms in HA+EM1 are then worked out,
and their possible reduction paths are analyzed. On basis of this, an
operational natural semantics for HA + EM1 is developed and tested on
the previous examples.
Keywords: Logic; Mathematics