Does this work? Use the [Bellantoni-Cook theorem][1] to enumerate all the polynomial time Turing machines.  If P=NP you will eventually run into a machine that you can recognize as running Levin's universal search algorithm on some NP-complete problem.  That proves Levin's algorithm on that problem runs in P-time and therefore P=NP.  The paper also cites a result of Leviant that

> a function is polytime if and only if it can be proved convergent in the logical system $L_2(QF^+)$ using the function’s recursion equations and a 'surjective' principle.  Here $L_2(QF^+)$ is second order logic with comprehension (i.e., definability of sets) for positive quantifier-free fomulas.

which might be of use to you.

  [1]: http://www.cs.toronto.edu/~sacook/homepage/ptime.pdf%20Bellantoni-Cook%20theorem