The reflection principles express—at least partially—the soundness of the system. The most natural and full expression of the soundness of a system involves the truth predicate and is known as the Global Reflection Principle (see Kreisel and Lévy 1968). The Global Reflection Principle for a formal system S states that all sentences provable in S are true: