If something is provable in ZFC, can ZFC prove that ZFC proves it?

Question

IF ZFC proves a Well-formed formula, it means,

if $ZFC \vdash \phi$,

then, $ZFC \vdash (ZFC \vdash \phi$) ?

Generally, if an axiom system proves a wff, the axiom system can prove that it proves the fomula?

Answer 1

Yes, but not conversely.

If $T$ is a recursive theory that is strong enough to internalise FOL via the standard methods,¹ then all "real" statements in the language of $T$ get coded via standard codes, and all proofs are of finite length which lets us code real proofs in a way that is compatible with the internalisation of FOL.

You can prove this easily by induction on the complexity of the formula, that a standard formula gets assigned a standard code, and then by the definition of the provability predicate.

If $T$ is not recursive, you will need an oracle for it anyway, but the above arguments apply.

Note that in the other direction of the implication, if $T$ is consistent but actually proves $\lnot\operatorname{Con}(T)$, then $T$ does not prove $0=1$, but it proves that it proves $0=1$ (because the internal proof is not standard anymore).

---

1. Note that in PA this means Gödel codes, but in ZFC we can actually code things via finite strings as objects in $V_\omega$ instead. This makes more intuitive sense, and if you know that $V_\omega$ is "essentially $\omega$", then you can move between Gödel codes and actual finite sequences freely enough.