@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.
@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?