[Agda] Classical Mathematics for a Constructive World
Peter Divianszky
divipp at gmail.com
Sun Nov 25 23:36:35 CET 2012
On 25/11/2012 20:03, Peter Hancock wrote:
> Some thoughts prompted by your question.
>
>> 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?
>
> 1. If we wanted to prove something specifically about computable
> sequences, then we could either prove it about
> a. sequences for which there is a turing machine computing
> extensionally the same function.
> b. sequences for which it is not absurd that there exists...(ditto).
I am a bit confused.
Is
ℕ → ₂
not the space of computable functions from ℕ to ₂?
Are ℕ → ₂, a. and b. three different things, given that the domain is ℕ
and the image is ₂ ?
Could you highlight the difference?
> 2. What is a classical sequence? Conceivably, it is a relation between
> Nat and 2 for which it is
> not absurd that it is total. Maybe this gets us into problems with
> predicativity; because
> quantifying over relations is (from a predicative p.o.v) like
> quantifying over proper classes.
> As far as I know, predicativity makes sense classically.
I guess "a relation between Nat and 2 for which it is not absurd that it
is total" gives the same interpretation for classical sequences as the
one with "weak values" in the paper "Classical Mathematics for a
Constructive World".
Is there a question about predicativity here? I just would like to
translate the infinite pigeonhole principle to Agda as honest as I can.
> So, not a yes/no answer. What do you think?
>
> Peter
>
More information about the Agda
mailing list