Your point about ASCII codes ignores that we don't just want individual symbols to be numbers, we want entire formulas to be numbers too. Of course, you can en

Your point about ASCII codes ignores that we don't just want individual symbols to be numbers, we want entire formulas to be numbers too. Of course, you can encode any sequence of ASCII codes as a number (just concatenate the binary digits), I didn't doubt that. But to formally prove that this leads to unique parsing requires unnecessary technical work that mathematicians prefer to avoid because the exact coding scheme doesn't matter. > Any system less powerful than PA is trivially incomplete. That is false. See here for examples of complete theories, for which Gödel's incompleteness theorems don't apply because they are not strong enough: https://en.m.wikipedia.org/wiki/Complete_theory https://en.m.wikipedia.org/wiki/Complete_theory (Moreover, there are theories that are neither stronger nor weaker than PA. One such theory can give rise to an interesting proof of consistency of PA: https://en.m.wikipedia.org/wiki/Gentzen%27s_consistency_proof https://en.m.wikipedia.org/wiki/Gentzen%27s_consistency_proo...)