[FOM] Formalization Thesis vs Formal nature of mathematics
messing
messi001 at umn.edu
Mon Dec 31 08:42:36 EST 2007
Sazonov wrote:
I know no particular exclusion from the formalist paradigm. If you mean
something like informal "deriving" consistency of PA, I will call this
just a speculation which leads to diminishing the role of mathematical
rigour and thereby wrecking the backbone of mathematics. For this
speculation counter-speculations can be presented. Consis_PA, as a
formula of PA, does not express adequately the consistency of PA
because consistency should refer to formal proofs of feasible length
whereas PA deals with both feasible and non-feasible finite objects. I
see no way of "deriving" consistency of PA except belief. What could we
say if it is, in fact, inconsistent? Beliefs are something outside of
science. Science is not a theology.
------------------------------------------------------------------------
I do not understand what is meant here by "Consis_PA as a formula of PA,
does not adequately express ...." Is it being asserted that there is
some meaningful notion of "feasible length" for a proof in PA, or in any
other branch of mathematics? If so, can one make explicit an upper
bound for the length, say in terms of written lines of text, for the
concept of "feasible length". Would the Skewes number serve as such an
upper bound, or 10^{10^{79}} or ...? If, eventually the Riemann
Hypothesis is proven and the proof is published in the Annals of
Mathematics in a paper which is 100,000 pages long, would this qualify
as "feasible length"?
-------------------------------------------------------------------------
Sazonov wrote:
I know that FLT was proved (to be 'true'), and know virtually nothing
on the proof. This is almost absolutely useless knowledge. It cannot be
used, unlike the proof and definitions, constructs and algorithms (and
corresponding intuitions) involved in the proof.
------------------------------------------------------------------------
I do not understand the "this is almost useless knowledge." For
arithmetic geometers, it is actually the result that Taylor-Wiles
proved, the conjecture of Shimura-Taniyama-Weil, stating that all
elliptic curves defined over Q are modular, which is important. It was
known that it implied FLT. This result of Taylor-Wiles is effectively
employed by number theorists, or those working on automorphic forms, to
prove new and important theorems, even though these mathematicians have
not necessarily studied the proof of Taylor-Wiles. To take another
example: Neron proved in the early 1960's (there is a Seminaire Bourbaki
expose in which he announced his result and then the full proof was
published in 1964 in the Publ. Math. IHES, volume 21) the existence of
"Neron models" for abelian varieties defined over the fraction field of
a Dedekind domain. He employed Andre Weil's algebro-geometric language,
rather than the Grothendieck language of schemes. For many years most
algebraic geometers found it essentially impossible to penetrate Neron's
paper, two notable exceptions being Michael Artin and Michel Raynaud,
who genuinely understood Neron's result in scheme-theoretic terms.
Nevertheless from the first moment it was announced, arithmetic
geometers were able to effectively use the existence of Neron models as
a BLACK BOX and to prove many interesting theorems based on formal use
of it. The same can be said concerning formal use of Hironaka's theorem
on resolution of singularities. To know that a smooth variety, X, over
a field of characteristic zero can be compactified to a smooth proper
variety, Y, such that Y \ X is a unionm of divisors with normal
crossings, is a powerful tool, but again it can be employed as a BLACK BOX.
William Messing
More information about the FOM
mailing list