In his seminal “Outline of a Theory of Truth” Kripke (1975) proposed understanding modal predicates as complex expressions defined by a suitable modal operator and a truth predicate. In the case of the alethic modality of logical or metaphysical necessity, this proposal amounts to understanding the modal predicate ‘is necessary’ as the complex predicate ‘is necessarily true’. In this piece we work out the details of Kripke’s proposal, which we label the Kripke reduction, from a proof-theoretic perspective. To this end we construct a theory for the modal predicate and a theory of truth formulated in a language with a modal operator and show that the modal predicate theory is interpretable in the theory of truth where the interpretation translates the modal predicate ‘N’ by the complex predicate ‘$\Box$T’, the truth predicate modified by the modal operator. In addition, we show that our work can be viewed as the proof-theoretic counterpart to the semantic Kripke reduction recently carried out by Halbach and Welch (2009), which is based on Kripke’s theory of truth.