Expanding the Realm of Systematic Proof Theory

Abstract. This paper is part of a general project of developing a systematic and algebraic proof theory for nonclassical logics. Generalizing our previous work on intuitionistic-substructural axioms and singleconclusion (hyper)sequent calculi, we define a hierarchy on Hilbert axioms in the language of classical linear logic without exponentials. We then give a systematic procedure to transform axioms up to the level P′ 3 of the hierarchy into inference rules in multiple-conclusion (hyper)sequent calculi, which enjoy cut-elimination under a certain condition. This allows a systematic treatment of logics which could not be dealt with in the previous approach. Our method also works as a heuristic principle for finding appropriate rules for axioms located at levels higher than P′ 3. The case study of Abelian and Lukasiewicz logic is outlined.

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Agata Ciabattoni, Lutz Straßburger, Kazushige Terui
• Keywords: Artificial Intelligence, CSL 2009, Hyper)sequent Calculi, Intuitionistic-substructural Axioms, Systematic