[Agda] If all functions (N->N)->N are continuous, then 0=1.

[Altenkirch Thorsten]

I am puzzled again!

Clearly, this formulation of continuity is inconsistent with functional
extensionality because it makes it possible to observe an intensional
property of a function - its modulus of continuity. What is surprising is
that you manage to derive a contradiction w.o. using ext! So the wrong
formulation of continuity doesn't even work in vanilla intensional Type
Theory. 

Thorsten

On 27/11/2013 21:56, "Martin Escardo" <m.escardo at cs.bham.ac.uk> wrote:

>
>
>
>   If all functions (N->N)->N are continuous, then 0=1.

That is a bit of a lie. What you are saying is if for all functions we
know why they are continuous, then 0=1.

I mean "is continuous" does sound like a proposition, doesn't it?

>
>
>
>Think of functions a : N -> N as sequences of natural numbers:
>
>    a 0, a 1, a 2, a 3, ..., a n, ...
>
>The "continuity axiom" for functions
>
>     f : (N -> N) -> N,
>
>that map sequences a : N -> N to numbers f(a), going back to Brouwer
>in his intuitionistic mathematics in the early 20th century, says that
>the value f(a) can depend only on a finite prefix of the infinite
>argument a.
>
>This makes sense computationally: there are no crystal balls in
>computational processes, able to see and grasp the infinite input at
>once. The input of f is computed bit-by-bit, in fact, often only when
>f queries it.
>
>After finitely many queries to its argument a : N -> N, the function f
>is supposed to deliver its answer, if it's ever going to produce an
>answer.
>
>When this finiteness condition holds, we say that f is continuous
>(never mind the reason for the terminology "continuous" in this message).
>
>The link
>
>   http://www.cs.bham.ac.uk/~mhe/continuity-false/continuity-false.html
>
>writes down Brouwer's formulation of continuity in Agda notation, and
>proves that:
>
>   If all functions (N->N)->N are continuous, then 0=1.
>
>What is going on? There is some discussion in the above link.
>
>You may wish to read Andrej Bauer's related discussion
>http://math.andrej.com/2011/07/27/definability-and-extensionality-of-the-m
>odulus-of-continuity-functional/
>
>The ideas of http://homotopytypetheory.org/book/ are relevant in this
>respect too. To solve the apparent paradox, think about how one can
>constructively prove existence without disclosing witnesses. Doubly
>negated existence is too weak. One needs a stronger, constructive
>notion of existence that deliberately doesn't exhibit witness, which
>sometimes, but not always, can get to be disclosed. I attended a nice
>talk by Thierry Coquand yesterday, in which he showed how the "axiom
>of description" explains when and how the secret can be constructively
>disclosed. In the HoTT book, this is explained as the axiom of unique
>choice.
>
>NB. Only the purest form of intensional Martin-Loef Type Theory is
>used in the above Agda proof, and no universes are needed. No HoTT
>axioms in particular.
>
>Best, Martin
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.