Yes there's a proof. One flavor is that in any system for expressing numbers using symbols, you can show a correspondence between finite strings of symbols, and

Yes there's a proof. One flavor is that in any system for expressing numbers using symbols, you can show a correspondence between finite strings of symbols, and whole numbers. So, what works for whole numbers also works for things like proofs and formulas. I think the correspondence may be called "Goedel numbering."