If {P is provable} is provable, then P is provable?

Question

This is simple question.

   If, sort-of-says, "X is provable" is provable,

         then, we can always predicate that X is provable?

It means,

for the theory T,

  If   T ⊢ (X is provable)   

 then  T ⊢ X  ?

Answer 1

Yes, if you add enough assumptions. First, $T$ needs to axiomatize arithmetic or something of similar power, so that ($X$ is provable) can be encoded in the language of $T$. Then $T$ needs to have a model $M$ (like the integers, if $T$ axiomatizes arithmetic), and the abovementioned encoding of ($X$ is provable) must be such that its interpretation in $M$ really is true if and only if $T\vdash X$.

Unfortunately (?) with all those assumptions, the desired conclusion becomes trivially true. All the hard work lies in proving the assumptions.

More formally, if $T\vdash(X\text{ is provable})$ then by assumption, $M\vDash (X\text{ is provable})$ holds, and then again by assumption $T\vdash X$ holds.