I had an informal conversation in which I was told that logical systems could be intuitively drawn in a hierarchy according to their expressive power, i.e. the amount of things we can prove with them. This hierarchy, would be infinitely dense, but some points have been studied and have special names. Here is a list of names in order of strength:
Presburger arithmetic
Presburger arithmetic with bitwise operators
——– we end the decidable side
Robinson arithmetic
First-order peano arithmetic
System T
System F (maybe System F is not strictly stronger than System T?)
———big gap: set theories are much more powerful
Zermelo's set theory (somewhat equivalent to higher-order logic in
power)Fraenkel axioms allowing to speak about certain ordinals
Axioms of existence of large cardinals…………
I want to know more about this hierarchy. Is there a comprehensive study or some sample analysis of the hierarchy?
In that respect, Is there an overview of several logical systems? does not count as a duplicate since the focus there is non-classical logics, here I think everything is fairly classical.
Best Answer
I don't know of a good source which covers this whole spectrum. That said, there are a variety of sources covering different pieces of it. Below I'll describe how I view this hierarchy of systems, and say specifically which texts I have in mind - texts by Hajek/Pudlak, Simpson, Mathias, Jech, and Kanamori. (I've copied the links below as well, so you don't have to bounce around in this answer.)
I'm not an expert (to put it mildly) in decidable theories or even "ultraweak" theories like $\mathsf{Q}$, so I'll only go as low as theories which admit "reasonably simple" coding of finite sequences. Moreover, I'll only consider three languages for the theories in question: first-order arithmetic (e.g. $\mathsf{PA}$) possibly augmented with additional symbols for natural functions like exponentiation, second-order arithmetic (e.g. $\mathsf{RCA_0}$), and set theory (e.g. $\mathsf{ZFC}$).
Here, then, is the hierarchy as I perceive it:
We begin with the "not-too-weak" first-order arithmetics. Personally I'd draw the line at $\mathsf{I\Delta_0+exp}$; this theory consists of the basic "$+/\times/<$" properties of $\mathbb{N}$ without induction, the induction scheme restricted to $\Delta_0$ formulas, and an axiom asserting that exponentiation is total and satisfies the usual recursive definition. This is the weakest natural theory of arithmetic which allows "easy" coding of finite sequences. Climbing up from here we get theories like $\mathsf{I\Sigma_n}$ (the basic properties plus $\Sigma_n$-induction) and $\mathsf{B\Sigma_n}$ (a more technical variant of $\mathsf{I\Sigma_n}$) which satisfy $$...<\mathsf{I\Sigma_n<B\Sigma_{n+1}<I\Sigma_{n+1}}<...$$ These climb all the way up to $\mathsf{PA}$, and $\mathsf{PA}$ proves "$\mathsf{I}\Sigma_n$ is consistent" for each $n$ (although of course $\mathsf{PA}$ does not prove "$\mathsf{I\Sigma_n}$ is consistent for each $n$"). The standard text here is Metamathematics of first-order logic.
$\mathsf{PA}$ is in my opinion the strongest "natural" theory of first-order arithmetic, so going above it I'll switch to the context of second-order arithmetic. A relevant term here is reverse mathematics. Typically the weakest theory considered here is $\mathsf{RCA_0}$, which is conservative over $\mathsf{I\Sigma_1}$; a couple theories up we get $\mathsf{ACA_0}$, which is conservative over $\mathsf{PA}$. Then higher up we get things like $\mathsf{ATR_0}$ which are much stronger than $\mathsf{PA}$. The strongest common theory in reverse mathematics is $\Pi^1_1$-$\mathsf{CA_0}$, and then we keep going through higher levels of the second-order comprehension hierarchy. At the top of these sits $\mathsf{Z_2}$, which has comprehension for all second-order formulas and bears essentially the same relation to the $\Pi^1_n$-$\mathsf{CA_0}$s as $\mathsf{PA}$ does to the $\mathsf{I\Sigma_n}$s. The standard text here is Subsystems of second-order arithmetic.
At this point we switch over to set theory. As with the transition between first- and second-order arithmetics, things "glue together" long before we need to make the shift: the weakest set theory I know much about here is $\mathsf{KP\omega}$ (Kripke-Platek + Infinity), which is weaker in consistency strength than $\mathsf{ATR_0}$ (which is itself weaker than $\Pi^1_1$-$\mathsf{CA_0}$). That said, there is also the surprisingly-weak set theory $\mathsf{Z}$ (= $\mathsf{ZFC}$ without $\mathsf{Replacement}$ or, less importantly, $\mathsf{Choice}$). Mathias has an epic paper about these systems, but it's quite technical.
Then there's a big gap.
The gulf between things like $\mathsf{Z+KP}$ and $\mathsf{ZF}$ is ridiculously huge, and I don't know a good source that covers that range. There are some famous results here, e.g. Harvey Friedman's analysis of the role of $\mathsf{Replacement}$ in Borel determinacy, but for the most part this is territory I don't know anything about. My knowledge kicks back in at $\mathsf{ZF}$. Of course here we have a huge amount of robustness, e.g. the agreement in consistency strength between $\mathsf{ZF}$, $\mathsf{ZFC+V=L}$, $\mathsf{ZF+DC}$ + "Every set of reals has the Baire property," and so on. The study of e.g. fragments of the axiom of choice over $\mathsf{ZF}$ doesn't play with consistency strength at all, although of course we see huge changes in what we can prove in general.
And then ...
Large cardinals.
Yippee!
There are two standard texts here: Kanamori's Higher infinite and Jech's Set theory. Very roughly, there are three "blocks" of large cardinal axioms:
The small large cardinals. Basically, these are the ones compatible with $\mathsf{V=L}$. They include inaccessibles, Mahlos, weakly compacts, and so on - more-or-less at the top of this are the remarkable cardinals.
The medium large cardinals. The natural starting point here is $\mathsf{0^\sharp}$, which technically isn't a large cardinal but fits the picture; a bit higher is the easier-to-explain measurable cardinal, and a fair way above are the Woodin cardinals. Strength-wise, the characterizing feature of these cardinals I have in mind is that, while incompatible with $\mathsf{V=L}$, they still have well-understood inner model theory. However, there's another important phase transition which happens here: large cardinals at this and the next level are connected with "large-scale" model-theoretic phenomena, even if they have "local" characterizations. E.g. we can prove (in an appropriate conservative extension of $\mathsf{ZFC}$) that there is a measurable cardinal iff there is a nontrivial elementary embedding of $V$ into some inner model, and this was in fact how Scott proved that measurables are incompatible with $\mathsf{V=L}$.
And then we get the large large cardinals, which are beyond the reach of current inner model theory. Supercompacts and rank-into-rank cardinals are perhaps the most famous, although I also want to plug Vopenka's principle here, if only because of its hilarious history.