[FOM] Fast-growing functions and P = NP

[Timothy Y. Chow]

Recently I looked briefly at some work of da Costa and Doria on P = NP. 
Their main publication on this topic is incorrect, as various people have 
pointed out.  However, it made me think of the following question, which
I'm sure someone here can answer immediately.

Fix some standard enumeration of polynomially clocked Turing machines.
Define f as follows: Given a polynomially clocked machine M, let

    f(M) = length of the shortest SAT instance on which M errs.

(Let f(M) = infinity if no such SAT instance exists.)  Now let

    F(n) = max_{|M|=n} f(M).

The maximum is taken over all polynomially clocked machines of size n.
Question: Would a strong lower bound on F imply that P != NP is unprovable 
in some corresponding fragment of arithmetic?

Tim