« first day (1760 days earlier)      last day (1051 days later) » 

9:16 AM
This is plainly wrong. PA (and later ACA) was designed to model real-world counting. So of course mathematics that can be carried out in ACA are effective in real-world applications! This is not circular at all. If the world was different enough that counting had a different structure, we would be much less likely to invent PA! The problem with other responses is that they conflate "all mathematics" with "mathematics that is effective for the real-world", and I had already explained that in my answer. — user21820 17 hours ago
^ Strangely, a plainly wrong post on MathOverflow can get 4 upvotes...
 
 
8 hours later…
5:38 PM
@user21820 Going from a vague concept of "real-world counting" all the way up to ACA seems like a big jump to me. Why can't I argue that bounded arithmetic already captures "real-word counting" and hence it is remarkable that stronger induction axioms, or the weak Koenig lemma, also seem to describe the real world? — Timothy Chow 5 hours ago
@TimothyChow: That's why I explicitly said that it rests on "believing that there is some kind of real-world interpretation of PA that is standard". If you believe in PA− but only very limited induction, then you of course can't get to ACA. But that doesn't really make sense, because from any model of PA− the initial segment is a model of full PA. So simply belief in some kind of real-world interpretation of PA− that is standard suffices! (Of course you might argue that this claim itself cannot be proven without sufficiently strong meta-system, but the intuition is still explanatory.) — user21820 2 mins ago
 

« first day (1760 days earlier)      last day (1051 days later) »