[FOM] logical complexity of mathematical statements

[Timothy Y. Chow]

On Wed, 14 Oct 2015, Harvey Friedman wrote:
> Effectively computable is nice but extremely weak. What more does it
> give? Say a small finite exponential stack?

I don't know the machinery well enough to give a precise answer, but I 
believe that your guess is correct.  People have implemented the 
algorithms and have used them to solve actual equations, so the complexity 
can't be that bad.  I just looked at Wikipedia and it appears to give a 
fairly detailed explanation, probably enough to answer the question if you 
spend a little time studying it.

Tim