Niveau: Supérieur
Intuitionistic Control Logic Chuck Liang Hofstra University Hempstead, NY Dale Miller INRIA & LIX/Ecole Polytechnique Palaiseau, France March 2, 2012 Abstract We introduce a propositional logic ICL, which adds to intuitionistic logic elements of classical reason- ing without collapsing it into classical logic. This logic includes a new constant for false, which augments false in intuitionistic logic and in minimal logic. The new constant requires a simple-yet-significant modification of intuitionistic logic both semantically and proof-theoretically. We define a Kripke-style semantics as well as a topological space interpretation in which the new constant is given a precise deno- tation. We define a sequent calculus and prove cut-elimination. We then formulate a natural deduction proof system with a term calculus, one that gives a direct, computational interpretation of contraction. This calculus shows that ICL is fully capable of typing programming language control constructs such as call/cc while maintaining intuitionistic implication as a genuine connective. Contents 1 Introduction 2 2 Syntax 2 3 Kripke Semantics 3 4 Sequent Calculus and Cut-Elimination 6 5 Soundness and Completeness 9 6 Natural Deduction and ??-Calculus 12 7 A Topological Semantics 21 8 Related Work and Conclusion 23 A Strong Normalization for the Implicational Fragment 28 1
- proof-theoretical properties
- logic
- also changed
- intuitionistic logic
- using ?
- all worlds
- without esc
- classical logic
- can all