[Agda] A proof of omniscience in Agda

[Martin Escardo]

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