[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

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