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?
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.
