[FOM] Reasons for choosing between EFA and WKL*0?
Colin McLarty
colin.mclarty at case.edu
Thu Jan 9 15:30:28 EST 2014
Exponential Function Arithmetic (EFA) has a clear conceptual motivation,
and it is the usual framework for Friedman's conjecture that EFA proves
Fermat's Last Theorem. On the other hand WKL*0 is much more flexible.
Since WKL*0 is Pi^0_2 conservative over EFA, the question of FLT by itself
gives no reason to prefer working with either EFA or WKL*0.
But I want to ask people here what advantages, if any, they see to working
in EFA.
Specifically I am just finishing up a proof of the Artin-Schreier theorem
in EFA. As everyone who works with this knows, a lot of the work is fairly
unenlightening details of coding which would not need to be done in WKL*0.
So am I just wasting time using EFA? Well, it is a good discipline for a
while. But are there objective reasons why it is desirable to prove a
result in EFA, when possible, rather than WKL*0?
best, Colin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140109/4ad23c36/attachment.html>
More information about the FOM
mailing list