[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

Another possible answer is this:

    http://math.andrej.com/2012/10/03/am-i-a-constructive-mathematician/
    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.

Martin


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
http://www.cs.bham.ac.uk/~mhe