[FOM] Intuitionists and excluded-middle
Jesse Alama
alama at stanford.edu
Mon Oct 24 17:01:05 EDT 2005
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)
More information about the FOM
mailing list