@TimothyChow I've just read your article. Actually I was hoping to see a more complete account of the part where ordinals below ε0 "are used to track game trees". But I think we pretty much agree on the philosophy part:
> For example, suppose we design a computer program to search for positive natural numbers a and b such that a^2 = 2 b^2. [The strict formalist] Stefan has no conclusive grounds for believing that such a search is futile.
> Stefan is thus faced with a puzzle that I call ‘‘the unreasonable soundness of mathematics.’’ Stefan can observe that conventional mathematicians are remarkably successful at making accurate predictions of the results of syntactic manipulations, but he has no explanation for this success.
Relatedly, it seems that we can 'explain' PA's soundness by appealing to PA*, which is basically M-bounded PA plus "∀n ( n<M ⇒ n+1<M )" (A) and "0<M".
@CarlMummert @LeakyNun: Also, for any explicit formal system S, we can define Con(S) as "∀p<M ( p is not a proof of (0=1) over S )", and this has the interesting feature of being compatible with the possibility that S is consistent in the sense of having no explicitly constructible proof of (0=1) and yet has no real-world model.
