[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

> 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.

Thanks for the detailed explanation.

I have another question.
In the statement of the main theorem you use

₂ℕ : Set
₂ℕ = ℕ → ₂

which are the computable sequences of Booleans and
not all the classical sequences as I understand.
Should not the theorem be proved for classical sequences, provided that 
it is a translation of a classical theorem?

Peter