[Agda] Classical Mathematics for a Constructive World
Peter Hancock
hancock at spamcop.net
Sun Nov 25 20:03:24 CET 2012
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).
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.
So, not a yes/no answer. What do you think?
Peter
More information about the Agda
mailing list