For a theory T in which proof-checking is computationally decidable that formalizes its own provability, the following proposition is true but unprovable:

For a theory T in which proof-checking is computationally decidable that formalizes its own provability, the following proposition is true but unprovable: Theorems of T are computationally enumerable. There is a proof the above proposition is true but unprovable here: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 Note that the above result is more powerful than the one quoted in the post above because theorems of T might not computationally enumerable, which is the case for the Dedekind axiomatization of Natural Numbers.