 In order to understand Löb’s theorem properly it is useful to first consider the so-called “reflection principles”. Above, the focus has been on expressing, inside a formal system, that the system is consistent, i.e., on \(\Cons(F)\). But naturally the theory should not merely be consistent but also sound, i.e., prove only true sentences. How should the soundness of a system, i.e., the claim that everything derivable in the system is true, be expressed? If one wants to express this in the language of the system itself, it cannot be done by a single statement saying this, because there is, by the undefinability of truth, no suitable truth predicate available in the language. Various restricted and unrestricted soundness claims can, however, be expressed in the form of a scheme, the so-called Reflection Principles: