# 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