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