It is an important challenge.
According to the Theory of Types, every proposition belongs to a certain order. In original Gödel sentence G, the order of G is ambiguous.
The original sentence
~(T -> G)
should be a simultaneous assertion of multiple sentences of this kind:
~(T -> Gn), where n is a natural number,
and Gn stands for "G of the nth order."
Let G stand for the series of "is not provable by T": G1, G2, G3, ..., Gn, ...
Let S stand for the correlation function "is not provable by T"
Then G2 = S(G1);
G3 = S(G2);
G4 = S(G3);
G = G1, G2, G3, G4, ...
S;G= G2, G3, G4, G5, ...
where ; is a PM notation for applying correlation function on a series; G cannot be treated as a class because no two G's are of the same order (there is a lot of room for expansion in the theory of types, as of today and by the theory of types, I can't even utter phrases like "two G's".).
Since there is no G1, S;G and G are the same series. (I realize that G1 is a problem; if logical types can also be extended downwards ad infinitum, then this solution is complete.)
And G should be read as:
This series of statements cannot be proved by theory T.
Notice that the input "this series of statements" and the output of the above sentence are the same. It appears to be self-referential, but it is not individually; it is the same series shifted to the right; in a similar fashion, adding 1 to the series of integers results in the same series.
If the order of G is spelt out, G is a simultaneous assertion of the following sentences:
The first order statement G1 in this series cannot be proved.
- this is the 2nd order statement G2, which is False
because there is no G1. Gn is a statement about a statement,
and a statement about a statement is at least 2nd order.
The 2nd order statement G2 in this series cannot be proved.
- this is the third order statement G3, which is True
because we just showed G2 is false.
The 3rd order statement G3 cannot be proved. - G4
---False, we just showed G3 is true.
So on so forth.
See Liar's paradox in Principa Mathematica
On the other hand, if G is taken literally, it is nonsense according to the theory of types:
No proposition can say anything about itself, because the propositional sign cannot be contained in itself (that is the "whole theory of types").
Wittegenstein, Tractatus 3.332