[FOM] Weaker foundations for FLT

[Harvey Friedman]

On 3/2/06 12:16 PM, "praatika at mappi.helsinki.fi"
<praatika at mappi.helsinki.fi> wrote:

> Solovay wrote:
> 
>> As the cited book shows the Wiles-Taylor proof is a truly
>> enormous beast. The work naturally seems to be carried out in third
>> order number theory, and to compress it into PA seems a heroic if not
>> impossible task.
> 
> Not that I know much about FLT and related issues, but nevertheless...
> this is not necessarily a problem: Feferman has formulated certain theories
> of finite types, suitable for a direct formalization of ordinary
> mathematics, which are conservative over PA. If the third order stuff can
> be carried out in such a system, it follows that FLT is after all provable
> in PA.  
> Right?

My favorite large conservative extensions of PA are in my two papers:

Set Theoretic Foundations for Constructive Analysis, Annals of
Mathematics, Vol. 105, (1977), pp. 1-28.

A Strong Conservative Extension of Peano Arithmetic, Proceedings
of the 1978 Kleene Symposium, North Holland, (1980), pp. 113-122.

These are both set theories with intuitionistic logic, and the axioms are
very uncluttered. The first is completely intuitionistic, and is meant to be
a convenient formalization for constructive mathematics roughly along the
lines of Bishop. 

The second is partly intuitionistic. The underlying logic is intuitionistic,
but it is classical at lowest type. It has what Bishop called "the limited
principle of omniscience".

Both have power set in the form of set exponentiation. This supports a
flexible array of finite types. Of course, all proposed conservative
extensions, including Feferman's, are not going to support seriously
impredicative definitions.

I assume that in the proof of FLT, as done now, one can spot seriously
impredicative definitions? This would render the plan you have in mind
impossible.

Harvey Friedman