[FOM] The unreasonable soundness of mathematics

[Mario Carneiro]

On Sun, May 15, 2016 at 4:26 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:

> On Sat, 14 May 2016, Mario Carneiro wrote:
>
>> Finally, once "for all feasible n, phi(n)" statements are regarded as
>> having ultrafinitist meaning, the "endless surprise" puzzle is resolved: we
>> have a single statement, which quantifies over all the numbers you can hope
>> to care about; the ultrafinitist is made to be convinced of such a
>> statement by translating an analogous pure mathematical statement talking
>> about "all n", with a finite and feasible proof. Having seen the proof, the
>> ultrafinitist will not be surprised by the gigabyte computer's failure to
>> find a counterexample, nor the terabyte computer.
>>
>
> It looks to me that the distinction you drew earlier in the conversation,
> between yourself and "true ultrafinitists," comes into play here.  Namely,
> the *formalization of feasible reasoning* seems relevant.
>
> It sounds to me that you, Mario Carneiro (and not Mario Carneiro speaking
> for an ultrafinitist), are comfortable taking a traditional formal proof,
> that has no explicit "feasibility predicate," and glossing it line by line
> using the rule that when you see "An: phi(n)" then you read it out loud as
> "for all feasible n, phi(n)," and if Formal Statement X follows formally
> from Formal Statement Y according to traditional syntactic rules, then you
> accept that the "out-loud-reading" of Formal Statement X (i.e., its
> translation into a meaningful statement that explicitly involves the
> adjective "feasible") correctly follows from the "out-loud-reading" of
> Formal Statement Y.  Is that right?
>

> However, it seems to me that a true ultrafinitist isn't entitled to this.
> The true ultrafinitist has to check whether the "out-loud-reading" of
> Formal Statement X follows from the "out-loud-reading" of Formal Statement
> Y *via ultrafinitistically valid logical reasoning*.
>

Earlier, I had this to say about axioms/inference rules used in the proof:

Note that it doesn't matter how complicated the original proof of |- P(42)
> was or what axioms were used, since all of the above pertains to the proof
> of |- not P(42) by simulation of computer A, using "finite reasoning"
> (meaning an abstraction of a finite system, which corresponds for
> sufficiently small proofs). If the correspondence between computer A and
> computer B fails, then the theory is inconsistent. Since consistency is
> already considered an important determinant for fitness of a axiom system,
> it wouldn't seem to produce any new desiderata.
>

In other words, I would expect of the formal system that it is sufficiently
powerful to analyze the behavior of computer A, and it is consistent. I
would like to shorten this to saying that the formal system is at least as
powerful as PA, but as D. Mekheri points out, this would commit one to
totality of exponentiation and other not strictly necessary things for the
analysis of a given finite computer.

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). But this approach makes
it clear that weaker axiom systems like Robinson's Q or EFA are also
permissible in this regard, as well as wildly stronger systems like ZFC and
large cardinal extensions thereof. All of these can be leveraged to produce
predictions about computer A, and they will either be true or we will get a
proof of inconsistency, both of which are useful results.

This is why I feel comfortable using infinite reasoning in an ultrafinite
world, because all the axiom systems in sight are "probably consistent" and
all my reasoning is conditional on consistency anyway. If something breaks
we will have to backtrack, but this too will give a lot of insight on the
multiverse of logical systems and their relationships.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160516/ff4173a5/attachment.html>