Unprovable statements S where the only way to prove S is to assume S

Question

Motivation: Incompleteness (and various independence statements) is about unprovable statements. One natural way to make an unprovable statement provable is to assume it as a new axiom. But this feels like cheating, so people often look for "natural" axioms to add that will imply their favorite unprovable statement. The question is whether there are any statements that are unprovable in a theory where essentially the only way to get a theory which proves the statement is to assume it.

Question: Let $T$ be a theory (e.g. ZFC). Say a statement $S$ is "minimally unprovable" in/over $T$ if $S$ is not provable from $T$ (and neither is its negation), and such that if $R$ is any statement that is provable from $T \cup \{S\}$ but not provable from $T$ alone, then there is a proof in $T$ that $R$ is equivalent to $S$.

1. Does every (sufficiently powerful?) theory have minimally unprovable statements?

2. Are there examples of a(n interesting) theory $T$ together with a minimally unprovable statement $S$?

Answer 1

The following is essentially Joel's answer and also essentially the last part of Francois's answer, but its "look and feel" seems different enough to make it worth pointing out. The main point is that, if $S$ is minimally unprovable over $T$ then $T\cup\{\neg S\}$ is consistent and complete. Consistency is just your requirement that $S$ is not provable from $T$.

To establish completeness, suppose $Y$ is a sentence that is not provable from $T\cup\{\neg S\}$; I'll show that $\neg Y$ must be provable from $T\cup\{\neg S\}$. The assumption means that $(\neg S)\to Y$ isn't provable from $T$, and therefore neither is its contrapositive $(\neg Y)\to S$. Therefore neither is the (propositionally equivalent) formula $(S\lor\neg Y)\to S$. Now apply the main clause in the definition of minimally unprovable, with $S\lor\neg Y$ in the role of $R$. We've just seen that the conclusion of that clause fails, so one of the hypotheses must fail. The first hypothesis says that $R$ is provable from $T\cup\{S\}$, which is clearly true because of the disjunct $S$ in $R$. So the second hypothesis must fail; that is, $R$ must be provable from $T$. But then, by propositional logic, $\neg Y$ is provable from $T\cup\{\neg S\}$, as claimed.

Now if $T$ is recursively axiomatizable and contains enough arithmetic, then $T\cup\{\neg S\}$ has the same properties and, by Rosser's improvement of Goedel's second incompleteness theorem, it cannot be both consistent and complete. Therefore, $S$ cannot be minimally unprovable over $T$.

Answer 2

Theorem. There are no minimally unprovable statements, over any computably axiomatizable theory $T$ interpreting basic arithmetic.

Proof. Suppose that $S$ is not provable in $T$, that $T+S$ is consistent, that $T$ is computably axiomatizable and that $T$ contains (an interpretation of) PA or some other sufficient arithmetic theory. Let $R$ be the assertion $$\text{if the Rosser sentence of }T+\neg S\text{ holds, then }S.$$ Note that $T+S$ proves $R$ easily. So $T+R$ is consistent. Meanwhile, $T$ does not prove $R$, since if it did, then $T+\neg S$ plus the Rosser sentence of $T+\neg S$ would prove $S$, contradicting Rosser's theorem that this theory is consistent. Finally, $T+R$ does not prove $S$, since it is consistent with $T+\neg S$ that the Rosser sentence of $T+\neg S$ fails, so it is consistent with $T+R$ that $S$ fails. QED

If you weaken the hypotheses, then you can have theories with minimally unprovable statements. For example, let $T$ be the theory of true arithmetic, plus the assertion that a new constant symbol $c$ is either $0$ or $1$. The assertion $c=0$ is not provable in $T$, but it is minimally unprovable, since if $T+R$ does not settle the value of $c$, then it has the same models as $T$.

Answer 3

Here is a classical example of a theory that has minimal unprovable statements. Let $T$ be the theory of (nontrivial) dense linear orders: $$\exists x \exists y (x \lt y), \qquad \forall x (x \not\lt x),$$ $$\forall x \forall y(x \neq y \to x \lt y \lor y \lt x),$$ $$\forall x \forall y \forall z (x \lt y \land y \lt z \to x \lt z),$$ $$\forall x \forall y (x \lt y \to \exists z(x \lt z \land z \lt y)).$$ It is well known that $T$ has four completions obtained by adding any one of the four axioms $\min \land \max$, $\min \land \lnot\max$, $\lnot\min \land \max$, $\lnot \min \land \lnot \max$, where $\min$ is $$\exists x \forall y (x = y \lor x \lt y)$$ and $\max$ is $$\exists x \forall y (x = y \lor y \lt x).$$ These four sentences are maximally unprovable statements over $T$ and therefore their negations are all minimally unprovable. In other words, $\min \lor \max$, $\min \lor \lnot\max$, $\lnot\min \lor \max$, $\lnot \min \lor \lnot \max$ are all minimally unprovable sentences over $T$.

In general, any coatom in the Lindenbaum–Tarski algebra of an incomplete theory will be a minimally unprovable statement for that theory. Many common theories (including PA and ZFC) have atomless Lindenbaum–Tarski algebras.