# Theorem proved only when assumed provable, Löbs theorem

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?

• could the downvoter please give a reason? I'd like to improve my question – nnolte Oct 2 '19 at 7:33
• I'm not the downvoter, but you should really use latex via MathJax – Olivier Roche Oct 3 '19 at 6:14

In other words: in $$\{ZF ; \neg RH\}\vdash \ "ZF \textrm{ is consistent with} \neg RH"$$
"But this means that the theory $$\{ZF ; \neg RH\}$$ proves its own consistency
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.