Being a new member, I am not yet sure whether my question will be taken as a research level question (and thus, appropriate for MO). However, I have seen similar questions on MO, couple of which led me asking mine, and I seem to not be able to find many resources except discussion on FOM and MO. So, any references to resolve the question and fix my possible confusion would be appreciated.
As the title suggests, I want to understand the relation between $ZFC \vdash \varphi$ and $ZFC \vdash\ 'ZFC \vdash \varphi'$. Let me give my motivation (and some partial answers) asking this question so that what I'm trying to arrive at is understood.
We know that if $ZFC \vdash \varphi$, then $ZFC \vdash\ 'ZFC \vdash \varphi'$ for we could write down the Gödel number of the proof we have for $\varphi$ and then check that the formalized $\vdash$ relation holds. I believe even more can be checked to be true for this provability predicate (Hilbert-Bernays provability conditions).
Is the converse true in general? Not necessarily. (Just to make sure that it will be pointed out sooner if I am doing any mistakes, I will try to write down everything unnecessarily detailed using less English and more symbols!)
Let us assume only that $ZFC$ is consistent (However, I am not assuming the formal statement $Con(ZFC)$, that is $\ 'ZFC \nvdash \lceil 0=1 \rceil'$). Then, it is conceivable that $ZFC \vdash\ \ 'ZFC \vdash \lceil 0=1 \rceil'$ but $ZFC \nvdash 0=1$. It might be that in reality ZFC is consistent but $\omega$-inconsistent.
Indeed, if I am not missing a point, it is consistent to have this situation:
$ZFC \vdash Con(ZFC) \rightarrow Con(ZFC+\neg Con(ZFC))$ (Gödel)
$ZFC \vdash Con(ZFC) \rightarrow\ \exists M\ M \models ZFC+\neg Con(ZFC)$ (Gödel)
$ZFC \vdash Con(ZFC) \rightarrow\ \exists M\ M \models\ ZFC+\ 'ZFC \vdash \lceil 0=1 \rceil'$
$ZFC \vdash Con(ZFC) \rightarrow\ \exists M\ M \models\ ZFC+\ 'ZFC \vdash\ 'ZFC \vdash \lceil 0=1 \rceil\ '\ '$ (Soundness and the second provability condition here)
$ZFC \vdash Con(ZFC) \rightarrow Con(ZFC+\ 'ZFC \vdash \neg Con(ZFC)\ ')$
So we cannot hope to have $ZFC \vdash\ 'ZFC \vdash \varphi'$ implying $ZFC \vdash \varphi$ for an arbitrary formula without requiring an additional assumption. At least, we know this for $\varphi: 0=1$ (this is not because of the consistency argument above, but because consistency and $\omega$-inconsistency of ZFC is a possibility).
If you believe that ZFC's characterization of natural numbers coincides with what we have in mind and agree that ZFC should not be $\omega$-inconsistent, then you might want to throw in the assumption $Con(ZFC)$.
Now imagine a universe where $Con(ZFC)$ holds but all the models of ZFC is $\omega$-nonstandard and believe $\neg Con(ZFC)$. I do not know whether this scenario is even possible (which is another question I am wondering) but if it is possible, then it would be the case that $'ZFC \vdash \neg Con(ZFC)\ '$, by completeness since $\neg Con(ZFC)$ is true in all models. Then if the implication in title (or should I say, an informal version of it: $V \models ZFC \vdash \varphi$ implies $V \models \varphi$) held, then $\neg Con(ZFC)$ which contradicts our assumption that there are models at all. The point is arbitrary models of ZFC may not be sufficient to have existence of ZFC-proofs implying existence of actual proofs.
However, if we add a stronger assumption $\psi$ that there is an $\omega$-model, then whenever we have an arithmetic sentence $\varphi$, if
$ZFC \vdash\ 'ZFC \vdash \lceil \varphi \rceil'$
then
$ZFC+\psi \vdash \exists M\ \omega^M=\omega \wedge M \models ZFC+\ \varphi$
and because $\omega$ in the model is the real one, by taking care of quantifiers one by one we can deduce $ZFC+\psi \vdash \varphi$. Thus, existence of an $\omega$-model solves our problem for arithmetical sentences. I cannot see any reason to make this work for arbitrary sentences without strengthening the assumption. Here is a thought:
We know, by the reflection principle, that we can find some limit ordinal $\alpha$ such that $\varphi \leftrightarrow \varphi^{V_{\alpha}} \leftrightarrow V_{\alpha} \models \varphi$. Thus, if we could make sure somehow that $V_{\alpha}$ is a model of ZFC while we reflect $\varphi$, then we would be done. But I could not modify the proofs of reflection in such a way that this can be done and am not even sure that this could be done.
My question to MO is to what extent (and under which assumptions) can we get the implication in the title?
Edit: After reading Emil Jerabek's answer, I realized I should clarify some details.
Firstly, I want to treat ZFC only as a formal system (meaning that if you are claiming some assumption $\psi$ does what I want, I want to have a description of how that proof would formally look. This is why I kept writing all the leftmost $ZFC \vdash$'s all the time). Then, it is clear by the above discussions that even if we could prove $ZFC \vdash \varphi$ within our system, we may not prove $\varphi$ without additional assumptions on our system.
One solution could be that our system satisfies the "magical" property that whenever we have $ZFC \vdash \exists x \in \omega\ \varphi(x)$, say for some arithmetic sentence, then we have $ZFC \vdash \varphi(SSS…0)$ for some numeral. This of course is not available by default setting for we know that the theory $ZFC$+ $c \in \omega$ + $c \neq 0$ + $c \neq S0$ +… is consistent if $ZFC$ is consistent. Thus, that magical property seems like an unreasonably strong assumption.
To make my question very precise, what I want is some assumption $\psi$ so that for some class of formulas, whenever I have $ZFC \vdash ZFC \vdash \varphi$, then $ZFC + \psi \vdash \varphi$. For arithmetic sentences, existence of an $\omega$-model is sufficient.
I agree that $\Sigma^0_1$ soundness should be sufficient for arithmetic sentences if what you mean by $\Sigma^0_1$ soundness is having $ZFC \vdash ZFC \vdash \varphi$ requiring (maybe even as a derivation rule, attached to our system!) $ZFC \vdash \omega \models \phi$, where $\phi$ is the translated version of $\varphi$ into the appropriate language, since I can again go through quantifier by quantifier and prove the sentence itself, that is $ZFC \vdash \varphi$.
However, I see no reason why $\Sigma^0_1$ soundness should be enough for arbitrary sentence $\varphi$. It seems to me that what we need is some structure for which we have the reflection property that formal truth in the structure is provably equivalent to $\varphi$ and that structure being model of all the ZFC-sentences used in the ZFC-proof of $\varphi$.
I believe existence of $\Sigma_n$-reflecting cardinals which are inaccesible is more than sufficient for sentences up to $n$ in the Levy hiearchy. By definition of those, we have the equivalence $\varphi \leftrightarrow V_{\kappa} \models \varphi$ and then provability of $\varphi$ in ZFC implies $V_{\kappa} \models \varphi$. However, I am not sure if we had to go that far. ${}{}$
Best Answer
$\def\zfc{\mathrm{ZFC}}\def\pr{\operatorname{Prov}\nolimits}$The statement
is equivalent to the statement that $\zfc$ is either inconsistent or $\Sigma^0_1$-sound: the latter means that every $\Sigma^0_1$-sentence provable in $\zfc$ is true in standard integers. One direction is obvious as $\pr_\zfc(\ulcorner\varphi\urcorner)$ is a $\Sigma^0_1$-sentence, and its truth in $\mathbb N$ says exactly that $\varphi$ is provable in $\zfc$. The converse follows from the Friedman–Goldfarb–Harrington principle: if $T$ is a recursively axiomatized theory containing Robinson’s arithmetic and $\sigma$ a $\Sigma^0_1$-sentence, there exists a sentence $\varphi$ (that can also be taken $\Sigma^0_1$) such that
$$I\Delta_0+\mathit{EXP}\vdash\pr_T(\ulcorner\varphi\urcorner)\leftrightarrow(\sigma\lor\pr_T(\ulcorner0=1\urcorner)).$$
$\Sigma^0_1$-soundness is stronger than consistency, but weaker than $\omega$-consistency. If you are wondering about foundational issues, it is best to consider it as a separate assumption on its own.