[Agda] Classical Mathematics for a Constructive World

Martin Escardo m.escardo at cs.bham.ac.uk
Sun Nov 25 21:24:52 CET 2012

Another possible answer is this:

    Andrej Bauer

    "there are many worlds of mathematics, and the view of the worlds
    is relative to which one I am in"

I agree with both Andrej and Fred.


On 25/11/12 18:35, Martin Escardo wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

Martin Escardo

More information about the Agda mailing list