I am currently reading Scott Aaronson's "Quantum Computing since Democritus", where I stumbled over a reasoning to (positively) answer the following question: Is there any theorem which can only be proved by assuming that it can be proved? (chapter 3)
The reasoning goes as follows, for concreteness assume the Riemann Hypothesis (RH) is the theorem and Zermelo-Fraenkel set theory (ZF) is the formal system to prove it in:
Assume: We can prove in ZF: if (ZF proves RH), then RH
--> provable in ZF: if not(RH), then ZF does not prove RH
In other words: in {ZF + not(RH)}: ZF is consistent with not(RH)
"But this means that the theory {ZF + not(RH)} proves its own consistency,
and this, by Gödel, means {ZF + not(RH)} is inconsistent.
But saying that {ZF + not(RH)} is inconsistent is equivalent to saying that RH is a theorem of ZF.
Therefore we proved RH"
I fail to understand (at least) one step here:
Why does {ZF + not(RH)} prove it's own consistency?
Would this proof not require that one can also prove the consistency of ZF itself within {ZF + not(RH)}?
Or am i wrong in assuming that for {ZF + not(RH)} to be consistent, ZF needs to be consistent?
That's not what it means! Rather, it means that $\{ZF ; \neg RH)\}$ proves the consistency of $\neg RH$ within ZF.
Write $\operatorname{Bew}$ for provable (Beweisbar) and $\operatorname{Con}$ for consistant. If you want to study statements like $\operatorname{Bew(A)} \to A$ modal logic is what you're after.