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.
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.