## 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 knownthat $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$?

lessthan Con(T) to T (but no naturality requirement). $\endgroup$ – Joel David Hamkins Jul 16 '10 at 1:44