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

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?

-
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). –  Gadi A Mar 20 '11 at 8:59
@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. –  Sebastian Reichelt Mar 20 '11 at 12:43
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. –  Dan Brumleve Mar 20 '11 at 18:05
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. –  Dan Brumleve Mar 20 '11 at 20:35
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) –  Sebastian Reichelt Mar 21 '11 at 21:14

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.

-