[Agda] Classical Mathematics for a Constructive World

[wren ng thornton]

On 12/1/12 9:32 PM, wren ng thornton wrote:
> If you consider the Russian constructivists to be correct ---i.e., that
> GMP is admissible when studying the sorts of objects they studied---,
> then the connection to continuity/compactness/etc is going to show up
> once you admit objects of study which cannot be exhaustively searched.
> Once you have such objects, the GMP begins to look rather dubious. It
> may be the case that for every proof p of (forall X. P X) we can
> construct some Y_p such that ¬(P Y_p). However, as indicated by the
> subscripting, the specific Y_p we come up with may depend on the exact
> structure of p. It need not be the case that, in the absence of the
> additional information that the content of p provides, we can identify
> some Y such that ¬(P Y).

Er, I missed a few negations in there. But hopefully the idea should be 
clear.

-- 
Live well,
~wren