[FOM] Formalization Thesis vs Formal nature of mathematics

[messing]

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