[FOM] logical complexity of mathematical statements

[Timothy Y. Chow]

Harvey Friedman wrote:

> "Linearly independent logarithms of algebraic numbers are
> algebraically independent" by similar reasoning seems to be Pi03. Look
> at Baker's Theorem, a special case. Does Baker give a bound for the
> corresponding Pi03 statement, and if so, what kind of bound?

Yes, if L_1, ..., L_n are the linearly independent logarithms of algebraic 
numbers and a_0, ..., a_n are algebraic numbers (not all zero) then Baker 
gives an effectively computable nonzero lower bound for

   | a_0 + a_1 L_1 + ... + a_n L_n |

Tim