TY - GEN

T1 - A local system for intuitionistic logic

AU - Tiu, Alwen

PY - 2006

Y1 - 2006

N2 - This paper presents systems for first-order intuitionistic logic and several of its extensions in which all the prepositional rules are local, in the sense that, in applying the rules of the system, one needs only a fixed amount of information about the logical expressions involved. The main source of non-locality is the contraction rules. We show that the contraction rules can be restricted to the atomic ones, provided we employ deep-inference, i.e., to allow rules to apply anywhere inside logical expressions. We further show that the use of deep inference allows for modular extensions of intuitionistic logic to Dummett's intermediate logic LC, Gödel logic and classical logic. We present the systems in the calculus of structures, a proof theoretic formalism which supports deep-inference. Cut elimination for these systems are proved indirectly by simulating the cut-free sequent systems, or the hypersequent systems in the cases of Dummett's LC and Gödel logic, in the cut free systems in the calculus of structures.

AB - This paper presents systems for first-order intuitionistic logic and several of its extensions in which all the prepositional rules are local, in the sense that, in applying the rules of the system, one needs only a fixed amount of information about the logical expressions involved. The main source of non-locality is the contraction rules. We show that the contraction rules can be restricted to the atomic ones, provided we employ deep-inference, i.e., to allow rules to apply anywhere inside logical expressions. We further show that the use of deep inference allows for modular extensions of intuitionistic logic to Dummett's intermediate logic LC, Gödel logic and classical logic. We present the systems in the calculus of structures, a proof theoretic formalism which supports deep-inference. Cut elimination for these systems are proved indirectly by simulating the cut-free sequent systems, or the hypersequent systems in the cases of Dummett's LC and Gödel logic, in the cut free systems in the calculus of structures.

KW - Calculus of structures

KW - Deep inference

KW - Intermediate logics

KW - Intuitionistic logic

KW - Locality

KW - Proof theory

UR - http://www.scopus.com/inward/record.url?scp=33845212916&partnerID=8YFLogxK

U2 - 10.1007/11916277_17

DO - 10.1007/11916277_17

M3 - Conference contribution

SN - 3540482814

SN - 9783540482819

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 242

EP - 256

BT - Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings

PB - Springer Verlag

T2 - 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006

Y2 - 13 November 2006 through 17 November 2006

ER -