Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
One further question: Does RT$_2^2$ being $\Pi^0_3$-conservative over RCA$_0$ mean that there might be, say, a $\Pi^0_5$ sentence that RCA$_0$+RT$_2^2$ can prove but RCA$_0$ by itself can't? I tried to count the quantifiers in the Hilbert-Waring theorem and I think it's $\Pi^0_3$ but maybe there's something else like that which goes higher.
Btw, regarding above comment about primitive recursive algorithms: I'm not sure whether the question was a minor point of terminology, or whether the issue is actually significant.
Unfortunately I don't seem to be able to mark an answer as "accepted" without signing up for an account here, which I'd rather not do. But Bjørn and François' answers and Henry Towsner's comment are all very clarifying and I think I understand the matter now. Overall I think the Quanta article didn't convey the point very well, but MO came through. Thanks again everyone!
Thanks! The explanation of RT$^2_2$ being useful in termination proofs adds helpful context. But do you really mean to say that (PRA proves termination) means the algorithm itself is primitive recursive? For example I thought PRA proves that the (partial recursive) algorithm for the Ackermann function terminates.
Thanks! I understand why it's an interesting and impressive result (and your explanation helped fill in the picture), but it still seems purely technical, as opposed to something like the incompleteness theorem that made people re-examine the concept of truth. The Quanta article made it sound like this RT$_2^2$ result told us something new about potential vs completed infinity, and old philosophical conundrum. So I'm wondering what that something (if any) is. And is there really such a scarcity of these conservativity results?