A proposition that cannot be proved in a theory T that axiomatizes its own provability is the following: Theorems of T can be computationally enumerated

A proposition that cannot be proved in a theory T that axiomatizes its own provability is the following: Theorems of T can be computationally enumerated. [Church 1934] presented the following simple proof that T cannot computationally enumerate its own theorems: In order to obtain a contradiction, hypothesize theorems of a foundational theory T are computationally enumerable. Then procedures that are provably total in T are computationally by a procedure that is provably total in T. Consider the Boolean procedure Diagonal defined on natural number input n to be the result of the complement of the result of the ith provably total procedure on input i. The procedure Diagonal differs from every procedure in the enumeration of provably total procedures in T. However, by construction, diagonal is a provably total procedure in T, which is a contradiction. See the following article for additional information: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021