[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

On 28/11/12 08:52, Peter Hancock wrote:

> I would be horrified to be shown a closed term of type N->N from
> which I could not read off a Turing machine and a(n internal) proof
> that it computes the denotation of the term in the standard mode.

But this is very different from the CT axioms you said. The above is a
meta-property, which is true, whether or not you postulate CT or
variations.

>     Incidentally, the same/similar goes for axioms of continuity at type
> "2", ie. (N->N)->N,
>     and even more so for axioms of extensionality at type 2.  I am *not*
>     sufficiently mad to expect strong forms of (a) Church's thesis and
> (b) continuity at type 2 both to
>     hold in the same model.

I am quoting the above because now you say:

> By the way, I for (the only?) one am not very sympathetic to all
> this stuff about "many worlds", coming from Andrej Bauer.

You have discussed two worlds above: the computable world, and the 
continuous world.

Then there is the pure world, in which one cannot (dis)prove that
functions are continuous or computable. I think Andrej called it the
politically correct world.

Best,
Martin