Does this work? Use the Bellantoni-Cook theorem 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.