Ulrich Berger
(Swansea, Great Britain)
On the computational interpretation of classical analysis
Data: 13 de Setembro de 2006
Local: 5.5.
Hora: 14h
Resumo
We discuss the proof-theoretic and computational properties
of open induction, a principle which is classically
equivalent to dependent choice and hence contains full
classical analysis. We show that, intuitionistically, open
induction and dependent choice are quite different: While
dependent choice is conservative over intuitionistic
arithmetic, open induction is intuitionistically as strong
as classically. Via modified realizability we obtain a new
direct method for extracting programs from classical proofs
of Pi^0_2-formulas using open induction. We also show that
the computational interpretation of classical countable
choice given by Berardi, Bezem and Coquand can be derived
from our results.
Este seminário é organizado com apoio do CMUC.
Reinhard Kahle, 15.09.06