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