[Agda] Classical Mathematics for a Constructive World
Martin Escardo
m.escardo at cs.bham.ac.uk
Sun Nov 25 19:35:31 CET 2012
On 25/11/12 13:06, Peter Divianszky wrote:
> 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?
One possible answer is this:
http://math.fau.edu/richman/HTML/CONSTRUC.HTM
Fred Richman
"Every theorem in constructive mathematics can be understood as
referring to the conventional universe of mathematical discourse,
and the proofs are acceptable within that universe. We do not
limit ourselves to a restricted class of "constructive objects""
Martin
More information about the Agda
mailing list