 Of course PA + axioms 1–6 is restrictive insofar as it does not contain the induction axioms in the language with the truth predicate.  There are various labels for the system that is obtained by adding all induction axioms involving the truth predicate to the system PA + axioms 1–6: T(PA), CT, PA(S) or PA + ‘there is a full inductive satisfaction class’. This theory is no longer conservative over its base theory PA. For instance one can formalise the soundness theorem or global reflection principle for PA, that is, the claim that all sentences provable in PA are true. The global reflection principle for PA in turn implies the consistency of PA, which is not provable in pure PA by Gödel’s  Second Incompleteness Theorem.  Thus T(PA) is not conservative over PA. T(PA) is much stronger than the mere consistency statement for PA: T(PA) is equivalent to the second-order system ACA of arithmetical comprehension (see Takeuti 1987 and Feferman 1991). More precisely, T(PA) and ACA are intertranslatable in a way that preserves all arithmetical sentences. ACA is given by the axioms of PA with full induction in the second-order language and the following comprehension principle: