[imh]

Thanks for the answer! Out of curiosity what about systems we can prove able to "do" basic arithmetic, ignoring whether they can talk about it?

I'm imagining the difference between a system that can show "P(n)" for any n, rather than a system that can show "P(n) for any n."

It seems like the former must come with a proof about the system. The quantifiers "for any n" have to come somewhere. If they aren't embedded within the system, do we still end up with a system that must be able to express "This sentence is not provable?"