[FOM] Intuitionists and excluded-middle
jeremy.clark at wanadoo.fr
Tue Oct 25 03:26:48 EDT 2005
On Oct 24, 2005, at 11:01 pm, Jesse Alama wrote:
> There must be a reference on the constructive/intuitionistic
> development of the absolute value function and its basic properties.
> Where might I find it?
Bishop and Bridges' "Constructive Analysis" for example. The
development is not at all axiomatic, so e.g. the abs function is
defined for constructive reals, and then from the definition it is
easy to prove abs(x)>0 => x neq 0. A constructive real is basically a
Cauchy sequence of rational numbers so it is easy to show that if x
neq 0 then x>0 or x<0.
> PS Although intuitively your "neq" is stronger than "not =", this may
> be only an appearance. Constructivist query: is the trichotomy
> law for real numbers admitted?
Absolument pas! So yes, the constructive neq is stronger than "not
=". (Though they are classically equivalent of course.)
More information about the FOM