"A good example of this is by proving that 
is irrational. Proving this directly (via constructive proof) would probably be very difficult--if not impossible."
found here: http://en.wikibooks.org/wiki/Mathematical_Proof/Methods_of_Proof/Proof_by_Contradiction
I suppose this is why you were asking, because it does not appear to be readily available.
Why do you want a constructive proof?
Lots of interesting proofs related to sqrt(2) on wikipedia.
Constructive proofs seem to be in short supply on this one.
I agree with what others have said. Off the top of my head I do not know of a direct proof. I am not really sure that if you had a direct/constructive proof that it would nessasarily give you anything more that the proof by contradiction does.
Here is a constructive proof.
It is easy to show that the continued fraction for sqrt(2) is infinite, in fact a recurrence relationship proves:
This proves sqrt(2) is irrational, since all non-terminating continued fractions are irrational (it's easy to show the continued fractions for rationals terminate, which proves this).
I have of course read the traditional proof by contradiction along time ago (as have many schoolboys heard of it), but I have looked hard for the constructive version and have not been able to find one.
What Elroch says is interesting and of course makes sense: rationals do indeed have the hallmark of having a terminating or repeatable pattern in their decimal places. If this was not so it would simply not meet the definition. I am not so sure that what is posted above really proves it though because so far as I know other continued fractions do have a rational limit. Are you sure about this, Elroch? I was thinking that there would be a constructive proof with a direct example, whatever that would mean in this case (although the above is indeed simple)....
Yes I am 100% sure of this, strangequark. It's not difficult to fill in the standard results I described as "easy" above. I will sketch the two proofs from scratch.
THEOREM 1: All rationals have a terminating continued fraction
First remove the integer part, so you have a rational strictly between 0 and 1. Proof by induction on the denominator. Clearly no problem if the denominator is 1.
a/b = 1/(b mod a + c/a)
for some c
But a was less than b, so has a finite continued fraction by induction hypothesis.
That concludes the proof. The converse of theorem 1, that all finite continued fractions are rational, is even easier.
THEOREM 2: The continued fraction of sqrt(2) is (1;2,2,2,2,2 ...)
(Here, I use a standard notation that is easier to write, but it's the same as the fancy version in the graphic in my earlier post).
Consider R = sqrt(2) - 1 (the continued fraction of sqrt(2) with the integer part, which is 1, subtracted)
1/(sqrt(2) - 1) = sqrt(2) + 1 (I multiplied top and bottom by (sqrt(2)+1) )
So we have a recurrence relation:
R = 2 + 1/R.
This recurrence relation immediately gives the repeating part of the continued fraction, by definition.
Which ends the proof of theorem 2.
This may seem a bit alien if you've never played with continued fractions, but it is easy manipulation, and can be made rigourous with a small amount of work defining an infinite continued fraction as the limit of its partial sums.
Thanks, Elroch. I had imagined such a proof to be a bit harder. I don't strictly study continued fractions too much although I've played around with infinite nested radicals a lot which are essentially the same as far as I know. I still have one question, though: how do we know that there will be a separate framework for defining sqrt(2) as irrational if before the proof we don't know there are irrationals anyways? How do we know we can have a pre-built framework to extract the definition from and complete the proof in the first place?
Well, if you want to construct all of the mathematics that supports this, you will first of all need to construct the real numbers from the rational numbers using whatever method you require (I suggest Dedekind cut). Then prove the closure of the real numbers (i.e. for each set of real numbers bounded above there is a least upper bound (LUB) ). Then prove the existence of sqrt(2) by defining it as the LUB of the set of numbers whose squares are less than or equal to 2 and showing its square is indeed 2. Given the existence of sqrt(2) it has to be either rational or not rational, and you can use the argument in my earlier post to prove that it is the latter. Is that enough?
Looks complete to me. Excellent. I love Dedekind cuts. Thanks Elroch.
Lolz... Continued fraction proof. I like it!
Hmmm... well there you go! The Analyst saves the day again!
Does anyone here know or have a referance for a constructive proof that sqrt2 is irrational?