# When is a statement provable?

We all know that Gödel showed that there, in a formal system, are true statements that are non-provable (undecidable). In ZFC, there's Kaplansky's Conjecture, the Whitehead problem, etc.

We can also agree that we're sure to find more non-provable statements in ZFC. What I'm curious about is the following:

What is the defining characteristic of a non-provable statement in ZFC? Are they all "strong" in some sense? Is it a necessary condition that they are strong, then? What future theorems might turn out to be non-provable? Is it, through the characteristics of the theorems known to be non-provable possible to make a fairly accurate guess if a theorem will turn out to be non-provable in ZFC?

-

Not all statements that are not provable in ZFC are "strong", if by strong you mean that ZFC + the statement in question is stronger than ZFC in the sense that it implies the consistency of ZFC.
The typical example is the Continuum Hypothesis (CH). ZFC + CH is consistent iff ZFC is, and in this sense, CH is not strong since ZFC + CH itself does not imply the consistency of ZFC.

However, if one wants to prove that the existence of a measurable cardinal is not provable in ZFC, the argument is that ZFC + there is a measurable cardinal implies the consistency of ZFC and hence, by the second incompleteness thm, the existence of a measurable cardinal cannot be proved in ZFC.

Note that the situation in set theory is different from number theory. In order to show that something is not provable in Peano Arithmetic (something which is consistent with PA), one usually uses the Incompleteness Theorems, i.e., one shows that the statement implies the consistency of PA. So in some sense, number theoretic statements known to be independent over PA are strong (over PA), statements known to be independent over ZFC are not necessarily strong over ZFC.

-
What about (in PA) the existence of an infinite element c, such that c>0, c>1, c>2, etc>? Does this prove Con(PA)? – Ross Millikan Dec 30 '10 at 22:10
No. Since Con(PA) is not provable from PA (assuming PA is consistent), we have an $M \vDash PA + \lnot CON(PA)$. The extension of $Th(M)$ (theory of $M$) by the set of axioms {$c > n| n \in \mathbb{N}$} is finitely satisfiable so it's satisfiable by the compactness theorem. Thus we have a model of $Th(M) +$ {$c > n| n \in \mathbb{N}$}, which will be a model of $PA + \lnot CON(PA) +${$c > n| n \in \mathbb{N}$}. Therefore, by soundness, $PA +$ {$c > n| n \in \mathbb{N}$} cannot prove $CON(PA)$. In fact, any model $M$ of $\lnot CON(PA)$ already has such a $c$. – Jason Dec 31 '10 at 0:28
@Jason: I thought so, and that this was an example of something independent under PA that didn't prove Con(PA). Thanks. – Ross Millikan Dec 31 '10 at 3:48
Sentences $\phi$ that are independent of an axiom system $A$, such that neither $\phi$ nor $\neg \phi$ increases the consistency strength of $A$, are called "Orey sentences", and they can be constructed for arithmetical theories like PA as well as set theory. So number theory and set theory seem comparable in this regard. – Shivaram Lingamneni Oct 14 '14 at 4:33
@Ross Millikan: The existence of an infinite element cannot be expressed by a single sentence! However, if you introduce a new constant symbol, then there is a consistent extension of PA that says that there is an infinite element. So this is not quite the same as an independent sentence. – Stefan Geschke Oct 14 '14 at 16:47

Often, you can classify characteristics of a collection of independence results through the use of forcing axioms. For example, if you assume Martin's axiom MA$(\aleph_1)$, which states that for every $\aleph_1$ many dense subsets of a partial order having the countable chain condition, there is a filter meeting all of them, then you can derive a number of statements that are not true in the constructible universe. For example, MA$(\aleph_1)$ implies $2^{\aleph_0} = 2^{\aleph_1}$, the nonexistence of Suslin lines, and the existence of a Whitehead group that isn't free.

It is a current focus of research in set theory to study more powerful forcing axioms that rely on the relative consistency of certain large cardinals with ZFC. For example, the proper forcing axiom, which strengthens MA$(\aleph_1)$ by only requiring the partial order to be proper, has its relative consistency following from the existence of a supercompact cardinal while implying the relative consistency of a Woodin cardinal. These types of forcing axioms give us a flavor of a number of statements that can be true. Consequently, if a statement implied by such an axiom contradicts what is true in some canonical inner model, then we can believe in the statement's independence with ZFC provided we believe in the relative consistency of a large cardinal that implied the possibility of the forcing axiom.

-