Abstract This paper explores how, given a proof, we can systematically transform it into a proof that contains no irrelevancies and which is as strong as possible. I define a weaker and stronger notion of what counts as a proof with no irrelevancies, calling them perfect proofs and gaunt proofs, respectively. Using classical core logic to study classical validities and core logic to study intuitionistic validities, I show that every core proof or classical core proof can be transformed into a perfect proof. In a sequel paper, I show how proofs in core logic can also be transformed into gaunt proofs and I observe that this property fails for classical core logic.

Abstract This paper is the second part of a series exploring how, given a proof, we can inductively transform it into a proof that contains no irrelevancies and is as strong as possible. In the prequel paper, I defined a weaker and a stronger notion of what counts as a proof with no irrelevancies, calling them perfect proofs and gaunt proofs, respectively. There, I showed how proofs in core logic and classical core logic can be transformed into perfect proofs. In this paper I study gaunt proofs. I show how proofs in core logic can be inductively transformed into gaunt core proofs, but that this property fails for the natural deduction system of classical core logic.