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!