No me atrevo a responder negativamente, porque en cuanto lo haga, alguien publicará algún dato interesante que yo desconozca. - pero sospecho que la respuesta a su pregunta es no Actualmente no se conoce ninguna axiomatización agradable de este tipo.
¿Por qué? Usted menciona $ACA_0$ . Pues que las consecuencias aritméticas de ZF son mucho mucho mucho mucho más que los de $ACA_0$ por ejemplo, ZF demuestra la consistencia de $ACA_0$ por no mencionar $ATR_0$ , $\Pi^1_1-CA_0$ , $Z_2$ , $Z_3$ , . . . , $Z_\omega$ , . . . , $KP$ , . . . , $Z$ (= teoría de conjuntos de Zermelo), . . . En términos más generales, supongamos $\alpha$ es un ordinal "razonablemente definible" (por ejemplo $\omega_1, \omega_2, \omega_\omega, ...$ ). Entonces $ZF$ demuestra que $V_\alpha$ existe y, por tanto, que $Th(V_\alpha)$ es coherente.
Ahora, $ZF$ no puede decidir qué $Th(V_\alpha)$ es en general (¿es cierta la hipótesis del continuum? eso es una cuestión de $Th(V_{\omega+3})$ ), pero $ZF$ podrá demostrar que cierta las cosas están en $Th(V_\alpha)$ (por ejemplo $ZF$ demuestra que $V_{\omega+\omega}$ es un modelo de $Z$ ). Así que podemos tomar "grande" definible $\alpha$ s, y aislar "subteorías conocidas" de $Th(V_\alpha)$ y $ZF$ demuestra la consistencia de estas teorías - y esto nos da una clase verdaderamente desalentadora de consecuencias aritméticas de $ZF$ . Antes incluso de empezar a hacer nada interesante, ya hemos dejado muy atrás el ámbito de las teorías conocidas de la aritmética.
Se me ocurre otra vuelta de tuerca a esta cuestión. Supongamos que quiero describir las consecuencias aritméticas de alguna teoría más fuerte ZFC+X (conociéndome, X es probablemente una propiedad cardinal grande :P). Bueno, eso va a ser aún más difícil que describir las consecuencias aritméticas de ZFC. Pero, tal vez pueda "reducir" el problema de ZFC: ¿qué pasa si sólo quiero un conjunto axiomatizado "bonito"? $\Gamma$ de sentencias aritméticas tales que tal vez $\Gamma$ no agota las consecuencias aritméticas de ZFC+X, pero las consecuencias aritméticas de ZFC+ $\Gamma$ ¡son exactamente las consecuencias aritméticas de ZFC+X!
Digamos que tal $\Gamma$ "captura ZFC+X aritméticamente sobre ZFC". Entonces: para "naturales" tales X (cardinales grandes, nociones de forzamiento, enunciados sobre aritmética cardinal, etc.), ¿podemos encontrar "naturales" $\Gamma$ que capturan aritméticamente ZFC+X sobre ZFC?
Que yo sepa, no existe ningún ejemplo de este tipo. Obsérvese que incluso ZFC+"Con(ZFC+X)" no capta en general las consecuencias aritméticas de ZFC+X: ZFC+X tendrá algunas consecuencias aritméticas de alta complejidad (en el sentido de la jerarquía aritmética mientras que las declaraciones de coherencia son meramente $\Pi^0_1$ y podemos encontrar, por ejemplo, verdadero $\Pi^0_2$ sentencias que no son demostrables desde ZFC + todos verdadero $\Pi^0_1$ ¡frases! (Si no recuerdo mal, "ZFC es $\Sigma^0_1$ correcta" es tal afirmación).
Y la misma situación parece darse con respecto a la descripción de las consecuencias aritméticas de ZFC "modulo" más pequeño teorías, como KP o Z.
De nuevo, sin embargo, este no es mi campo de especialización, ¡así que estaré encantado de que me corrijan si se sabe algo en este sentido!
3 votos
¿Por qué los votos para cerrar? Me parece una buena pregunta.