OK, so I've gone through the demonstration that there are undecidable propositions inside any formal system sufficient for addition, multiplication, and the basic logical operations of the elementary theory of whole numbers. From here it's actually pretty easy to see why the consistency of the formal system, which I'm referring to as PM, cannot be proven within the system. Again, I will stay as close as I can, up to the ability of this editor to represent it, to Goedel's notation.
Let Wid(c) be defined as the statement that there exists a formula x such that it cannot be derived from the set of formulae c. That is, (Ex)[Form(x) & ~(Bew(x))]. Here Bew means provable from the formulae c. Literally, There exists an x such that x is a formula of PM and x is not provable from the formulae c.
Now we have to prove this. Remember that 17 Gen r is not provable within PM. So, Wid(c)-->~(Bew(17 Gen r)). That is, as long as there are unprovable propositions, the undecidable one from before is unprovable. But the fact that for any x, 17 Gen r is not provable is equivalent to the statement(for all x)q(Z(x),Z(p)), recalling that 17 Gen r = p(Z(p)). Therefore, if PM is consistent, we can prove 17 Gen r! This is a contradiction of Wid(c)-->~(Bew(17 Gen r)) above. Here we use the fact that 17 Gen r states its own unprovability, so to prove it unprovable is to prove it.
Thus, a formal system like PM cannot prove its own consistency. Well, what's so big about that? For one thing, suppose you have a bigger system that contains PM, can it prove it's own consistency? It seems it can't because the argument above would apply to it and we would have an infinite regress. Please let me know if I'm wrong about this.
Next time I will return to I am a Strange Loop.