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?
Does your uncountable set of propositions include some which cannot be written as a finite string of symbols?
If "yes" - how might such as proposition be proven true with a finite string of symbols?
(If your proof symbols are from an infinite character set, that has its own issues.)
I'm assuming a finite alphabet and a finitely axiomatizable proof system per convention. I can't think of an uncountable set of propositions in which each can be written as a finite string of symbols, so that's what I was missing. Thank you for clearing this up for me.
If you substitute uncountability in your intuition with algorithmic incompressibility (too much information to be captured by shorter descriptions) you have Chaitin's incompleteness theorem.
Kudos for the well-placed hunch!