[FOM] Faithful Formalisation

[Timothy Y. Chow]

Alan Weir wrote:

> The faithful formalisation should attempt to formalise the branch of 
> algebraic topology or p-adic representation theory using the proper 
> concepts of the theory as primitives and capture the structure of the 
> proof, filling in the gaps with inference steps used by the 
> practitioners.

The trouble I see with this approach is that in actual practice, 
mathematics does not split up into separate branches that each have their 
own "proper concepts."

Sometimes you'll find concept A defined in terms of concept B in one paper 
and concept B defined in terms of concept A in another.  People are not 
terribly picky about what concepts you use or how you define them as long 
as the precision is sufficient unto the day thereof.  Say a paper starts 
with, "Let E be an elliptic curve over Q."  What does that mean?  Is an 
elliptic curve a set of points?  A projective variety?  An equation?  A 
group scheme?  It can be all these things.  If you want to define it 
purely arithmetically then nobody will blink, so long as your definition 
provides sufficient support for your argument.  If you want to define it 
some other way, then again nobody will blink, and they will not 
necessarily think that you have changed the ground rules as long as it is 
known how to move between the two definitions.

Against such a background, I think that if an argument that superficially 
employs "geometric" concepts is restated by redefining the so-called 
"geometric" concepts arithmetically, then mathematicians will not usually 
regard the argument as having materially changed.  Two arguments are 
considered the same if they follow the same general chain of thought and 
if the hard parts show up at the same spots and are circumvented using the 
same tricks.  If some "geometric" concept is reformulated in "analytic" 
language or "arithmetic" language or whatever, but in a routine way, then 
it won't be considered a material change to the argument.

If the Frey-Serre-Ribet-Wiles-Taylor proof is somehow formalized in PA in 
such a way that all the main steps are recognizably there and the 
obstacles are overcome using the same kind of arguments, then I think most 
mathematicians will regard it as a faithful rendition.  That the formalism 
happens to be cast, at the micro level, in the language of arithmetic, is 
largely irrelevant.  To be sure, we'll want the proof to mention elliptic 
curves and modular forms and so forth, but if these concepts are defined 
arithmetically then everything will be fine.

Tim