Fermat's Last Theorem and Catalan's conjecture in Weak Exponential Arithmetics
Abstract:
Wiles's proof of Fermat's Last Theorem (FLT) has stimulated a lively
discussion on how much is actually needed for the proof. Despite the fact
that the original proof uses set-theoretical assumptions unprovable in
Zermelo-Fraenkel set theory with axiom of choice (ZFC), it is widely believed
that much less is needed in principle. Harvey Friedman even conjectured that
Fermat's Last Theorem is provable in so called elementary function arithmetic
(EFA) (which is just ISigma_0 + "2^x is total" in a different language).
Smith has showed that EFA proves Fermat's Last Theorem for some small even
exponents n (e.g. for n = 4, 6, 10). On the other hand Shepherdson and
recently Kolodziejczyk constructed models of IOpen and T^0_2 respectively,
where FLT does not hold for n=3.
I will present a joint work with Vítězslav Kala. We consider structures and
theories in the language L^e=(0,1,+,*,e,