[FOM] The unreasonable soundness of mathematics

[Mario Carneiro]

On Wed, May 18, 2016 at 11:06 PM, Timothy Y. Chow <tchow at alum.mit.edu>
wrote:

> 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.
>

I claim that yes, it is ultrafinistically true, but I also agree with your
last sentence. To answer your original question about glossing "feasible"
on all the statements, this is valid provided that all reasoning is
conditional on Con(T). If X is checked to be true, and Y follows
syntactically from X, then either Y is true, or Con(PA) is false. Since I
place a low probability on Con(PA) being false, I am thus convinced of the
truth of Y. And as I said, if Con(PA) is false, (1) we would know it when
we see it and (2) this is also a mathematical result of great relevance,
which is a consolation prize over my original deduction on truth of Y being
incorrect. In fact, even this assertion Con(PA) is ultrafinite: if PA is
inconsistent but the proof is too long for it to have an effect on any
human derivations, it won't be able to damage the predictive power you get
as a result.

As for soundness, that's not an assumption, it logically follows from
soundness of proof deductions and my assumption that computer A is
following its mathematical specification.


> 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.
>

I don't view proofs as physical theories - I think I have the same desire
as you to assign a "higher" level of truth to them, but I am also
constrained by the limitations of math itself. To you I am probably
"cheating" by resolving your puzzle by assuming Con(PA), for which I have
no real reason to believe is true (besides the obvious societal reasons),
and is also subject to the "surprise" problem. In other words, you could
also rephrase it as the "unreasonable consistency of PA".

I don't believe there is any useful way to entirely eliminate consistency
assumptions in mathematics. Godel showed this, and mathematics lives on in
spite of this clear weak point. So at some point you just have to "live
with it". Nevertheless, I think that the situation above is a fairly good
way to make sense of the predictive power of mathematics, within its
natural limitations.


> 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.


Finally, let me point out that statements like "the theorem A follows from
the axioms and rules of inference of T" are certainly being shown
unconditionally by a proof, and the difference in epistemological status in
at least this case should be clear. The dependence on consistency only
arises when you attempt to correlate these proofs with "actual numbers" in
the way we have discussed.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160519/3982262d/attachment-0001.html>