**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.

T, the consistency ofXimplies the consistency ofY. – Jonathan Julian Jan 21 '15 at 21:41