No CrossRef data available.
Article contents
On the unification of classical, intuitionistic and affine logics
Published online by Cambridge University Press: 12 October 2018
Abstract
This article presents a unified logic that combines classical logic, intuitionistic logic and affine linear logic (restricting contraction but not weakening). We show that this unification can be achieved semantically, syntactically and in the computational interpretation of proofs. It extends our previous work in combining classical and intuitionistic logics. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. We define a phase semantics for this logic that naturally extends the Kripke semantics of intuitionistic logic. We present a sequent calculus with novel structural rules, which entail a more elaborate procedure for cut elimination. Computationally, this system allows affine-linear interpretations of proofs to be combined with classical interpretations, such as the λμ calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.
- Type
- Paper
- Information
- Copyright
- © Cambridge University Press 2018
References
Andreoli, J.-M. (1992). Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2 (3) 297–347.CrossRefGoogle Scholar
de Groote, P. (1994). On the relation between lambda-mu calculus and the syntactic theory of sequential control. In: Proceedings of the 5th International Conference Logic Programming and Automated Reasoning LPAR'94, 31–43.Google Scholar
Felleisen, M., Friedman, D., Kohlbecker, E. and Duba, B. (1987). A syntactic theory of sequential control. Theoretical Computer Science 52 (3) 205–237.CrossRefGoogle Scholar
Gentzen, G. (1935). Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, North-Holland (1969) 68–131.Google Scholar
Girard, J.-Y. (1991). A new constructive logic: Classical logic. Mathematical Structures in Computer Science 1 255–296.CrossRefGoogle Scholar
Girard, J.-Y. (1993). On the unity of logic. Annals of Pure and Applied Logic 59 201–217.CrossRefGoogle Scholar
Girard, J.-Y. (1995). Linear logic: Its syntax and semantics. In Girard, J.-Y., Lafont, Y. and Regnier, L. (eds.) Advances in Linear Logic, London Mathematical Society Lecture Note Series, vol. 222. Cambridge University Press.CrossRefGoogle Scholar
Hodas, J. and Miller, D. (1994). Logic programming in a fragment of intuitionistic linear logic. Information and Computation 110 (2) 327–365.CrossRefGoogle Scholar
Ilik, D. (2012). Delimited control operators prove double-negation shift. Annals of Pure and Applied Logic 163 (11) 1549–1559.CrossRefGoogle Scholar
Ilik, D., Lee, G. and Herbelin, H. (2010). Kripke models for classical logic. Annals of Pure and Applied Logic 161 (11) 1367–1378.CrossRefGoogle Scholar
Jagadeesan, R., Nadathur, G. and Saraswat, V. (2005). Testing concurrent systems: An interpretation of intuitionistic logic. In: Proceedings of the Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 2821, Springer, Hyderabad, India, 517–528.CrossRefGoogle Scholar
Kameyama, Y. and Yonezawa, T. (2008). Typed dynamic control operators for delimited continuations. In: Symposium on Functional and Logic Programming, 239–254.CrossRefGoogle Scholar
Kopylov, A.P. (1995). Propositional linear logic with weakening is decidable. In: Symposium on Logic in Computer Science, IEEE, 496–504.Google Scholar
Lafont, Y. (1997). The finite model property for various fragments of linear logic. Journal of Symbolic Logic 62 1202–1208.CrossRefGoogle Scholar
Liang, C. (2016). Unified semantics and proof system for classical, intuitionistic and affine logics. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5–8, 2016, 156–165. URL http://doi.acm.org/10.1145/2933575.2933581.CrossRefGoogle Scholar
Liang, C. and Miller, D. (2011). A focused approach to combining logics. Annals of Pure and Applied Logic 162 (9) 679–697.CrossRefGoogle Scholar
Liang, C. and Miller, D. (2013a). Kripke semantics and proof systems for combining intuitionistic logic and classical logic. Annals of Pure and Applied Logic 164 (2) 86–111. URL http://hal.inria.fr/hal-00787601.CrossRefGoogle Scholar
Liang, C. and Miller, D. (2013b). Unifying classical and intuitionistic logics for computational control. In: Kupferman, O. (ed.) Proceedings of the 28th Symposium on Logic in Computer Science, 283–292. URL http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics13.pdf.CrossRefGoogle Scholar
Moschovakis, J. (2015). Intuitionistic logic. In: Zalta, E.N. (eds.) The Stanford Encyclopedia of Philosophy, Stanford University, spring edition. URL plato.stanford.edu/archives/spr2015/entries/logic-intuitionistic.Google Scholar
Okada, M. (2002). A uniform semantic proof for cut elimination and completeness of various first and higher order logics. Theoretical Computer Science 281 (1-2) 471–498.CrossRefGoogle Scholar
Luke Ong, C.H. and Stewart, C. (1997). A Curry-Howard foundation for functional computation with control. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, 215–227.Google Scholar
Parigot, M. (1992). λμ-calculus: An algorithmic interpretation of classical natural deduction. In: LPAR: Logic Programming and Automated Reasoning, International Conference, Lecture Notes in Computer Science, vol. 624, Springer, 190–201.CrossRefGoogle Scholar
Troelstra, A.S. and Schwichtenberg, H. (2000) Basic Proof Theory, Cambridge University Press, 2 edition.CrossRefGoogle Scholar
Veldman, W. (1976). An intuitionistic completeness theorem for intuitionistic predicate logic. Journal of Symbolic Logic 41 (1) 159–166.Google Scholar