Is there a compendium of the consistency strength between the most important formal theories?

Preliminar Notions: A formal system is a tuple $(\Sigma,G,A,R)$ where $\Sigma$ is an alphabet (set of symbols), $G$ is a formal grammar on $\Sigma$ that generates a formal language $L$ (set of well formed formulas -wffs-). $A$ is a formal theory (subset of $L$) called the set of axioms and $R$ is a set of inference rules that determine the mathematical theory (formal theory) derived from the axioms.

A mathematical theory $\tau$ is consistent if it does not have any contradictions. Given two mathematical theories, $s$ and $\tau$, it is said that $s$ is consistent relative to $\tau$ if the consistency of $\tau$ implies the consistency of $s$ ($Con(\tau)\to Con(s)$). We also say that $s$ has greater consistency strength than $\tau$ if $\tau$ is consistent relative to $s$ but $s$ is not known to be consistent relative to $\tau$.

Motivation: In logic it is common practice to analyze the consistency strength of a theory relative to another, and the most popular comparison is made against $ZFC$. There are a lot of theorems in the literature showing $Con(\tau)\to Con(s)$ for $\tau$ and $s$ formal theories and also it is a typical question to ask about the consistency strength of a mathematical theory whenever its formal system is presented/introduced. Based on this, I believe a diagram or a compendium of the consistency strength between the most important formal theories would be useful to have (in order to locate a new formal system quickly in the "hierarchy of consistency strength") but I have not been able to find any on the internet.

The Question: Do you know of a diagram or a compendium of the consistency strength of the most important formal theories studied in mathematical logic? I'm searching for theories that contain enough arithmetic to prove Gödel's Incompleteness Theorems and by important I mean that the formal system that generates the theory has been studied by several mathematical logicians (let's say 25). I'm also searching for diversity, not just relations between large cardinal hypothesis but also systems like Martin-Löf Type Theory or the systems used to study Homotopy Type Theory or Reverse Mathematics.

Extra: If there is none, we can contribute by adding consistency relations as answers and referencing the paper/book where the result comes from.

An Example: $$Con(ZFC)\leftrightarrow Con(ZF) \to Con(PA) \to Con(PRA)$$

On the answer to the question: The answer that fits the most to the requirements of the question is a combination of Joel David Hamkins' answer and the comment on it by Ali Enayat about Harvey Friedman's paper. It should be easy for someone to have a good general picture of the consistency strength between formal theories combining these two. If you wish to add more theories from other fields such as HoTT or Category Theory you are welcome to do so as a comment in that answer.

• The vast majority of systems encountered in the wild can be outright proved consistent, which makes the question moot. Does this mean you are only interested in strong theories like ZFC and its extensions, or do you have in mind provability of the implication in some weak metatheory? Jan 21, 2015 at 21:17
• Well, I know there are some random systems out there that very few people study. ZFC and its extensions are welcomed but not just them. For example NBG and MK Set Theories can be included and as examples of somewhat weak theories that should be included might be Second Order Arithmetic and Robinson Arithmetic. Jan 21, 2015 at 21:25
• Once again: in normal mathematics, the axiomatic second order arithmetic is provably consistent, and of course Robinson arithmetic is, hence it doesn’t make much sense to consider relative consistency of these theories, unless you severely restrict the metatheory. So, what is your metatheory? Jan 21, 2015 at 21:32
• For subsystems of second order arithmetic, there is the Reverse Mathematics Zoo. rmzoo.math.uconn.edu Jan 22, 2015 at 2:00
• @Joel: Sure. But on the level of generality of the question, a formal system may be anything from large cardinal hypotheses down to propositional logic, so I wanted to know what is the OP's perspective. Jan 22, 2015 at 11:51

Cantor's Attic, which I founded with Victoria Gitman, is a compendium of information on the consistency strength hierarchy in set theory, spanning the range from ZFC (which in this context is viewed as a weak theory) up through the large cardinal hierarchy to the strongest notions. Any expert set-theorist is encouraged and welcome to make additions to the database (just create an account and then begin editing). We aim at a comprehensive listing of all the main concepts of infinity, organized in large part by their large cardinal consistency strength.

There are numerous parts of the large cardinal consistency-strength hierarchy that are mapped out in fine detail in various sources. See, for example, the chart in Kanamori's book:

Or Victoria Gitman's chart of the large cardinal hierarchy in the vicinity of Ramsey cardinals, on which she wrote her dissertation:

(source: boolesrings.org)

Or Norman Perlmutter's similar chart for a different region of the large cardinal hierarchy on which he had focussed in his dissertation:

(source: boolesrings.org)

So indeed there are many such charts for the relative consistency strength of the various large cardinal hypotheses studied in set theory. Where to look depends a lot on which particular part of the hierarchy you are interested.

If anyone else knows of good charts of regions of the large cardinal hiearchy available online, I'd appreciate it if you could provide a link. Feel free to post as an answer! (Or it to this answer as an image or at least in the comments.)

• Can anyone explain to me how to make the images a little smaller? Jan 22, 2015 at 2:02
• Thank you for the nice references and the reminder of Cantor's Attic. I think I looked at it once when I found your website/blog and possibly I got the idea of this recopilation from it. I met Victoria last week in London and she told me a friend of hers is working in a diagram like the one I ask for (though I think just in relation to Set Theory and not other branches in the Foundations of Mathematics). Do you know if there is a similar project in relation to Arithmetic? Possibly having ZFC in the top of the hierarchy? That way it is just a matter of connecting both compilations. Jan 22, 2015 at 4:38
• Jonathan: for an diagram of the consistenct/interpretability hierarchy that also includes arithmetical theories, see the last page of Harvey Friedman's Interpretations according to Tarski, available at the link u.osu.edu/friedman.8/files/2014/01/Tarski1052407-13do0b2.pdf Jan 22, 2015 at 22:16
• Two of the embedded images return 404's. Aug 29, 2018 at 19:03

Another charp, that I found it interesting:

It can be find here: Large cardinals

This is an old question, but for interested readers, I might add the charts on this webpage, which I find quite good:

https://dansnielsen.wordpress.com/2018/06/28/a-travel-guide-to-the-large-cardinals/