[Agda] Classical Mathematics for a Constructive World

[Altenkirch Thorsten]

On 28/11/2012 08:52, "Peter Hancock" <hancock at spamcop.net> wrote:

>Now, my question, such as it was.  Something I got from rereading an
>ancient
>book by Troelstra, is essentially this:
>
>   SCT + EXT2 + AC are jointly inconsistent over HAomega
>
>EXT2 is extensionality at type (N->N)->N.
>I also saw something like this in Beeson's book.  Troelstra indicates that
>from these 3 ingredients one could solve the halting problem.  He mentions
>that a proof can also be constructed from the Kreisel-Lacombe-Shoenfield
>theorem (from 1959).
>I was surprised that SCT is so hostile, even to extensionality.
>Univalence apparantly
>implies EXT2 inter alia, and is compatible with AC.

Isn't this just the observation that from these 3 assumptions we can
decide extensional equality of functions f : N -> N because using SCT + AC
we get a function code : (N -> N) -> N  such that code f = code g <-> f =
g?

>Similar things can be formulated for continuity at type 2, where the
>thing that is said to "exist"
>is roughly speaking a well-founded countably-branching tree that
>represents the type2 functional
>a la Ghani/Hancock/Pattinson or Escardo.


I agree that continuity is similar to CT because it reflects the fact that
we talking about computable functions only. One may think that they are
inconsistent because the FAN principle and CT are jointly inconsistent
(due to the construction of the Kleene tree). However, does this also work
when we have WCT or WhCT? Indeed CT corresponds to the ability to observe
directly the well-founded tree corresponding to a computation of type 2
which is also inconsistent with Ext.

Thorsten

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.