>It is parametric over formal systems described in Principia Mathematics. That's it.

No, it is parametric over formal systems capable of describing Turing machines. Period. Goedel's Incompleteness Theorem can be derived from Chaitin's Incompleteness Theorem, which is stronger and is defined, in the first place, over systems capable of describing Turing machines.

This is a computability problem, not a problem where you've failed to write down the right formal system. Go learn logic.