[FOM] The unreasonable soundness of mathematics

Sat Apr 30 23:35:14 EDT 2016

I would abbreviate your two interpretations as "P(n) is true for all
reasonable n" vs "(all n, P(n)) is provable".  In order to relate these
two, take some reasonable n, say 42. Then we arrive on the one hand that
P(42) is true (as some explicitly checkable numeric assertion), according
to computer A, and on the other hand we have that |- P(42) is provable
according to computer B (by universal instantiation).

Now let's suppose that the correspondence fails somehow, so that computer B
has proven |- P(42) but computer A has found that P(42) is false. Assuming
that the theory used by computer B is sufficiently powerful, it will be
able to formalize the abstract machine states of computer A, and thereby
will also prove |- not P(42), and hence the theory is inconsistent (and the
proof of this is reasonably sized too). Thus the correspondence reduces to
a consistency problem for the theory of computer B.

Now I suppose the part you want to home in on is the formalization of
computer A's operation by computer B. The reason this is possible is
because computer A satisfies an abstract model *because it was designed
that way*. Computer A is not some mysterious physical system whose behavior
is the object of study, but is instead a deliberately designed instrument
whose fitness is measured by its adherence at a high level to a given
abstract model. Although it's not a true Turing Machine because it doesn't
have infinite resources, it is good enough to match the abstract model for
"reasonable" computations, so that we can effectively capture this behavior
that we specified for computer A, in computer B, by formalizing not the
circuits and transistors, but the specification.

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.

Now, of course it is also possible for the correspondence to fail in the
other direction, that is, computer A is failing to find any counterexample,
but computer B is not finding any proof of |- all n, P(n) (or perhaps even
proven |- exists n, not P(n)). In this case, I don't think anyone would be
surprised, and the gloss "P(n) is true for all reasonable n" even indicates
how this can happen - just take P(n) to be false at some unreasonable n. It
is not hard to come up with examples of such P(n), like "P(n) = n <
2^2^2^2^2^2^2^2". This corresponds to your observation: "empirical
observation alone can lead only to a "conjecture" and not a "theorem.""

Mario

On Sat, Apr 30, 2016 at 4:17 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:

> Mulling over the recent FOM discussion I had with Mario Carneiro, I came
> up with an insight that I am going to call the "unreasonable soundness of
> mathematics", for reasons that should become clear.  I will start by posing
> a puzzle for ultrafinitists, but I will go on to pose a more general puzzle.
>
> Let us start by picking some Pi_1 statement, such as "PA is consistent" or
> Fermat's Last Theorem (FLT).  What does such an assertion mean to an
> ultrafinitist?  As I understand it, there are two entirely different ways
> that an ultrafinitist might interpret such a statement.
>
> Under the first interpretation, "PA is consistent" means something along
> the lines of, "When we program a computer in a certain way and set it
> running, we have never observed it to output `0=1', and furthermore nobody
> in the future will ever observe a similarly programmed computer to output
> `0=1', no matter how big a computer they build and no matter how patiently
> they wait."  Let's use the term "Computer A" to refer generically to
> computers that perform this kind of search for a counterexample to a Pi_1
> statement.
>
> Under the second interpretation, "PA is consistent" is judged to be an
> infinitary mathematical statement which therefore has no "direct" meaning;
> instead, we make the sociological observation that mathematicians accept
> infinitary statements when and only when they are in possession of a
> *proof*.  Therefore when someone asserts "PA is consistent," they really
> mean something along the lines of, "It is an accepted fact in the
> mathematical community that if you take your favorite proof assistant and
> give it the appropriate input, then it will verify that there is a correct
> proof of Con(PA) in one of the generally accepted axiomatic systems for the
> foundations of mathematics."  Let's use the term "Computer B" to refer
> generically to computers that are equipped with proof assistants and that
> are dedicated to verifying formal proofs.
>
> Which interpretation is favored might depend on who you ask, and in what
> context.  It might also depend on the Pi_1 statement in question.  For "PA
> is consistent" I suspect that most ultrafinitists will gravitate towards
> the first interpretation.  For FLT, I suspect that more ultrafinitists will
> gravitate towards the second interpretation, because they will hesitate to
> attribute direct semantic content to assertions about the integers.  It
> does not matter for what I say below which interpretation you prefer for
> which statements; the only important thing to note is that for Pi_1
> statements, two entirely different readings are possible.
>
> Now for the puzzle.  Most working mathematicians believe that there is a
> very close relationship between the activity of Computer A and the activity
> of Computer B.  For example, in the case of FLT, they believe that the
> proof of FLT *explains* why Computer A is failing to find a solution to the
> Fermat equation.  When they study the proof of FLT, their internal mental
> state gradually changes until they reach a point when they say they
> "understand" the proof, and at that point they arrive at a conviction that
> Computer A is doomed never to find a solution.  Note that this conviction
> is of a type that can never be achieved solely through empirical
> observation of Computer A---empirical observation alone can lead only to a
> "conjecture" and not a "theorem."  Computer B plays the role of verifying
> that the alleged proof satisfies certain conditions---or as we more
> commonly say, that the proof is "correct"---and hence its behavior
> contributes vitally to the *explanation* of the behavior of Computer A.
>
> I claim that for the ultrafinitist, this behavior of working
> mathematicians is very puzzling.  Over time, the ultrafinitist can observe
> that the mathematical community is very good at predicting the results of
> certain computations, and that if asked for the source of their success,
> they reply by pointing to proofs.  For the ultrafinitist, however, *proofs
> have no semantic content*.  They do not make any assertions "about"
> anything.  Taken at face value, they appear to make assertions about
> integers and equations and elliptic curves and modular forms, but for the
> ultrafinitist such things do not "exist."  In particular, terms in a formal
> language do not refer to integrated circuits and flash drives and
> flatscreen monitors and the rest of the physical components of a computer.
> I claim that it is therefore totally mysterious why the activity of
> Computer B should have *anything at all to do* with explaining the behavior
> of Computer A.  This mystery I refer to as "the unreasonable soundness of
> mathematics."
>
> The working mathematician is accustomed to *abstracting* the behavior of
> the physical computer and *reasoning* about the abstract objects, but the
> process of abstraction, or at least the resulting abstract object, is
> precisely what the ultrafinitist is skeptical about.  Indeed, we may recall
> Voevodsky's famous (or infamous?) talk, in which he seemed to suggest that
> perfectly correct proofs of "PA is consistent" in standard foundational
> systems give us no reason to believe that PA is consistent. I interpret
> Voevodsky to be arguing that in the case of "PA is consistent," the
> behavior of Computer B tells us nothing about the behavior of Computer A.
> The only thing I would add is that there appears to be nothing special
> about "PA is consistent" in this regard.  It seems to me that if we share
> Voevodsky's skepticism, then we should also be skeptical that (for example)
> the standard proof that sqrt(2) is irrational tells us anything at all
> about what to expect if we program Computer A to search for positive
> integers X and Y such that X^2 = 2*Y^2.  In other words, it seems to me
> that the skeptical argument runs much deeper than any skepticism about
> specific axioms.
>
> ---
>
> That concludes the first part of my discussion.  I would now like to
> suggest that the above viewpoint suggests a possible avenue for convincing
> the ultrafinitist to regard certain abstract mathematics as being real.
>
> It seems to me that much of the skepticism about the existence of abstract
> infinitary objects has its roots in physical intuition.  That is, it is
> tacitly assumed that the acquisition of knowledge about physical objects
> through sense perception is a well-understood phenomenon.  After all, I
> have never heard anyone go on and on about the "unreasonable effectiveness
> of vision in providing knowledge about the physical universe"; it is not
> regarded as puzzling, and in need of further explanation, how human beings
> can possibly acquire knowledge of physical objects---or at least, it is
> regarded as much *less* puzzling than how we could possibly acquire
> knowledge of an abstract object such as an elliptic curve.  But if physics
> is regarded as a gold standard of some kind, then we can argue that
> knowledge of abstract objects is in fact entirely analogous to knowledge of
> physical entities that are not directly perceptible.  An "electron" in
> quantum field theory is not something that is directly accessible to our
> senses.  Rather, it is an *abstract* theoretical entity that is posited in
> order to explain the results of experiments, and it cannot even be
> correctly conceptualized in commonsense terms such as "particle" or
> "wave."  Similarly, elliptic curves are theoretical objects that are
> posited to explain the results of computer searches, and so we should not
> balk at accepting their reality any more than we should balk at accepting
> the reality of electrons.
>
> ---
>
> Finally, let me address a potential objection.  In the past, I have
> complained that discussions about the "unreasonable effectiveness of
> mathematics in physics" rarely take the trouble to articulate what
> *reasonable* effectiveness would look like.  If we cannot give a clear
> account of how much effectiveness we can "reasonably" expect, then how can
> we be sure that the amount of effectiveness that we actually observe is
> really "unreasonable"?  Perhaps this is just another manifestation of the
> all-too-human tendency to see amazing patterns in randomness.  Similarly,
> someone might object that if one considers the connection between Computers
> A and B to be puzzling, then what on earth is *not* puzzling? Surely the
> proof that sqrt(2) is irrational is more of a gold standard for explanation
> than quantum field theory is, given that the latter is still riddled with
> mathematical gaps.
>
> In response to this objection, I would raise the stakes and draw attention
> to Harvey Friedman's Pi_1 propositions that imply the 1-consistency of some
> large cardinal axiom and that are themselves implied by a slightly larger
> cardinal axiom.  Specifically, I ask, do the formal proofs of these
> propositions allow us to predict the behavior of the relevant Computer A
> with unshakable confidence?  I think that many people would balk here. But
> if you balk at large cardinal axioms, then what is your account of the
> relationship between Computer B and Computer A?  Are the proofs of Computer
> B doing more than just "explaining" the physical behavior of Computer A in
> the sense that physical theories "explain" physical phenomena?  If so, then
> in what sense are they doing more, and how do we pick which axioms to
> accept?  There seems to be some kind of puzzle here even for those who lack
> sympathy for the ultrafinitist position (though perhaps this is nothing
> than the usual puzzle of which axioms for mathematics to accept).
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160430/997aa3d7/attachment-0001.html>