(Non?)-linearity of the consistency strength ordering in ZF

Marios, this is indeed a fascinating topic.

The consistency strength hierarchy is not linearly ordered. One can produce counterexamples by variants of Gödel sentences or of Rosser sentences. It is actually an interesting exercise to produce explicit examples of a pair of Rosser-like sentences $\phi,\psi$ both independent of ZFC, such that ZFC$+\phi$ and ZFC$+\psi$ are incomparable, by letting $\phi$ refer to the length of proofs of consistency of ZFC$+\psi$, and letting $\psi$ refer to the length of proofs of the consistency of ZFC$+\phi$. Explicit examples can be found, I believe, in Per Lindström's "Aspects of Incompleteness" (Lecture Notes in Logic 10).

Harvey Friedman has worked on this question, and expanded on the idea above. I believe it is his result that one can even embed a universal countable partial order in the consistency strength degrees or in the degrees of interpretability. I'm pretty sure he has commented on this in the FOM list, but I don't seem to be able to find his relevant postings right now. (I once gave a talk on this years ago, but cannot find my slides either. Old age...)

On the other hand, everybody agrees that these examples are not natural (see for example, the beginning of the section "The Gödel hierarchy" in this paper by Simpson, or page 54 of "Fixing Frege" by John P. Burgess). It is a remarkable empirical phenomenon that we indeed have comparability for natural theories. We expect this to always be the case, and a significant amount of work in inner model theory is guided by this belief. But although we have many striking partial results in this direction, it is not quite a theorem, in part because natural is not a formal concept.

The standard way by which we establish comparability of statements is by using forcing and the technique of inner models to measure a given statement against the large cardinal hierarchy, identifying this way the large cardinal companion of the statement. Different statement can then be compared by comparing their companions.

Hugh Woodin, in his book on Pmax suggests a way of formalizing this observation, by explaining how to associate Universally Baire sets to theories, the point being that under appropriate determinacy assumptions, the Wadge degrees of any two such sets are comparable, and the resulting ordering coincides precisely with the interpretability or consistency strength orderings. (The universally Baire sets ultimately trace back to the complexity of certain iteration strategies.) This, of course, requires that we work under additional large cardinal assumptions beyond ZFC, so it only applies to theories of high consistency strength (past $\omega$ Woodin cardinals, for example). This remarkable approach has thus the drawback that it does not explain why we find the phenomenon in the low levels of the hierarchy, the ones that are precisely amenable to current inner model theoretic techniques.

At the moment there are a few notable examples of theories that we do not quite know how to fit into the linear ordering of consistency strength. This is most likely due to our present technical limitations. For example, strongly compact cardinals are expected to either coincide or sit just below supercompact cardinals consistency-wise. However, their behavior is rather atypical and they are not really as well understood as other (strong) large cardinals.

For a nice introduction to these ideas, examples, and a far reaching program that touchesof Woodin's recent work on "ultimate $L$", see these slides of a talk by John Steel at the Workshop on Set Theory and the Philosophy of Mathematics, Oct. 2010.

The order $\le_{cons}$ isn't linear. There are Godel Lob provability logic $GL$. It's a modal logic with one modality. $GL$ is complete with respect to arithmetic semantic. It was shown by Solovay. Formula $\square(\Diamond p \to \Diamond q) \lor \square(\Diamond q \to \Diamond p)$ is not theorem of $GL$. So by completeness theorem (it can be proved for $ZF$) there are propositions $A$ and $B$ such that $ZF \not \vdash (Con({\ulcorner} A{\urcorner}) \to Con({\ulcorner} B{\urcorner}))$ and $ZF\not \vdash (Con({\ulcorner} B{\urcorner}) \to Con({\ulcorner} A{\urcorner}))$ But such $A$ and $B$ provided by Solovay proof are complex. I don't know any "natural" example.

There are some results of Woodin that indicate why large cardinal axioms of a certain kind might indeed be linearly ordered by consistency strength. In Kanamori's chart there are some possibilities for nonlinearity, but I think this is just lack of knowledge.

I am not aware of any result that actually says that two natural statements are incomparable in consistency strength over ZF. Note however that this might be a problem of our current proof technology.

We have good technology to show that the consistency of a statement $\sigma$ implies the consistency of $\tau$ (all over ZF). Namely, start with a model of ZF+$\sigma$ and use forcing and/or inner models to construct a model of ZF+$\tau$. The second incompleteness theorem tells us how we can get a stronger theory from a consistent theory $T$, namely by adding the axiom "$T$ is consistent".

But how could we prove that two given statements are incomparable in consistency strength?