## 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:

1. 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$?

2. Is there a natural theory $T$ and an interesting mathematical statement $\varphi$, such that $T \nvdash \varphi$ but $T + Con(T) \vdash \varphi$?

-

I've been told that the consistency of ZFC can be used to give a construction of the Rado graph (the "unique" countably infinite random graph), but there are many other constructions that do not require this. – Charles Staats Jul 16 2010 at 0:20
You may be interesed in this related question: mathoverflow.net/questions/12865/… – Joel David Hamkins Jul 16 2010 at 1:39
This question mathoverflow.net/questions/26411/… is also related, in that it inquires about adding less than Con(T) to T (but no naturality requirement).  – Joel David Hamkins Jul 16 2010 at 1:44

## 3 Answers

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!

-
Joel, I believe the question is about $T+Con(T+\varphi)$ proving a statement $\psi$, not about $Con(T+\varphi)\leftrightarrow Con(T+\psi)$ being provable in $T$ (or in a weaker system). Your example is of the second kind. – Andres Caicedo Jul 16 2010 at 0:34

1
My statement $\psi$ was "our inability to carry out a Vitali construction without using AC." While it is true that this statement can be thought of as a consistency statement, it needn't be. – Joel David Hamkins Jul 16 2010 at 0:45
It is really great answer! – Sergei Tropanets Jul 17 2010 at 1:03
This is a nice result that I was not aware of. However, Kaveh might disqualify it as a "metamathematical" statement. – Timothy Chow Jul 20 2010 at 2:44
Thank you Joel. The first half is really nice, but I have to think about it a little more. The second part refers to the theory since the polynomial from the MRDP theorem will depend on the encoding of the theory. This will make it metamathematical. – Kaveh Jul 21 2010 at 23:46
show 2 more comments

### You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.

The Paris–Harrington Theorem is equivalent (over IΣ1) to Con(PA + Tr(Π1)), where Tr(Π1) is the set of all true Π1 sentences in the language of arithmetic.

For clarity, the 1-consistency of PA, i.e. what is meant by Con(PA + Tr(Π1)), is the following statement:

If φ is a (Gödel code for a) true Π1 sentence, then PA ⊬ ¬φ.

Or the dual reflection principle:

If φ is a (Gödel code for a) Σ1 sentence and PA ⊦ φ, then φ is true.

Note that IΣ1 proves the existence of Σ1 truth predicates, so the above is expressible as a Π2 statement.

-

In fact, most "combinatorial" statements (Hydra games, Kanamori-McAloon, ...) are equivalent to this theory. On the other hand, the theory is not recursive, so I am not sure it qualifies as "natural". (I find it natural, but I also think that a formal definition of naturalness ought to include that it is recursive.) – Andres Caicedo Jul 16 2010 at 0:26
By a natural theory I mean something that ordinary mathematicians use, i.e. prove theorems using it (theorems inside it, not about it), so I think being recursively enumerable is probably a necessary condition. – Kaveh Jul 23 2010 at 0:32
PA is recursively enumerable, it's just that 1-consistency is stronger than just plain consistency. – François G. Dorais♦ Jul 23 2010 at 1:00

The short answer is no. Con(T) is a very weak assumption and it is asking a lot for it to have interesting mathematical consequences. A slightly less ambitious question is whether "ZFC + the consistency of some large cardinal axiom" has any interesting mathematical consequences. Here the work of Harvey Friedman is relevant, as I explained in this answer to a related MO question. I don't think Friedman's examples are quite there yet but they're getting close.

-

2
Note that Friedman uses not simple consistency but the rather stronger notion of Sigma-1 soundness. – Charles Stewart Jul 17 2010 at 12:34
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 43, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 20, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9374820590019226, "perplexity_flag": "middle"}