[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

So you use a variant of the infinite pigeonhole principle in which ₂ℕ is 
computable.
This is fine, I am impressed that you have got computational content 
from a very classical proof.
I guess in your example ₂ℕ should be computable.

Peter


On 25/11/2012 21:24, Martin Escardo wrote:
> 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
>