[FOM] Intuitionists and excluded-middle

[Jesse Alama]

Jeremy Clark <jeremy.clark at wanadoo.fr> writes:

> Just for the record, here is the constructive proof of the  
> irrationality of sqrt(2).
>
> Define x < y iff there is positive integer n s.t. y-x > 1/n.
> Define x neq y iff x<y or y<x (or equivalently abs(x-y) > 0).
> Define x irrational iff for all rational a/b, x neq a/b. (Note that  
> this is stronger than not(x=y).)
>
> Consider rational a/b. We can prove (by usual means) that a^2 - 2b^2  
> neq 0. (This is integer neq, of course.)
> Now,
>
> abs( a/b - sqrt(2) ) = abs( (a/b + sqrt(2)) )^-1 b^-2  abs (a^2 -  
> 2b^2) > ((abs(a)+2)b^2)^-1
>
> So we get a/b neq sqrt(2) for all rational a/b, so sqrt(2) is  
> irrational.

This is a nice argument.  The only thing that troubles me is the
comment that the disjunction

x < y or y < x

is equivalent to the inequality

abs(x - y) > 0.  What follows merely expresses my puzzlement about
this equivalence, viewed constructively; it doesn't impact your
argument since apparently you never use this characterization (instead
of taking the disjunctive characterization you take the "abs > 0"
characterization).

To establish this equivalent within a constructive proof system (say,
the intuitionistic Gentzen systems of Troelstra and Schwichtenberg's
_Basic Proof Theory_), we have to prove the implication

abs(x - y) > 0  ->  (x < y  or  y < x)

The bottom of the proof looks like

   abs(x - y) > 0  =>  x < y  or  y < x
------------------------------------------
=>  abs(x - y) > 0  ->  (x < y  or  y < x)

Unless this penultimate sequent is an axiom, I'm not sure how to get
the result constructively, since without loss of generality we can
imagine that we're working with a cut-free proof system with the
subformula property.  Another approach is to admit rules that
introduce, say, `abs', '>', '-', or some combination of these on the
left-hand side of sequents, for example, the rule:

  Given a derivation of the sequent

  X,x < y  or  y < x  =>  Y,

  (for sets of formulas X and Y) infer

  X,abs(x - y) > 0  =>  Y.

If we take either of these two approaches the absolute value function
gets short-shrift; one of its cute little properties, which has a
"non-trivial" classical proof, gets reduced to just an axiom or a rule
of inference.

There must be a reference on the constructive/intuitionistic
development of the absolute value function and its basic properties.
Where might I find it?

Jesse

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?

-- 
Jesse Alama (alama at stanford.edu)