Foundations of mathematics are inferentially incomplete, that, is, there are true but unprovable propositions (although [Gödel 1934] results do not hold for fo

Foundations of mathematics are inferentially incomplete, that, is, there are true but unprovable propositions (although [Gödel 1934] results do not hold for foundations). See following for a proof: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 However, inferential incompleteness does not cause practical difficulties for proof checking assistants :-)