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);
...
Thus

```
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