Let $\phi$ be a ZFC formula and $\lceil \phi \rceil$ its syntactic representation.
Suppose that
- ZFC proves that "if $\phi$ then there exists a string $x$ that represents a ZFC proof of $\lceil \neg \phi \rceil$ in some suitable proof system" ($x \equiv \lceil ZFC \vdash ^* \neg \phi \rceil$)
Can we conclude (by contradiction) that:
- ZFC proves $\neg \phi$