2
$\begingroup$

Is the shortest formula which is provably equivalent to the Gödel sentence also the shortest undecidable formula?

I know that even if one accepts the Gödel sentence as an axiom, then yet another undecidable formula can be constructed, but it will be longer, not shorter: if we append to PA its Gödel sentence G then we can get a Gödel sentence G' for PA+G. G' is also undecidable in PA itself, and not equivalent to G (i.e. G = G' is not a theorem of PA), but G' is longer than G, and presumably the shortest formulas in each of their respective equivalence classes have the same relationship.

In other words, is any formula decidable if it is shorter than the shortest G-equivalent?

  • 1
    This question is not well-defined; every theory satisfying the conditions of Gödel's theorem has a Gödel sentence; you should say which theory you're talking about. Also, Gödel uses very elaborate scheme of encoding formulas using numbers and then decoding them, and it all goes into the Gödel sentence; there probably is some possible shortcut (so maybe you should also say which technical proof you're referring to).2011-03-20
  • 1
    @Dan Brumleve (first comment): If you change the formal system, the original G is no longer its Gödel sentence. It could be provably equivalent to the new Gödel sentence, but I'm not sure that is always the case. I would guess the answer is "no" for most systems because there is no reason to believe all undecidable sentences are equivalent, so there is a high chance that the shortest undecidable sentence will lie in some other equivalence class.2011-03-20
  • 0
    Sebastian, you are right, the example is my comment is nonsense because we need to fix the axioms before G can be constructed. However, I don't understand your probabilistic argument; there are many undecidable sentences, but in a vague sense G is the simplest one we can construct, so perhaps it _is_ the shortest. Lacking a proof either way, I may accept such a probabilistic argument as an answer. I am still tempted to think that the theory and encoding do not affect the answer, although I would be satisfied with an answer that only addresses some particular formal system such as PA.2011-03-20
  • 0
    It occurs to me that we can write a busy-beaver-type program which halts if and only if the answer is "yes". At the same time it actually finds the shortest undecidable formula and decides all shorter ones. But if the answer is "no", then it runs forever and gives no insight. I don't see a paradox here but it makes a "yes" answer seem improbable.2011-03-20
  • 0
    The Gödel sentence is actually very very complicated. Under an appropriate metric, Con(T) might be simpler, but not by much. Also, I'm not sure how you want your program to work. Since you cannot check algorithmically whether a given sentence is decidable, you can't find the shortest undecidable sentence either. (continued)2011-03-21
  • 0
    Conclusion: The only way to answer this question (for a specific system and metric!) seems to be to actually determine the shortest undecidable sentence. That is, you need to guess what it is, and then show that all shorter ones are decidable. Or, if you are really lucky, there is a way to construct a shorter undecidable sentence from every sentence equivalent to G, but I doubt it.2011-03-21
  • 0
    I am believing the answer must be "no" but I'm still not sure how to prove it. For example, AC is undecidable in ZF and very short (kilobits) whereas G(ZF) is huge (many gigabits). How to prove that there does not exist a formula X < AC such that "X = G(ZF)" is a theorem? For that matter, how to prove even that "AC = G(ZF)" is not a theorem? Seems like it should be easy but I'm not getting it yet.2011-03-22
  • 0
    In my last comment, I was trying to say that I don't think there is an easy way to answer this question, nor a general method. However, if ZF is consistent, then the axiom of choice is not equivalent to its Gödel sentence, because AC does not have any arithmetical consequences.2011-03-22
  • 0
    Voting to close; I think I can ask a more interesting soft-question about the relationship between string length and decidability.2011-03-25

2 Answers 2

6

Almost certainly not.

Gödel was the first to show how one could explicitly construct an undecidable proposition. If you notice the title of the paper where he presented the approach, the paper is labeled as part I. Gödel expected he would need to carry out all the details of his approach before people would be convinced of his surprising result, but in fact people quickly understood it and he never needed to write the followup paper. His paper explicitly describes the proposition as easy to construct in principle but "cumbersome" (English translation), and he was not trying to achieve the simplest undecidable proposition, but rather just the easiest one to prove. Since he didn't complete all the (very boring) details (including boring choices that must be made along the way), we should remember that "Gödel's undecidable proposition" is not only incredibly large, but it is not even a unique well-defined object.

Chaitin, on the other hand, has shown that in some sense most propositions are undecidable. In the words of the abstract of his 1982 paper Gödel's theorem and information, he says that "if a theorem contains more information than a given set of axioms, then it is impossible for the theorem to be derived from the axioms," and in the introduction he phrases it more memorably as "if one has ten pounds of axioms and a twenty-pound theorem, then that theorem cannot be derived from those axioms." To understand this, it is important to remember that, given a reasonable syntax, most propositions of a certain size contain information roughly proportional to their length. (See Chaitin's previous works for formalized versions of these claims.) Therefore once your propositions get longer than your axioms (normalized for the proportion of length that is due simply to syntax requirements), most propositions are undecidable (and they are not equivalent to each other, either).

Looking at Gödel's undecidable proposition (or rather the set of propositions that one could consider to fit this appellation) in the light of Chaitin's results, we see that it is extremely unlikely that anything in this set is the shortest or even equivalent to the shortest undecidable formula.

1

Assuming that PA is consistent:

Extend the language of arithmetic with a new constant symbol $c$, and let $\mathsf{PAc}$ be the theory consisting of all the axioms of PA, and nothing else, but interpreted in the extended language.

We can now "crank the Gödel handle" and produce a Gödel sentence $G$ for $\mathsf{PAc}$, which is certainly undecidable.

Yet another undecidable sentence is $$ c=0 $$ (This is undecidable, because if we had a proof of it, we could replace $c$ with $S(0)$ everywhere in the proof and get a proof of $S(0)=0$ in good old PA, which does not exist because we assume that PA is consistent. On the other hand, if we had a proof of $c\ne 0$, replacing $c$ with $0$ everywhere in that proof would produce a proof of $0\ne 0$, which likewise doesn't exist).

$c=0$ is not provably equivalent to $G$ either, because if we add $G$ as an axiom, $c=0$ is still unprovable, by exactly the same reasoning as before.

$c=0$ is certainly a shortest undecidable sentence of $\mathsf{PAc}$, for the boring reason that it has the smallest possible length of any wff. So $\mathbf{PAc}$ certainly doesn't have the property that its shortest undecidable sentence is equivalent to a Gödel sentence, and there is no particular reason to believe that $\mathsf{PA}$ would have this property either.