[Agda] A proof of omniscience in Agda

[Martin Escardo]

I wrote a blog post in Andrej's Mathematics and Computation reporting 
part of what evolved from this since then, with lots of proofs in Agda:

http://math.andrej.com/2014/05/08/seemingly-impossible-proofs/

M.

On 02/09/11 22:46, Martin Escardo wrote:
> 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
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe