@LeakyNun No, but I don't see a point, for a number of reasons. (1) It seems to be rather messy. The underlying theory of types has been more cleanly represented by other writings. (2) Russell and Whitehead introduce in PM the axiom of reducibility, not because it is meaningful or compelling, but because it allows them to do what they want. This makes totally no sense. The whole idea of the ramification in Russell's theory of types was to ensure that it was well-founded.

@Secret I don't like Please-Solve-Questions... Anyway if you don't know the answer, you should take a look at my post again about the halting problem.

ok sorry, I just thought questons belong to certain rooms thus I route them there

@Secret Uh?! No do not post any questions here unless it is your own or you are asking something about it.

Chat-rooms are not the dumping ground for questions.

sorry...

I will keep that in mind

Except, of course, your own chat-rooms, where you are free to do as you please, as long as you don't harm other people. =)

@user21820 B(n,k,i) means n encodes the result of substituting “k” to the free variable in the i-th formula with one free variable; Bew(n) means that n encodes a sentence for which there exists a number which encodes a proof of such sentence; how should I build the Gödel sentence from these two formulas?