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.

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.

(Hmm, I don't know if the BC theorem actually lets you enumerate the P-time Turing machines, or just syntactic descriptions of the languages, that might not get you all the recognizers. I better read the paper more carefully).

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 Levin's universal search algorithm. That proves Levin's algorithm runs in P-time and therefore P=NP.

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.