The article linked below explains why [Gödel 1931] did not prove inferential undecidability of Russell's Principia Mathematica and likewise why the formalization of [Gödel 1931] in Lisp proof being discussed is also invalid:
https://papers.ssrn.com/abstract=3603021
However, the article linked above does have a correct proof of inferential undecidability (also known as "inferential incompleteness").
Would be happy to respond to any questions that you might have.
The word "inferential" has to do with being able to be logically inferred, that is, deduced.
Russell's Principia Mathematica specified that each proposition must have an order to block paradoxes such as Russell's paradox.
See the article linked above for further explanation.
The article linked below explains why [Gödel 1931] did not prove inferential undecidability of Russell's Principia Mathematica and likewise why the formalization of [Gödel 1931] in Lisp proof being discussed is also invalid:
https://papers.ssrn.com/abstract=3603021
However, the article linked above does have a correct proof of inferential undecidability (also known as "inferential incompleteness").
Would be happy to respond to any questions that you might have.