**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$?
> 
> 
> 



Unprovable statements S where the only way to prove S is to assume S
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$.


