For common theories that talk about something more general than first-order arithmetic (e.g. set theories and subsystems of second-order arithmetic), are there nice axiomatizations of their arithmetic parts? I know that the arithmetic part of $ACA_0$ is $PA$ and the arithmetic parts of $RCA_0$ and $WKL_0$ are both $I\Sigma^0_1$, and I'm mostly interested in stronger theories (like $\Delta^1_1-CA$, $ATR_0$, $\Pi^1_1-CA$, $Z_2$, $KP$, $ZFC$). I'm also aware that Craig's theorem provides a recursive axiomatization of the arithmetical part of any recursively enumerable theory, but I'm interested in "nice" axiomatizations (basically meaning finite lists of axioms and schemas, where you should be able to tell whether a sentence satisfies a schema by doing some rudimentary syntax-checking instead of anything fancy), instead of using cheap tricks like from the proof of Craig's theorem.
-
2$\begingroup$ Somewhat related: math.stackexchange.com/questions/1989762/… $\endgroup$– Noah SchweberJul 2, 2017 at 1:41
-
$\begingroup$ Surely this is not known for ZFC... $\endgroup$– Will SawinJul 2, 2017 at 4:03
-
1$\begingroup$ @WillSawin Note that it's trivial to provide an axiomatization of the arithmetical consequences of ZFC; I do doubt that a natural axiomatization exists, but surely "surely" isn't justified there. $\endgroup$– Noah SchweberJul 2, 2017 at 18:25
-
$\begingroup$ @NoahSchweber My confidence in the word "surely" is based not on any mathematical argument but just in the fact that, if a natural axiomatization is known, it would be significant enough that I would have heard of it. $\endgroup$– Will SawinJul 3, 2017 at 3:00
1 Answer
A somewhat general method has been explained by Azriel Lévy [Axiomatization of induced theories, Proc. Am. Math. Soc. 12, 251-253 (1961); ZBL0178.31603; MR0122702] The method does not give axioms that are very intuitive, but I think they fit your "rudimentary syntax-checking" criterion as I understand it.
In short, the arithmetical part of ZF is axiomatized by the Peano axioms and all arithmetical sentences which say "if $\Phi \vdash \widehat{\sigma}$ then $\sigma$" where $\Phi$ ranges over finite subsets of ZF, $\sigma$ ranges over arithmetical sentences, $\widehat{\sigma}$ is the sentence in the language of set theory that says that $(\omega;0,1,{+},{\cdot}) \vDash \sigma$. Lévy proves that the same is true for any essentially reflexive theory (a theory that proves the consistency of any finite fragment of itself). Any recursive extension of ZF has this property and I think Z2 also has this property, but finitely axiomatizable theories will not have this property.
-
1$\begingroup$ This is a beautiful result, +1. However, note that in describing the axiomatization we still make reference to ZF itself, and so I don't think this is completely satisfying. $\endgroup$ Jul 2, 2017 at 18:16
-
$\begingroup$ Why is it necessary that the theory be essentially reflexive? It seems like having an $\omega$-model or being sound enough to encode standard proof theory ought to be enough. $\endgroup$ Jun 30, 2018 at 16:23
-
$\begingroup$ Why have $\Phi$ range over finite fragments? Why not simply add all statements of the form "If ZF proves $\hat\sigma$ then $\sigma$"? $\endgroup$ Dec 5, 2021 at 1:38
-
$\begingroup$ On second thought, perhaps that's the arithmetic part of ${\sf ZF}+{\rm Con}({\sf ZF})$, not of $\sf ZFC$. EDIT: Yeah, take $\sigma=F$ $\endgroup$ Dec 5, 2021 at 1:42