[FOM] Intuitionists and excluded-middle

[Jeremy Clark]

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.)

Regards,

Jeremy