Derivability of the Archimedean axiom
This is a standard proof (it has been taken from PlanetMath). It is
formulated negatively so as to avoid the need for classical
logic. Using a proof of
{n | ~P n}+{forall n, P n}, we can in
principle also derive
up and its specification. The proof above
cannot be used for that purpose, since it relies on the
archimed axiom.