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

   However, the [Gödel 1931] proof is incorrect for reasons
   mentioned elsewhere in this discussion.