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

[Altenkirch Thorsten]

I would put it rather positively: Type Theory enables us to have two
different forms of existence: the proof-relevant one which corresponds to
the statement "there exists" and which isn't necessarily a proposition and
the proof-irrelevant one which (following Mile Shulmann) we can paraphrase
as "there merely exists".

Hence we know that type-theoretically the correct way to express
continuity is using "merely exists" but not "exists". Actually a similar
situation arises which Church thesis which should say for every function
there merely exists a code which realizes it.

One is left wondering wether there is a better way expressing these
principles since propositional principles feel a bit alien in type theory.

Thorsten

On 28/11/2013 09:57, "Thierry Coquand" <Thierry.Coquand at cse.gu.se> wrote:

>
> It is tempting to have the following argument
>
> -when Brouwer formulated the continuity axiom, expressed in Martin's
>message as
>"the value f(a) can depend only on a finite prefix of the infinite
>argument a"  which can be reformulated as "there exists n such that if a
>k = b k
>for all k<n then f(a) = f(b)" this existence statement was understood
>intuitionistically
>
> -hence Martin's message shows that one cannot express
>constructive/intuitionistic
>existence using sigma types
>
> Thierry
>
>On Nov 28, 2013, at 9:28 AM, Altenkirch Thorsten wrote:
>
>> 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.
>> 
>> 
>> 
>> 
>> _______________________________________________
>> 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.