The theory given by all axioms of PA and Axioms 1–6 but with induction only for \(T\)-free formulae is conservative over PA, that is, it doesn’t prove any new \(T\)-free theorems that not already provable in PA. However, not all models of PA can be expanded to models of PA + axioms 1–6. This follows from a result due to Lachlan (1981). Kotlarski, Krajewski, and Lachlan (1981) proved the conservativeness very similar to PA + axioms 1–6 by model-theoretic means. Although several authors claimed that this result is also finitarily provable, no such proof was available until Enayat &amp; Visser (2015) and Leigh (2015). Moreover, the theory given by PA + axioms 1–6 is relatively interpretable in PA. However, this result is sensitive to the choice of the base theory: it fails for finitely axiomatized theories (Heck 2015, Nicolai 2016). These proof-theoretic results have been used extensively in the discussion of truth-theoretic deflationism (see Cieśliński 2017).