27 Nov 22:56 2013

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

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

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

When this finiteness condition holds, we say that f is continuous
(never mind the reason for the terminology "continuous" in this message).

```

28 Nov 09:28 2013

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

```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@...> 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, ...
>
```

28 Nov 10:52 2013

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

```
On 28/11/13 08:28, Altenkirch Thorsten wrote:
> 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.

That's indeed one the points:

>> 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.

(And no function extensionality in particular, as remarked in the

But the main point is that the interpretation Sigma of "exists" is not
always what we want (which is well known among a number of people).

Here is another (well known) example. If you define the image of a
function f : X -> Y to be

im f = Sigma(y : Y).Sigma(x : X). f x = y,  (wrong),

then you get that im f is pointwise isomorphic to X. This is so even
if all elements of X are mapped to the same element y0 of Y. What one
needs is to hide some information, but not all:

```

28 Nov 14:59 2013

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

```
On 28/11/13 08:28, Altenkirch Thorsten wrote:
> I am puzzled again!
>
> you manage to derive a contradiction w.o. using ext!

This has nothing to do with extensionality.

My one-sentence summary is this:

Finding a continuity witness is a non-continuous operation.

No finite part of f:(N->N)->N is enough to find out which finite part
of a:N->N suffices to compute f(a).

The formulation of continuity, using Sigma, both

(1) says that all functions are continuous, and
(2) provides a continuity-witness-finder.

The proof of 0=1 works by defining a non-continuous function using the
hypothetical continuity-witness-finder (2), thus contradicting (1).

Martin
```
30 Nov 03:10 2013

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

On Thu, Nov 28, 2013 at 2:59 PM, Martin Escardo wrote:

My one-sentence summary is this:

Finding a continuity witness is a non-continuous operation.

No finite part of f:(N->N)->N is enough to find out which finite part
of a:N->N suffices to compute f(a).

What would be an explicit definition of "finite part" for elements of (N -> N) -> N? Or, in other words, what's a good intuition for the topology of that type?

Andrea

The formulation of continuity, using Sigma, both

(1) says that all functions are continuous, and
(2) provides a continuity-witness-finder.

The proof of 0=1 works by defining a non-continuous function using the
hypothetical continuity-witness-finder (2), thus contradicting (1).

Martin
_______________________________________________
Agda mailing list
Agda-TrQ0NnR75ays1BDpvl8NfQ@public.gmane.orgmers.se
https://lists.chalmers.se/mailman/listinfo/agda

```_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
```
1 Dec 22:24 2013

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

```
On 30/11/13 02:10, Andrea Vezzosi wrote:
> On Thu, Nov 28, 2013 at 2:59 PM, Martin Escardo <m.escardo@...
> <mailto:m.escardo@...>> wrote:
>
>
>     My one-sentence summary is this:
>
>         Finding a continuity witness is a non-continuous operation.
>
>     No finite part of f:(N->N)->N is enough to find out which finite part
>     of a:N->N suffices to compute f(a).
>
>
> What would be an explicit definition of "finite part" for elements of (N
> -> N) -> N? Or, in other words, what's a good intuition for the topology
> of that type?

Sorry, I missed this question.

The topology of the type (N->N)->N is rather complicated in terms of
open sets. In terms of finiteness, an approach using domain theory is
natural, but requires a number of definitions and proofs before we can
say it.

Moreover, it is hard to formulate such things
constructively. Chuangjie Xu and I have done some work on this.

If you ignore constructivity, which can be useful for a rough (and
distorted) understanding, it is easier to think in terms of
convergent sequences. We say that a sequence f_i in (N->N)->N
converges to g if whenever a sequence a_i in N->N converges to b, then
the sequence f_i(a_i) converges to g(b).

So you still need to explain convergence in N->N. We say that a
sequence a_i in N->N convergers to b if for every n there is j such
that all a_i, for i>=j, agree with b in the first n positions.

Then the problem with the modulus-of-continuity functional is that it
doesn't preserve limits (it is not continuous).

If you want to know more, please feel free to ask. There are models of
type theory (classical and constructive) based on the above ideas. One
of them is Johnstone's topological topos. A closely related one,
studied by Chuangjie and myself, admits a constructive treatment.

Best,
Martin
```
4 Dec 07:22 2013

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

On Sun, Dec 1, 2013 at 10:24 PM, Martin Escardo wrote:
[...]
Then the problem with the modulus-of-continuity functional is that it
doesn't preserve limits (it is not continuous).

Does this mean that once we fix a modulus of continuity functional M we should be able to find a sequence f_i of continuous functions converging to g such that M f_i doesn't converge to M g? All without assuming M itself to be continuous?

It could be an interesting example.

If you want to know more, please feel free to ask. There are models of
type theory (classical and constructive) based on the above ideas. One
of them is Johnstone's topological topos. A closely related one,
studied by Chuangjie and myself, admits a constructive treatment.

What's a good article to start from for the constructive model?

-- Andrea

Best,

Martin

_______________________________________________
Agda mailing list
Agda-TrQ0NnR75ays1BDpvl8NfQ@public.gmane.orgmers.se
https://lists.chalmers.se/mailman/listinfo/agda

```_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
```

Gmane