I'm not a fan of how the proof is explained, specifically why are we doing x or y.
I would prefer this --
Let pi be a rational number thus ( * by the definition of rational numbers) pi = a/b, the quotient of positive integers. We will show no such a and b can exist, therefore pi cannot be rational.
( * is not completely necessary, since the definition of rationals is so elementary)
<Next Paragraph, and so on>
I suspect a lot of mathematicians prefer the format given because it is more obtuse...
> I suspect a lot of mathematicians prefer the format given because it is more obtuse...
No, because as you say, defining what a rational number is seems pretty pointless here, as why would you be reading the proof of something whose definition you don't even know? And you also want an explanation of what a proof by contradiction is, which also seems to be way too elementary. Proof by contradiction is one of the most basic techniques.
Spivak's version of this proof explains it a bit more, but still requires work from the reader. Any proof does. Mathematics cannot be a spectator sport.
A lot of people struggle at math because they're missing things like that. With today's technology, there's no reason things can't be broken down to arbitrarily small steps, so that people can be filled in on the cracks in the foundations of their understanding of math.
The usual reason for not including everything is that it becomes ridiculously laborious. With mathematics being abstraction piled atop abstraction, this is quite reasonable. Just look at how much work it is to prove 2+2=4 -- http://us.metamath.org/mpegif/mmset.html#trivia
But, as you can see from the above, there's technology to simplify things. I wonder if someday we'll be able to break things down in a friendly way so that for any piece a student doesn't understand, they can get a proof in terms of things they do understand?
Erm, the linked metamath page asks what's the longest path one can take. Well, geez, it's long. Proving that 2+2=4 from the usual Peano axioms isn't that hard or long. We define addition by a+0=a,a+S(b)=S(a+b). Now what we mean by a positive integer number is just a shorthand for that number of successive S(). So 2+2=4 is just S(S(0)) + S(S(0)) = S(S(S(S(0)))). To prove this, let's apply the second part of the addition to S(S(0)) + S(S(0)) we get S(S(S(0)) + S(0)). Let's repeat this "move the S() from the second to the outside" and you will get S(S(S(S(0)) + 0)). Now we can use our first half of definition where +0 can be left out: S(S(S(S(0)))). Now, that wasn't that long, was it?
I'm not a mathematician, so please bear with me. I'm trying to understand your definition of addition. Surely that can't be enough? At the very least a+b=0 satisfies your formulas (should I use the word axiom there?).
What I'm trying to understand is how I am supposed to think in order to prove/disprove my statement above. Disproving something by contradiction is easy enough, if you can find a contradiction but what if you can't? How can you be sure that you've covered all variations?
This is something one struggles with as a developer too. There are cases where you think that a fundamental function does the right thing for all inputs but then you discover an edge case where that isn't true. The number of cases where this has been the case even in high profile libraries suggests that I'm not alone in this.
What is missing from chx's description is the definition of the natural numbers (and the S (successor) function). The standard definition is:
0 is a natural number
S(n) is a natural number, if and only if n is a natural number
x=y if and only if S(x)=S(y)
for all x, S(x)!=0
These axioms are sufficient to show that the natural numbers form a line.
At this point, we can use the definition of addition that chx provided:
a+0=a
a+S(b)=S(a+b)
It is true that, without the restrictions on S, than defining a+b=0 would satisfy these. However, because of the restrictions on S from our definition of the natural numbers, it is impossible for S(a+b)=0.
In some sense, proofs as presented in a textbook should not hold your hand. The point of learning about proofs is being able to create proofs yourself, even if they are trivial variations on proofs you have seen.
Computer analogy: would it be a good idea if someone showing an implementation of a double-linked list explained every little detail about pointers and arrays etc.?
However, there are many things we can do syntax-wise to facilitate the understanding of proofs. I remember we experimented with using indentation (on paper) in proofs when I did functional analysis, and that was quite useful for keeping track of "variable scope" etc.
While it's true that you won't survive long with a lot of 'cracks' in your foundation of understanding, I think there's quite a bit of worth in helping people identify and explore the holes in their own understanding and making this as painless as possible.
I understand that we can't trod new ground if nobody is willing to put up with the difficult slogs, but there's no reason to make things difficult for the sake of difficulty. There are plenty of challenging exercises one can do simply by learning to apply a newfound understanding without having to leap from perch to perch because nobody would explain how to bridge a certain gap.
I think that things are trending in this direction already, actually.
It is immediately obvious that he is attempting proof by contradiction, because the first line supposes the opposite of the title of the paper. As in the proof of the irrationality of the square root of 2, he sets up his assumption that pi is rational by defining it as a/b.
In a proof, we don't have to know why something is done, just that it logically follows from our assumptions and is used as a step in the proof. Explaining how the author came up with the proof should be left to an educational textbook or an "Author's Notes" if the proof is several pages long and would help readers be guided along.
I'd prefer something similar to your version, like: Let's suppose that pi is rational, pi = a/b ...
I usually like to understand what is the intended meaning of the symbols and how they will be used later, in spite it's not necessary to have a correct proof. I was (slightly) surprised when I found out that a/b "was" pi.
But, each one has a preferred writing style, ...
But in this case, I suspect that the proof is optimized for space. An alternative title could be "A proof that pi is irrational in one page" so some details and constructions are skipped to put everything in one page.
Using pi as a name is only a very weak cue for "proof by contradiction". The title of the paper gives enough hint to detect it, but I would still use "suppose pi is rational", because it is the dead giveaway for proof by contradiction.
And as to 'obtuse': how many C programmers comment their 'main' function to help people unfamiliar with the language learn that it is the entry point of the program and receives its command line arguments as input? At some time, you have to assume your audience knows some lingo.
My main objection to this proof is that I do not find it beautiful; it feels like one shouldn't need to do integrals over goniometric functions to prove it.
Because it uses such fairly heavy weaponry, it isn't immediately clear to me that the logic isn't circular.
I'm not a fan of how the proof is explained, specifically why are we doing x or y.
I would prefer this --
Let pi be a rational number thus ( * by the definition of rational numbers) pi = a/b, the quotient of positive integers. We will show no such a and b can exist, therefore pi cannot be rational.
( * is not completely necessary, since the definition of rationals is so elementary)
<Next Paragraph, and so on>
I suspect a lot of mathematicians prefer the format given because it is more obtuse...