Subject: Intuitionistic and intermediate logics in CoS
Newsgroups: gmane.science.mathematics.frogs
Date: 2006-05-19 00:03:43 GMT (1 year, 51 weeks, 1 day, 16 hours and 55 minutes ago)
Hi, I am currently working on formalizing intuitionistic and intermediate logics (Dummett's LC and first-order Goedel logic) in CoS. I have a draft paper written; if any of you happen to be working on the same thing, or are interested, please let me know and I can send the paper to you. You can find the abstract below. Best, -Alwen -- A local system for intuitionistic logic Abstract: This paper presents systems for first-order intuitionistic logic and several of its extensions in which all the propositional 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, Goedel 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 Goedel logic, in the cut free systems in the calculus of structures.