Cómo es el teorema de la forma normal de Kleene para $\Sigma^1_1$ ¿relaciones probadas en RCA0?

Question

Todo lo siguiente se refiere a Simpson's Subsistemas de aritmética de segundo orden (2ª ed.).

En las notas posteriores a los lemas VII.1.6 y VII.1.7 (pp. 245-246), Simpson señala que ambos lemas son demostrables en $\mathsf{RCA}_0$ aunque las pruebas dadas requieren $\mathsf{ACA}_0$ no sólo porque se basan en una versión formal del teorema de la forma normal de Kleene para $\Sigma^1_1$ relaciones: lema V.1.4 (pp. 169-170).

¿Es este teorema de la forma normal demostrable de hecho en $\mathsf{RCA}_0$ ?

---

(Teorema de la forma normal de Kleene) Dejemos que $\varphi(X)$ ser un $\Sigma^1_1$ fórmula. Entonces podemos encontrar una fórmula aritmética (de hecho $\Sigma^0_0$ ) fórmula $\theta(\sigma, \tau)$ tal que $\mathsf{ACA}_0$ prueba

$$\forall{X}(\varphi(X) \leftrightarrow \exists{f}\forall{m} \theta(X[m], f[m])).$$

(Aquí $f$ se extiende sobre las funciones totales de $\mathbb{N}$ en $\mathbb{N}$ . También

$$X[m] = \langle \xi_0, \xi_1, \dotsc, \xi_{m-1} \rangle$$

donde $\xi_i = 1$ si $i \in X$ , $0$ si $i \not\in X$ . Tenga en cuenta que $\varphi(X)$ puede contener variables libres distintas de $X$ . Si este es el caso, entonces $\theta(\sigma, \tau)$ también contendrá esas variables libres).

---

La comprensión aritmética se utiliza en la demostración del teorema de la forma normal para mostrar que $\varphi(X)$ se mantiene si existen funciones de Skolem para $X$ . Por tanto, una forma de demostrar que este lema es demostrable en $\mathsf{RCA}_0$ sería mostrar que la comprensión recursiva es suficiente para demostrar esta equivalencia.

Answer 1

Ciertamente, la forma fuerte del teorema de la forma normal -donde controlamos la complejidad de la matriz aritmética- no es demostrable en RCA $_0$ .

Esto se desprende de la consideración del modelo $REC$ de conjuntos recursivos. En $REC$ podemos convertir los cuantificadores de segundo orden en cuantificadores de primer orden, ya que basta con cuantificar sobre índices para máquinas de Turing totales . (A simple vista, creo que cada cuantificador de segundo orden se convierte en tres cuantificadores de primer orden). En particular, toda fórmula es (equivalente a) una fórmula analítica en el sentido amplio de matriz no limitada. Sin embargo, una fórmula analítica cuya matriz es $\Sigma^0_n$ es equivalente (en $REC$ ) a un $\Sigma^0_{2+n}$ -los argumentos habituales para producir una fórmula $\Sigma^0_k$ fórmula que no equivale a ninguna $\Sigma^0_m$ fórmula para $m<k$ pasan por aquí, por lo que el teorema de la forma normal (fuerte) no puede sostenerse.