# [FOM] The unreasonable soundness of mathematics

Timothy Y. Chow tchow at alum.mit.edu
Wed May 18 23:06:17 EDT 2016

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