Chaitin made the very good point that inferential undecidability (incompleteness) is too important a result to depend on the triviality of the existence of the proposition I'mUnprovable. Fortunately, inferential undecidability of strongly-typed theories can be proved without using the nonexistent I'mUnprovable.
