It is a central feature of all the main formal systems that when a statement is provable, then it is provably provable. Indeed, this feature is one of the derivability conditions that is commonly used in the proof of the incompleteness theorem, and it is central to Goedel's proof of the second incompleteness theorem.
But also, I might add, this principle is clearly something that we want to have in our formal systems. If you can prove a statement, it means that you have a finite proof, a sequence of statements each of which is either an axiom or follows from the previous statements by one of the deduction rules, and which ends in the statement being proved. To check that a proof really is a proof is meant to be a routine task. Thus, whenever a statement is provable, then we should expect that we can prove that it is provable, since this amounts just to proving that the proof really is a proof, which is something about which there will be little disagreement.
So yes, indeed, in any of the usual formal systems, whenever a statement is provable, then we can also prove that it is provable.
One may introduce the provability modality, writing Box φ to mean that φ is provable (in some fixed formal system under discussion). In this modal terminology, the principle that every provable statement is provably provable is the axiom:
- Box□ φ → Box Box□ □ φ
and this axiom is known as axiom 4 in the modal theory S4.
