Motivation
One of the methods for strictly extending a theory $T$ (which is axiomatizable and consistent, and includes enough arithmetic) is adding the sentence expressing the consistency of $T$ ( $Con(T)$ ) to $T$. But this extension ( $T+Con(T)$ ) looks very artificial from the mathematical viewpoint, i.e. does not seem to have any mathematically interesting new consequences, and therefore is probably of no interest to a typical mathematician.
I would like to know if there is a natural theory (like PA, ZFC, … ) which by adding the consistency statement we can prove new mathematically interesting statements.
I don't have a definition for what is a natural theory or a mathematically interesting statement, but a theory artificially build for the sole purpose of this question would not be natural, and a purely metamathematical statement (like consistency of $T$, or a statement depending on the encoding of $T$ or its language, or …) would not count as a mathematically interesting statement.
Questions:
Is there a natural theory $T$ and an mathematically interesting statement $\varphi$, such that it is not known that $T \vdash \varphi$, but $T + Con(T) \vdash \varphi$?
Is there a natural theory $T$ and an interesting mathematical statement $\varphi$, such that $T \nvdash \varphi$ but $T + Con(T) \vdash \varphi$?
Best Answer
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!