[FOM] Ineffective proofs and weak systems

[Harvey Friedman]

On 2/27/04 9:48 AM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

> There's a simple point about ineffective proofs that I'm confused about.
> Consider the following famous theorems of number theory.
> 
> Mordell's finite basis theorem: The group G of rational points on an
> elliptic curve defined over Q is finitely generated.
> 
> Roth's theorem: For every algebraic alpha and every k > 2, there exist
> only finitely many rationals p/q satisfying |alpha - p/q| < 1/q^k.
> 
> The proofs are notorious for being ineffective.

>... Now, what I'm confused about is, does this present any obstacle
> to formalizing the proof in, say, RCA_0?
> 
> Perhaps I'm confusing "recursive mathematics" (as represented by RCA_0)
> with intuitionism?
> 

Yes you are. 

I don't know that anybody has looked at the first example to see if it can
be proved in RCA0. I remember looking at the second example, and seeing that
it can be proved in RCA0.

If an AE sentence is true then there is obviously an effective way of going
from A to E. 

If an AE sentence is provable in RCA0 then there is a primitive recursive
way of going from A to E.

If an AEA sentence is true then there may not be an effective way of going
from A to E.

If an AEA sentence is provable in RCA0 then there may not be an effective
way of going from A to E.

If an AEA sentence is provable in various intuitionistic systems, then there
is an effective way of going from A to E.

Here is an example. Let n1 >= n2 >= n3 >= ... be a primitive recursive
sequence of natural numbers. Then it is eventually constant.

This is true, and this is provable in RCA0, and this is not provable in any
reasonable intuitionistic system.

Harvey Friedman