[FOM] The unreasonable soundness of mathematics

[Timothy Y. Chow]

On Mon, 16 May 2016, Mario Carneiro wrote:
> Indeed, the formal system could in principle be something as brain-dead 
> as "all true statements about [1...N] of length < M" where N is large 
> enough to cover all the numbers accessible to computer A and M is larger 
> than any statement of interest. This would require computer B to be much 
> more (physically) powerful than computer A, but it would allow us to 
> make true statements about the behavior of computer A.
> 
> However, in practice we would never bother with such a roundabout 
> axiomatization. Instead, we take a much simpler but more powerful axiom 
> system, like PA, and then our results become conditional on Con(PA), in 
> an effective way (that is, a violation of a proven statement by computer 
> A can be translated to a proof of contradiction in PA).

I still think you're sneaking in hidden assumptions about *soundness* 
without noticing it.

The exhaustive list of true statements (which only works for extremely 
small A, but let's accept that for now) does address the question of how 
we *know* that they're true, because we can simply check each statement 
one by one for truth.  However, there's still a "surprise" problem.  If 
I've checked the first 10^9 statements for truth, then there's still no 
reason for me to expect that statement (10^9 + 1) will be true.  Indeed, 
if I imagine implementing this system, the simplest way is to generate 
*all* statements, not just the true ones, and check them one by one. 
Under this system, statement (10^9 + 1) generally *won't* be true; it'll 
just be some random statement that might or might not be true.

If you instead try the shortcut of something like PA, the question still 
arises, why should theorems of PA be true?  Given that I've checked that X 
is true, and that Y follows syntactically from X, why should I expect Y to 
be true as well?  Your statement that the "violation of a proven statement 
by computer A can be translated to a proof of contradiction in PA" is not, 
as far as I can see, *ultrafinistically* true; I can check each instance 
of this claim but I don't know for sure that the next time I attempt the 
algorithm that I'll get a contradiction in PA.

The most that I can see you doing is treating mathematical proofs of (say) 
"the square root of 2 is irrational" in the same way that we treat 
*physical theories*.  I have a way that I can generate predictions of 
physical experiments (using larger and larger computers) and I can 
*provisionally* theorize that if I search for a solution to A^2 = 2*B^2 
then I won't find anything.  In this sense "the square root of 2 is 
irrational" has the same epistemological status as "there are no magnetic 
monopoles."  Now maybe you're fine with that; I think someone else chimed 
in at one point in this discussion that he regards mathematical theorems 
as just certain kinds of physical theories, and maybe you agree.  In that 
case, I guess my "unreasonable soundness of mathematics" reduces to a form 
of the "unreasonable effectiveness of mathematics in physics," and is 
(therefore?) perhaps not so interesting.

However, for those who think that "the square root of 2 is irrational" has 
a *different* epistemological status from that of "there are no magnetic 
monopoles" *because the former has been proved*, and yet claim to be 
ultrafinitists, I still see an unanswered puzzle.

Tim