TR-2004001: Tableaux for the Logic of Proofs
Bryan Renne · CUNY Academic Works (City University of New York) · 2004
The Logic of Proofs, LP, is an explicit provability logic due to Artemov.The introduction of LP answered a long-standing question concerning the intended semantics of Gödel's provability calculus and provability semantics for intuitionistic logic.The explicit nature of LP and its ability to naturally represent both modal logic and typed λcalculi, especially in light of the Curry-Howard Isomorphism, makes its applicability to Computer Science a primary focus of research in this area.In the present paper, I develop a tableau system for LP and give a semantic proof of cut elimination.