[Agda] Classical Mathematics for a Constructive World
Martin Escardo
m.escardo at cs.bham.ac.uk
Sun Nov 25 13:29:20 CET 2012
On 24/11/12 16:25, Peter Divianszky wrote:
> Is it true, that if one would use the double-negation monad, the
> computable finite pigeonhole principle could not be derived from the
> infinite one?
The point of the code is that we prove the classical infinite version
(with classical exists and or and ground propositions, and with
classical choice which requires the double negation shift) and then we
derive the finite version with intuitionistic quantifiers as a
consequence, which you can evaluate (as in the file Examples.hs).
See the slides
http://www.cs.bham.ac.uk/~mhe/.talks/mfps2011/mfps2011.pdf
Usually this is done as follows. Take a classical proof, use it to
derive a statement of the form (exists n : X. something decidable).
Then syntactically manipulate the classical proof to get an
intuitionistic proof and hence a realizer or program.
In the Agda file we avoid syntactical manipulations, by defining
K-exists and K-or quantitiers/connectives, and proving logical rules for
them and relations to exists and or. We embed classical logic in Agda so
that no syntactical translations are needed to extract programs. But
notice that in one file (three actually, but you need only on of them)
you have to disable the termination checker so that the proof of the
double-negation shift, needed to prove classical choice (i.e. choice
with K-exists rather than exists), is accepted.
Martin
More information about the Agda
mailing list