[FOM] Reasons for choosing between EFA and WKL*0?

[Colin McLarty]

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>