[Agda] Re: Agda Digest, Vol 73, Issue 2

[Valeria de Paiva]

Very cool note Martin!
I wish we had a snappy name for the minimalistic, non-contentious setting
that you've described, as it sure should be useful in many occasions.

Valeria

On Sat, Sep 3, 2011 at 3:00 AM, <agda-request at lists.chalmers.se> wrote:

> Send Agda mailing list submissions to
>        agda at lists.chalmers.se
>
> To subscribe or unsubscribe via the World Wide Web, visit
>        https://lists.chalmers.se/mailman/listinfo/agda
> or, via email, send a message with subject or body 'help' to
>        agda-request at lists.chalmers.se
>
> You can reach the person managing the list at
>        agda-owner at lists.chalmers.se
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Agda digest..."
>
>
> Today's Topics:
>
>   1. A proof of omniscience in Agda (Martin Escardo)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Fri, 02 Sep 2011 22:46:25 +0100
> From: Martin Escardo <m.escardo at cs.bham.ac.uk>
> Subject: [Agda] A proof of omniscience in Agda
> To: Agda mailing list <agda at lists.chalmers.se>
> Message-ID: <4E614EB1.2090105 at cs.bham.ac.uk>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
>
> The widely quoted Limited Principle of Omniscience (LPO) is not provable
> in constructive mathematics, and in particular in ML Type Theory (or in
> Agda, hopefully).
>
> However, if you enlarge the set of natural numbers with a point at
> infinity, then you get a set that constructively satisfies the principle
> of omniscience (in all varieties of constructive mathematics).
>
> Here is a proof written in Agda:
>
>
>
> http://www.cs.bham.ac.uk/~mhe/papers/omniscient/AnInfiniteOmniscientSet.html
>
> (Given my track record of using Agda in funny ways, I emphasize that
> this formal proof (1) doesn't disable the termination checker, (2)
> doesn't use postulates, (3) doesn't rely on translations of classical
> proofs into intuitionistic proofs, etc. It is in the purest possible
> fragment of Agda, corresponding to traditional ML Type Theory.)
>
> A proof in human notation is also available in a reference given in the
> above link.
>
> Best wishes,
> Martin
>
>
>
>
> ------------------------------
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> End of Agda Digest, Vol 73, Issue 2
> ***********************************
>



-- 
Valeria de Paiva
http://www.cs.bham.ac.uk/~vdp/
http://valeriadepaiva.org/www/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110903/57a1483e/attachment.html