When a solution is formalized inside a theorem prover, it is reduced to the level of arithmetic (a theorem prover is an arithmetic-level machine).
So a theory might be a very high-brow math, but a formal derivation is still arithmetic (if one just focuses on the syntax and the formal rules, and not on the presumed semantics).
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).
Yeah, I think this is the distinction I’m struggling with. To start with proofs in Euclid, why can I prove that the square root of two is irrational? Why can I prove there are infinite prime numbers? If I saw that they are escaping this self-reference somehow, maybe I’d get the point. And without that, I don’t see that I can rule out such an escape in Collatz.
These seem “simple” but actually step above pure arithmetic to even state them. That’s exactly the pattern—we need to go above arithmetic level to prove things. Can you find any famous proofs that stay purely within natural numbers?
We can eliminate the concept of rational numbers by framing it as the proof that there are no integer solutions to p² = 2 q²… but… no proof by contradiction? If escape from self-reference is that easy, then surely it is possible to prove the Collatz conjecture. Someone just needs to prove that the existence of any cycle beyond the familiar one implies a contradiction.
Not off the top of my head, but since a proof of Collatz does not require working under these constraints, I don’t think the distinction has any important implications.
Actually, Collatz DOES require working under these constraints if staying in arithmetic. The conjecture itself needs universal quantification (“for ALL numbers...”) to even state it. In pure arithmetic we can only verify specific cases: “4 goes to 2″, “5 goes to 16 to 8 to 4 to 2”, etc.
Alright, so Collatz will be proved, and the proof will not be done by “staying in arithmetic”. Just as the proof that there do not exist numbers p and q that satisfy the equation p² = 2 q² (or equivalently, that all numbers do not satisfy it) is not done by “staying in arithmetic”. It doesn’t matter.
This shows why it DOES matter: Both Collatz and p² = 2q² require going above arithmetic to even state them (“for ALL numbers...”). That’s the key insight—we can’t even formulate these interesting conjectures within pure arithmetic, let alone prove them. In pure arithmetic we can only check specific cases:
ALL solved conjectures have their proof or system above arithmetic level
NONE that stay in arithmetic are solved
When a solution is formalized inside a theorem prover, it is reduced to the level of arithmetic (a theorem prover is an arithmetic-level machine).
So a theory might be a very high-brow math, but a formal derivation is still arithmetic (if one just focuses on the syntax and the formal rules, and not on the presumed semantics).
The theorem prover point is interesting but misses the key distinction:
Yes, theorem provers operate at a mechanical/syntactic level
But they still encode and use higher mathematical concepts
The proofs they verify still require going above pure arithmetic
The mechanical verification is different from staying within arithmetic concepts
In pure arithmetic we can only:
Do basic operations (+,-,×,÷)
Check specific cases
Compute results
Any examples of real conjectures proven while staying at this basic level?
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).
Yeah, I think this is the distinction I’m struggling with. To start with proofs in Euclid, why can I prove that the square root of two is irrational? Why can I prove there are infinite prime numbers? If I saw that they are escaping this self-reference somehow, maybe I’d get the point. And without that, I don’t see that I can rule out such an escape in Collatz.
Both examples perfectly demonstrate my point:
√2 irrationality—requires real numbers (beyond arithmetic)
Infinite primes—requires infinity (beyond arithmetic)
These seem “simple” but actually step above pure arithmetic to even state them. That’s exactly the pattern—we need to go above arithmetic level to prove things. Can you find any famous proofs that stay purely within natural numbers?
Yes, the proof that there’s no rational solution to x²=2. It doesn’t require real numbers.
The proof requires:
The concept of rational numbers (not just natural numbers)
Proof by contradiction (logical structure above arithmetic)
Divisibility properties beyond basic operations
We can only use counting and basic operations (+,-,×,÷) in pure arithmetic. Any examples that stay within those bounds?
We can eliminate the concept of rational numbers by framing it as the proof that there are no integer solutions to p² = 2 q²… but… no proof by contradiction? If escape from self-reference is that easy, then surely it is possible to prove the Collatz conjecture. Someone just needs to prove that the existence of any cycle beyond the familiar one implies a contradiction.
Actually, your example still goes beyond arithmetic:
“No integer solutions” is a universal statement about ALL integers
Proof by contradiction is still needed
Even reframed, it requires proving properties about ALL possible p and q
In pure arithmetic we can only check specific cases: “3² ≠ 2×2²”, “4² ≠ 2×3²”, etc. Any examples using just counting and basic operations?
Not off the top of my head, but since a proof of Collatz does not require working under these constraints, I don’t think the distinction has any important implications.
Actually, Collatz DOES require working under these constraints if staying in arithmetic. The conjecture itself needs universal quantification (“for ALL numbers...”) to even state it. In pure arithmetic we can only verify specific cases: “4 goes to 2″, “5 goes to 16 to 8 to 4 to 2”, etc.
Alright, so Collatz will be proved, and the proof will not be done by “staying in arithmetic”. Just as the proof that there do not exist numbers p and q that satisfy the equation p² = 2 q² (or equivalently, that all numbers do not satisfy it) is not done by “staying in arithmetic”. It doesn’t matter.
This shows why it DOES matter: Both Collatz and p² = 2q² require going above arithmetic to even state them (“for ALL numbers...”). That’s the key insight—we can’t even formulate these interesting conjectures within pure arithmetic, let alone prove them. In pure arithmetic we can only check specific cases:
“4 goes to 2”
“3² ≠ 2×2²”