Lista finita de axiomas de $\mathsf{ACA}_0$ - ¿referencia?

Question

Parece que es de dominio público que $\mathsf{ACA}_0$ se puede axiomatizar de forma finita, véase por ejemplo

¿Puede expresarse una axiomatización finita de la AP en una teoría de conjuntos de primer orden finitamente axiomatizable?

Sin embargo, no puedo encontrar una referencia donde $\mathsf{ACA}_0$ se da explícitamente con la lista finita de axiomas. Siempre se define como una extensión de $\mathsf{PA}$ que ya tiene un esquema de axiomas infinito.

¿Hay alguna referencia que dé la lista de axiomas finitos explícitamente o el resultado anterior de la axiomatizabilidad finita es una afirmación existencial no constructiva?

Espero que este sea el lugar adecuado para pedir referencias. Borra esto y envíame un PM/Mail si no es así.

Answer 1

Una axiomatización finita para $\mathsf{ACA}_0$ viene dado por el lema VIII.1.5 de Simpson [2009], en las páginas 311-312. Fijar una cara luminosa universal $\Pi^0_1$ fórmula $\pi(e, m_1, X_1)$ con exactamente las variables libres mostradas. Entonces podemos dar una axiomatización finita de $\mathsf{ACA}_0$ de la siguiente manera.

1) Los axiomas básicos, esencialmente los axiomas de la aritmética de Peano menos el esquema de inducción (véase la definición I.2.4 en la página 4 de Simpson [2009]).

2) Un axioma de emparejamiento,

$$\forall{X}\forall{Y}\exists{Z} (Z = X \oplus Y).$$

3) $\Sigma^0_1$ inducción en la forma $$\forall{X}(\neg\pi(e, 0, X) \wedge \forall{m}(\neg\pi(e, m, X) \rightarrow \neg\pi(e, m + 1, X))) \rightarrow \forall{m} \neg\pi(e, m, X)).$$

4) $\Sigma^0_1$ comprensión en la forma

$$\forall{X}\exists{Y}\forall{m}(m \in Y \leftrightarrow \neg\pi(e, m, X)).$$

Lo universal $\Pi^0_1$ fórmula $\pi$ será, por supuesto, algo del tipo que se comenta en la entrada del blog de Peter Smith.

S. G. Simpson. Subsistemas de aritmética de segundo orden . Cambridge University Press, 2ª edición, 2009. doi:10.1017/cbo9780511581007 .

Answer 2

Tengo un blogpost sobre esto en http://www.logicmatters.net/2007/09/14/aca0-3-finite-axiomatizability/ (¡como se ha señalado!).

Sin embargo, la axiomatización finita que se obtiene de este modo no es especialmente bonita ni esclarecedora, ni tampoco tan "natural".