Equiconsistency

Since some theories are powerful enough to model different mathematical objects, it is natural to wonder about their own consistency.

Gödel's incompleteness theorems show that Hilbert's program cannot be realized: if a consistent computably enumerable theory is strong enough to formalize its own metamathematics (whether something is a proof or not), i.e. strong enough to model a weak fragment of arithmetic (Robinson arithmetic suffices), then the theory cannot prove its own consistency.

For theories at the level of second-order arithmetic, the reverse mathematics program has much to say.

The method of forcing allows one to show that the theories ZFC, ZFC+CH and ZFC+¬CH are all equiconsistent (where CH denotes the continuum hypothesis).

The consistency strength of numerous combinatorial statements can be calibrated by large cardinals.