 As the global reflection principle entails formal consistency, the conservativeness result for PA + axioms 1–6 implies that the global reflection principle for Peano arithmetic is not derivable in the typed compositional theory without expanding the induction axioms. In fact, this theory proves neither the statement that all logical validities are true (global reflection for pure first-order logic) nor that all the Peano axioms of arithmetic are true. Perhaps surprisingly, of these two unprovable statements it is the former that is the stronger. The latter can be added as an axiom and the theory remains conservative over PA (Enayat and Visser 2015, Leigh 2015). In contrast, over PA + axioms 1–6, the global reflection principle for first-order logic is equivalent to global reflection for Peano arithmetic (Cieśliński 2010), and these two theories have the same arithmetic consequences as adding the axiom of induction for bounded \((\Delta_0)\) formulas containing the truth predicate (Wcisło and Łełyk 2017). 