Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
    
Perhaps something similar to $PA+\lbrace Con^n(PA)|n \gt 0\rbrace$ as the theory, and $\bigwedge_n Con^n(PA)$ as a minimally unprovable statement? –  David Roberts Nov 8 '12 at 0:02
2  
I'm puzzled by the connection between the question and the motivation. What would you call a statement $X$ with neither $X$ nor its negation provable from $T$ so that for any statement $Y$ if $T+Y$ proves $X$, then $T+X$ proves $Y$? Is this farther from your motivation than your notion of "minimally unprovable?" Your notion is that of a statement so weak it can only prove things equivalent to itself. I think the alternative notion is of a statement that is so weak that nothing strictly weaker can prove it. –  Matt Brin Nov 8 '12 at 1:00
1  
Well, it pays to listen to the logician/set theorist, rather than me :-) I did think it unlikely, but that is easy to say after the fact. –  David Roberts Nov 8 '12 at 1:20
    
This is related in some way - mathoverflow.net/questions/26411/… –  François G. Dorais Nov 8 '12 at 2:17
    
See also the answer to this queston mathoverflow.net/questions/84074/…, which shares some features with the queston and answer here. –  Joel David Hamkins Nov 8 '12 at 2:38
show 1 more comment

3 Answers

up vote 22 down vote accepted

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

share|improve this answer
1  
Thank you for this very clear answer... –  Joël Nov 13 '12 at 18:46
add comment

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.

share|improve this answer
    
I forgot to exclude the trivial linear order with just one point by adding a non-triviality clause to $T$... –  François G. Dorais Nov 8 '12 at 3:13
1  
François: Thanks! Not being a logician, I didn't know about the Lindenbaum-Tarski algebra. But if I've understood correctly, atoms in the Lindenbaum-Tarski algebra of $T$ (if any exist) are exactly the minimally unprovable statements over $T$. –  Joshua Grochow Nov 8 '12 at 15:53
    
Josh and François, isn't it instead the co-atoms in the Lindenbaum algebra that are the minimally unprovable statements? After all, being lower in the Lindenbaum algebra means being a stronger assertion (as falsity is at the bottom). The assertions min$\wedge$max and so on in François's answer are actually atoms, and their negations are co-atoms. Right? –  Joel David Hamkins Nov 11 '12 at 16:27
    
(And one should also say that when the theory is complete, it has no independent assertions, but the Lindenbaum algebra still has an atom.) –  Joel David Hamkins Nov 11 '12 at 16:28
    
Absolutely, Joel! Fixing now... –  François G. Dorais Nov 13 '12 at 17:47
show 2 more comments

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

share|improve this answer
    
$T$ needs to be recursively axiomatizable? –  François G. Dorais Nov 8 '12 at 2:17
    
Yes, you are right! I'll edit. –  Joel David Hamkins Nov 8 '12 at 2:26
    
I edited to fix. Also, if you drop the c.e. requirement, then there can be minimally nonprovable assertions. –  Joel David Hamkins Nov 8 '12 at 2:36
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.