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

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.