The problem I’m trying to understand is more of a meta/proof-theoretic one: why do some arithmetical claims have a proof only when passing through non-arithmetical language?
Formally, we have the Peano Axioms which characterize all first-order properties of N. An example statement for the ternary Goldbach conjecture:
φ has a proof in Peano Axioms, but the only proof found so far passes through complex analysis. This means that the only known way to prove φ in PA is to encode all properties of complex analysis within the language of natural numbers.
This sounds horribly inefficient; intuitively, it sounds like that any “natural” statement provable in PA should be provable using tools from this system, and not by encoding concepts from a different field.
This does relate to some interesting concepts in logic, like Godel’s speed-up theorem. I didn’t mention these considerations at all in my post, might be good material for a part II 🙂
I also find instances of this phenomenon very interesting. One example I can think of is in differential geometry where statements about manifolds are often easier proved (and in many cases, so far only proved) by routing through Riemannian geometry (since via partitions of unity, a manifold can always be given a Riemannian metric) and manipulating the manifold primarily through its metric structure (eg Ricci Flow) - even though the original statement doesn’t invoke metrics at all!
The problem I’m trying to understand is more of a meta/proof-theoretic one: why do some arithmetical claims have a proof only when passing through non-arithmetical language?
I agree this is an interesting question. Thanks for pointing me to the speed-up theorem. I didn’t know about that one. :)
This sounds horribly inefficient; intuitively, it sounds like that any “natural” statement provable in PA should be provable using tools from this system, and not by encoding concepts from a different field.
Yeah, I don’t share that intuition. It feels like if that was true, there would be no other fields and everyone would be using arithmetic for everything at all times. I guess your phrasing of “natural” is doing a lot of work here.
The problem I’m trying to understand is more of a meta/proof-theoretic one: why do some arithmetical claims have a proof only when passing through non-arithmetical language?
Formally, we have the Peano Axioms which characterize all first-order properties of N. An example statement for the ternary Goldbach conjecture:
φ:∀N≥3∃p1,p2,p3(IsPrime(p1)∧IsPrime(p2)∧IsPrime(p3)∧p1+p2+p3=N⋅2+1)φ has a proof in Peano Axioms, but the only proof found so far passes through complex analysis. This means that the only known way to prove φ in PA is to encode all properties of complex analysis within the language of natural numbers.
This sounds horribly inefficient; intuitively, it sounds like that any “natural” statement provable in PA should be provable using tools from this system, and not by encoding concepts from a different field.
This does relate to some interesting concepts in logic, like Godel’s speed-up theorem. I didn’t mention these considerations at all in my post, might be good material for a part II 🙂
I also find instances of this phenomenon very interesting. One example I can think of is in differential geometry where statements about manifolds are often easier proved (and in many cases, so far only proved) by routing through Riemannian geometry (since via partitions of unity, a manifold can always be given a Riemannian metric) and manipulating the manifold primarily through its metric structure (eg Ricci Flow) - even though the original statement doesn’t invoke metrics at all!
I agree this is an interesting question. Thanks for pointing me to the speed-up theorem. I didn’t know about that one. :)
Yeah, I don’t share that intuition. It feels like if that was true, there would be no other fields and everyone would be using arithmetic for everything at all times. I guess your phrasing of “natural” is doing a lot of work here.