A modal logic internalizing normal proofs |
| |
Authors: | Sungwoo Park Hyeonseung Im |
| |
Affiliation: | Pohang University of Science and Technology, San 31 Hyojadong Namgu, Pohang Gyungbuk 790-784, Republic of Korea |
| |
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 △ 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 ⊃ and the modality △, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems. |
| |
Keywords: | Normal proof Modal logic Sequent calculus Natural deduction system Reflective system |
本文献已被 ScienceDirect 等数据库收录! |
|