I recently made this diagram to help visualize some of the important first- and second-order arithmetic theories. Maybe it will help some of you out in understanding how they all fit together.

Second order arithmetic

The vertical division represents the languages used by these theories. Intuitively, theories on the left side can only understand statements about the natural numbers, while theories on the right side can understand statements about the real numbers.

Some shapes are semicircular or otherwise "snug-fitting." These are meant to be exact. In particular, PRA is exactly the first-order theorems of RCA0, WKL0 extends RCA0 only in its second-order part, and PA is exactly the first-order theorems of ACA0.

To help make this scale more familiar, we'll compare it to some familiar functions:

Second order arithmetic with googology

Notice how the proof-theoretic ordinals of these theories compare with the FGH ordinals we use to estimate these functions:

  • EFA has proof-theoretic ordinal \(\omega^3\). It is dominated by tetration, which reaches roughly \(f_3\).
  • PRA, RCA0, and WKL have proof-theoretic ordinal \(\omega^\omega\). They are dominated by Ackermann functions, xE#, and arrow notation, which reach \(f_\omega\). They are also dominated by chained-arrow notation, which reaches \(f_{\omega^2}\).
  • PA and ACA0 have proof-theoretic ordinal \(\varepsilon_0\). They are dominated by the Goodstein function, BEAF, E^, and Hydra, which reach \(f_{\varepsilon_0}\).

The PTO/FGH comparisons don't seem to work for EFA and PRA... until you realize that replacing FGH with the Hardy hierarchy makes it all work out. For example, EFA has PTO \(\omega^3\), and tetration reaches \(H_{\omega^3}\). This suggests the Hardy hierarchy as a more natural choice for comparing with googological functions.

The \(f_\omega\)-level (or should I say \(H_{\omega^\omega}\)) functions get squashed in with chained-arrow notation, which we know is significantly stronger. If the Big Five had a finer division between WKL0 and ACA0, this might not be the case.

To put everything here into perspective, I estimate that 90% of theorems ever published in professional mathematics are provable in RCA0. Most of the ones about combinatorics and number theory are in that tiny oval labeled EFA.

ZFC is a huge oval containing all of these and many more. (Although drawing it into the diagram would be technically incorrect since it doesn't use the language of first-order or second-order arithmetic.)