Hi Liron, Your intuition is pretty good. A correct proof of inferential incompleteness of Russell's Principia Mathematica can be constructed using the compu

Hi Liron, Your intuition is pretty good. A correct proof of inferential incompleteness of Russell's Principia Mathematica can be constructed using the computational undecidability of the halting problem. See https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 However, the [Gödel 1931] proof is incorrect for reasons mentioned elsewhere in this discussion.