_Asumo aquí que te refieres a lógica de segundo orden con la semántica estándar, en contraposición a la de Henkin._
Resulta que la respuesta es no: la situación es mucho, mucho peor de lo que puede parecer a primera vista.
Vamos a ignorar por completo los sistemas deductivos y solo observemos el conjunto de valideces de segundo orden, es decir, el conjunto $Val_2$ de las valideces de segundo orden (= oraciones de segundo orden que son verdaderas en cada modelo según la semántica estándar). Intuitivamente, estas son las que deberían ser demostrables si nuestro sistema de pruebas es completo, y si tienes un sistema de pruebas del tipo que describes, entonces al buscar a través de todas las posibles pruebas tendríamos que $Val_2$ es recursivamente enumerable. Así que tu pregunta es realmente un aspecto de:
¿Cuál es la complejidad computacional del conjunto $Val_2$?
La respuesta resulta ser: realmente enorme. Por ejemplo, ni siquiera está en la jerarquía aritmética en absoluto _(entonces en particular, el teorema de Post nos dice que la respuesta a tu pregunta es no)_, o incluso hiperaritmética, entonces en cierto sentido no puedes averiguar si una oración de segundo orden es válida incluso si pudieras iterar el salto de Turing "tantas veces como quieras".
En este punto, es un buen ejercicio demostrar un pequeño fragmento de la afirmación anterior: muestra que hay una secuencia computable de oraciones de segundo orden $\psi_i$ tal que para cada $i$, $\psi_i$ es válida si y solo si $i$ no está en el problema de la detención. Dado que el complemento del problema de la detención no es c.e., esto dará una respuesta negativa a tu pregunta. PISTA: primero muestra que hay una oración de segundo orden $\varphi$ que caracteriza a $(\mathbb{N}; +,\times)$ hasta el isomorfismo, luego piensa en cómo describir las máquinas de Turing en el lenguaje de la aritmética...
Otro aspecto importante de la terribilidad de la lógica de segundo orden (con la semántica estándar) - no directamente relacionado con tu pregunta, pero importante para desarrollar una intuición sobre el tema - es su dependencia de la teoría de conjuntos (lo que ha llevado a un debate sobre si incluso califica como una lógica adecuada; no voy a entrar en eso aquí, pero si estás interesado puedes buscar el trabajo de Quine, Shapiro y Vaanaanen sobre el tema). Específicamente, si una oración de segundo orden es válida puede depender de principios teóricos de conjuntos que no son ni demostrables ni refutables a partir de los axiomas usuales de la teoría de conjuntos!
El ejemplo estándar es que hay una oración de segundo orden $\chi$ que es válida si y solo si la hipótesis del continuo es verdadera. Construir $\chi$ requiere un poco de trabajo pero en última instancia no es demasiado difícil, y revela la cualidad "contingente en la teoría de conjuntos" de la lógica de segundo orden (especialmente a la luz del forcing, que muestra que podemos cambiar si una oración de segundo orden es válida o no alterando el universo teórico de conjuntos, mientras que la lógica de primer orden es mucho más "absoluta").
$^1$Pero no completamente, posiblemente.
