 Exactly which instances of the reflection scheme are actually provable in the system? Löb’s Theorem gives a precise answer to this question (assuming that \(\Prov_F (x)\) satisfies the derivability conditions):