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?