Yes, the technique of formal proofs, in effect, involves translation of high-level proofs into arithmetic.
So self-reference is fully present (that’s why we have Gödel’s results and other similar results).
What this implies, in particular, is that one can reduce a “real proof” to the arithmetic; this would be ugly, and one should not do it in one’s informal mathematical practice; but your post is not talking about pragmatics, you are referencing “fundamental limit of self-reference”.
And, certainly, there are some interesting fundamental limits of self-reference (that’s why we have algorithmically undecidable problems and such). But this is different from issues of pragmatic math techniques.
What high-level abstraction buys us is a lot of structure and intuition. The constraints related to staying within arithmetic are pragmatic, and not fundamental (without high-level abstractions one loses some very powerful ways to structure things and to guide our intuition, and things stop being comprehensible to a human mind).
Yes, the technique of formal proofs, in effect, involves translation of high-level proofs into arithmetic.
So self-reference is fully present (that’s why we have Gödel’s results and other similar results).
What this implies, in particular, is that one can reduce a “real proof” to the arithmetic; this would be ugly, and one should not do it in one’s informal mathematical practice; but your post is not talking about pragmatics, you are referencing “fundamental limit of self-reference”.
And, certainly, there are some interesting fundamental limits of self-reference (that’s why we have algorithmically undecidable problems and such). But this is different from issues of pragmatic math techniques.
What high-level abstraction buys us is a lot of structure and intuition. The constraints related to staying within arithmetic are pragmatic, and not fundamental (without high-level abstractions one loses some very powerful ways to structure things and to guide our intuition, and things stop being comprehensible to a human mind).