FOM: Eliminability of analytical notions from the proof of elementary theorems: a question to Friedman

[dubucs]

Harvey Friedman wrote (28 Oct 1999 02:56:24 -0500):

> For instance, I have been pushing the program of showing that all of the
>famous number theoretic results of the 20th century (and earlier) can be
>proved within EFA = exponential function arithmetic. I conjecture that
>Mordell's Conjecture and Fermat's Last Theorem can be proved in EFA. Some
>world famous number theorists are quiite interested in this conjecture. It
>leads to a whole host of related investigations cast in "traditional
>foundational schemes." E.g., I recently posted a sketch (#56) that EFA is
>enough to prove the consistency of elementary algebra and geometry; and in
>fact, a whole host of theorems about elementary algebra and geometry to the
>effect that if you use elementary algera and geometry to prove a number
>theoretic result, then you can eliminate the elementary algebra and
>geometry in favor of elementary number theory.

Could you give to the members of FOM some idea of the ratio between the
length of the original (analytical) proof and the length of the elementary
proof which replaces it ?

Thanks,

Jacques Dubucs
IHPST CNRS Paris I
13, rue du Four
75006 Paris
Tel (33) 01 43 54 60 36
    (33) 01 43 54 94 60
Fax (33) 01 44 07 16 49