Suppose I am working in a standard formal theory such as ZFC or NBG.
Consider this statement:
"For all well-formed formulas s, ((there exists a proof p s.t. p is a valid proof of s) --> s)"
I'm fairly familiar with some of the basic facts of logic, e.g., Tarski's undefinability theorem, Godel's theorems, and the difference between "consistency" and "soundness."
Nonetheless, I have two questions:
1) Is this a theorem of ZFC/NBG? (What would a proof look like?)
2) Is there a term for this property of formal theories? E.g., "soundness," "consistency," and "completeness" are terms for other different properties.
Löb's theorem says that (in any sufficiently strong system) for any sentence $\phi$, if $\mathsf{Provable}(\phi) \to \phi\;$ is provable then $\phi$ is provable (so that the hypothesis in $\mathsf{Provable}(\phi) \to \phi\;$ was vacuous). A sound system that proves $\mathsf{Provable}(\phi) \to \phi\;$ for any $\phi$ that is not true is inconsistent.