I'm aware that very smart people have thought carefully about all this, but I still can't help thinking that this argument is unnecessarily complicated. It seems to me that a proof is something that can be written down as a finite string of symbols, so any proof system admits only countably many proofs. On the other hand, it's easy to make up an example of an uncountable set of propositions. That's too many for each of them to have a proof, so some of them must be unprovable. What am I missing?