lo.logic - Are there natural examples of mathematical statements which follow from consistency statements?

Vitali famously constructed a set of reals that is not Lebesgue measurable by using the Axiom of Choice. Most people expect that it is not possible to carry out such a construction without the Axiom of Choice.

Solovay and Shelah, however, proved that this expectation is exactly equiconsistent with the existence of an inaccessible cardinal over ZFC. Thus, the consistency statement Con(ZFC + inaccessible) is exactly equivalent to our inability to carry out a Vitali construction without appealing to AC (beyond Dependent Choice).

Thus, if $T$ is the theory $ZFC+$inaccessible, then T+Con(T) can prove "You will not be able to perform a Vitali construction without AC", but $T$, if consistent, does not prove this.

I find both this theory and the statement to be natural (even though the statement can also be expressed itself as a consistency statement). Most mathematicians simply believe the statement to be true, and are often surprised to learn that it has large cardinal strength.

---

There is another general observation to be made. For any consistent theory $T$ whose axioms can be computably enumerated, and this likely includes most or all of the natural theories you might have in mind, there is a polynomial $p(vec x)$ over the integers such that $T$ does not prove that $p(vec x)=0$ has no solutions in the integers, but $T+Con(T)$ does prove this. So if you regard the question of whether these diophantine equations have solutions as natural, then they would be examples of the kind you seek. And the argument shows that every computable theory has such examples.

The proof of this fact is to use the MRDP solution of Hilbert's 10th problem. Namely, Con(T) is the assertion that there is no proof of a contradiction from $T$, and the MRDP methods show that such computable properties can be coded into diophantine equations. Basically, the polynomial $p(vec x)$ has a solution exactly at a Goedel code of a proof of a contradiction from $T$, so the existence of a solution to $p(vec x)=0$ is equivalent to $Con(T)$. If $T$ is consistent, then it will not prove $Con(T)$, and so will not prove there are no integer solutions, but $T+Con(T)$ does prove that there are no integer solutions.

By the way, it is not true in general that if $T$ is consistent, then so is $T+Con(T)$. Although it might be surprising, some consistent theories actually prove their own inconsistency! For example, if PA is consistent, then so is the theory $T=PA+neg Con(PA)$, but this theory $T$ proves $neg Con(T)$. Thus, there are interesting consistent theories $T$, such as the one I just gave, such that $T+Con(T)$ proves any statement at all!