どう違うってそのままじゃない？
まあ本人の意図は本人が説明してくれたほうがいいけど

　T |- φ
は理論Tでφが証明可能、っていう2項述語でしょ
　Q |- φ
にあたる可証性述語Prov_Qは集合論の言語で書ける
それで
　¬Prov_Q(∀x(0+x=x))がZFで証明可能
とかそういうことを言いたいんだと思う

上のほうで350が書いてたことを読み返してみないと
訊いてることがいまいちわからないのはそうかもね