A Modal Logic Internalizing Normal Proofs

Abstract

In the proof-theoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the system reduces to a corresponding normal proof. This paper develops a system of modal logic that is capable of expressing the notion of normal proof within the system itself, thereby making normal proofs an inherent property of the logic. Using a modality Delta to express the existence of a normal proof, the system provides a means for both recognizing and manipulating its own normal proofs. We develop the system as a sequent calculus with the implication connective superset of and the modality Delta, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems. (C) 2011 Elsevier Inc. All rights reserved.