Document Open Access Logo

Linear Logic Using Negative Connectives

Author Dale Miller

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.29.pdf
  • Filesize: 0.84 MB
  • 22 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.29.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Linear logic
Keywords
  • Linear logic
  • multifocused proofs
  • sequent calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

In linear logic, the invertibility of a connective’s right-introduction rule is equivalent to the non-invertibility of its left-introduction rule. This duality motivates the concept of polarity: a connective is termed negative if its right-introduction rule is invertible, and positive otherwise. A two-sided sequent calculus for first-order linear logic featuring only negative connectives exhibits a compelling proof theory. Proof search in such a system unfolds through alternating phases of invertible (right-introduction) rules and non-invertible (left-introduction) rules, mirroring the processes of goal-reduction and backchaining, respectively. These phases are formalized here using the framework of multifocused proofs. We analyze linear logic by dissecting it into three sublogics: L₀ (first-order intuitionistic logic with conjunction, implication, and universal quantification); L₁ (an extension of L₀ incorporating linear implication which preserves its intuitionistic nature); and L₂ (which includes multiplicative falsity ⊥ and encompasses classical linear logic). It is worth noting that the single-conclusion restriction on sequents, a constraint imposed by Gentzen, is not a prerequisite for defining intuitionistic logic proofs within this framework, as it emerges naturally by restricting the formulas to those of L₀ and L₁. While multifocused proofs of L₂ sequents can accommodate parallel applications of left-introduction rules, proofs of L₀ and L₁ sequents cannot leverage such parallel rule applications. This notion of parallelism within proofs enables a novel approach to handling disjunctions and existential quantifiers in the natural deduction system for intuitionistic logic.

Cite As Get BibTex

Dale Miller. Linear Logic Using Negative Connectives. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.29

Author Details

Dale Miller
  • Inria Saclay & LIX Institut Polytechnique de Paris, France

Acknowledgements

I thank the reviewers of this paper for their comments and Jui-Hsuan Wu and Beniamino Accattoli for insightful discussions on topics related to this paper.

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. of Logic and Computation, 2(3):297-347, 1992. URL: https://doi.org/10.1093/logcom/2.3.297.
  2. Paola Bruscoli and Alessio Guglielmi. On structuring proof search for first order linear logic. Theoretical Computer Science, 360(1-3):42-76, 2006. URL: https://doi.org/10.1016/j.tcs.2005.11.047.
  3. Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A multi-focused proof system isomorphic to expansion proofs. J. of Logic and Computation, 26(2):577-603, 2016. URL: https://doi.org/10.1093/logcom/exu030.
  4. Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In G. Ausiello, J. Karhumäki, G. Mauri, and L. Ong, editors, Fifth International Conference on Theoretical Computer Science, volume 273 of IFIP, pages 383-396. Springer, September 2008. URL: https://doi.org/10.1007/978-0-387-09680-3_26.
  5. Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. J. of Automated Reasoning, 40(2-3):133-177, 2008. URL: https://doi.org/10.1007/s10817-007-9091-0.
  6. V. Danos, J.-B. Joinet, and H. Schellinx. LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, number 222 in London Mathematical Society Lecture Note Series, pages 211-224. Cambridge University Press, 1995. URL: https://doi.org/10.1017/CBO9780511629150.
  7. R. Dyckhoff and S. Lengrand. LJQ: a strongly focused calculus for intuitionistic logic. In A. Beckmann and et al., editors, Computability in Europe 2006, volume 3988 of LNCS, pages 173-185. Springer, 2006. URL: https://doi.org/10.1007/11780342_19.
  8. José Espírito Santo. Completing Herbelin’s programme. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4583 of LNCS, pages 118-132. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_10.
  9. José Espírito Santo, Ralph Matthes, and Luís Pinto. Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic. In Ugo de’Liguoro, Stefano Berardi, and Thorsten Altenkirch;, editors, 26th International Conference on Types for Proofs and Programs (TYPES 2020), LIPIcs, pages 4:1-4:24, 2020. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.4.
  10. Amy Felty. Encoding the calculus of constructions in a higher-order logic. In M. Vardi, editor, 8th Symp. on Logic in Computer Science, pages 233-244. IEEE, June 1993. URL: https://doi.org/10.1109/LICS.1993.287584.
  11. Gerhard Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68-131. North-Holland, Amsterdam, 1935. Translation of articles that appeared in 1934-35. Collected papers appeared in 1969. URL: https://doi.org/10.1007/BF01201353.
  12. Ulysse Gérard and Dale Miller. Separating functional computation from relations. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of LIPIcs, pages 23:1-23:17, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.23.
  13. Jean-Yves Girard. A new constructive logic: classical logic. Math. Structures in Comp. Science, 1:255-296, 1991. URL: https://doi.org/10.1017/S0960129500001328.
  14. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. Cambridge University Press, 1989. Google Scholar
  15. Hugo Herbelin. A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure. In Computer Science Logic, 8th International Workshop, CSL '94, volume 933 of Lecture Notes in Computer Science, pages 61-75. Springer, 1995. URL: https://doi.org/10.1007/BFb0022247.
  16. Hugo Herbelin and Gyesik Lee. Forcing-based cut-elimination for gentzen-style intuitionistic sequent calculus. In Hiroakira Ono, Makoto Kanazawa, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Proceedings, volume 5514 of LNCS, pages 209-217. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02261-6.
  17. Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327-365, 1994. URL: https://doi.org/10.1006/inco.1994.1036.
  18. Oiva Ketonen. Untersuchungen zum Prädikatenkalkul. Annales Academiae Scientiarum Fennicae, series A, I. Mathematica-physica 23, 1944. Google Scholar
  19. Oiva Ketonen. Investigations into the Predicate Calculus. College Publications, 2022. Ed. by S. Negri and J. von Plato. Google Scholar
  20. Olivier Laurent. A proof of the focalization property of linear logic. Unpublished note, May 2004. Google Scholar
  21. Olivier Laurent. Around classical and intuitionistic linear logics. In LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 629-638, July 2018. URL: https://doi.org/10.1145/3209108.3209132.
  22. Paul Blain Levy. Call-by-push-value: A subsuming paradigm (extended abstract). In J.-Y. Girard, editor, Typed Lambda Calculi and Applications (TLCA 1999), volume 1581 of lncs. Springer, 1999. Google Scholar
  23. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, 2009. Abstract Interpretation and Logic Programming: A Special Issue in Honor of Professor Giorgio Levi. URL: https://doi.org/10.1016/j.tcs.2009.07.041.
  24. Chuck Liang and Dale Miller. Focusing Gentzen’s LK proof system. In Thomas Piecha and Kai Wehmeier, editors, Peter Schroeder-Heister on Proof-Theoretic Semantics, Outstanding Contributions to Logic, pages 275-313. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-50981-0_9.
  25. Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. Monadic concurrent linear logic programming. In Pedro Barahona and Amy P. Felty, editors, Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pages 35-46. ACM, 2005. URL: https://doi.org/10.1145/1069778.
  26. Dale Miller. Forum: A multiple-conclusion specification logic. Theoretical Computer Science, 165(1):201-232, 1996. URL: https://doi.org/10.1016/0304-3975(96)00045-X.
  27. Dale Miller. Linear logic using negative connectives: extended version. Technical report, Inria Saclay, 2025. Extended version of a paper appearring in FSCD 2025. URL: https://hal.science/hal-05067259.
  28. Dale Miller. Proof Theory and Logic Programming: Computation as Proof Search. Cambridge University Press, 2025. To appear. Preprint available at URL: https://www.lix.polytechnique.fr/Labo/Dale.Miller/ptlp/.
  29. Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51(1-2):125-157, 1991. URL: https://doi.org/10.1016/0168-0072(91)90068-W.
  30. Dale Miller and Alexis Saurin. A game semantics for proof search: Preliminary results. In M. Escardó, A. Jung, and M. Mislove, editors, Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), volume 155 of ENTCS, pages 543-563. Elsevier, 2005. URL: https://doi.org/10.1016/j.entcs.2005.11.072.
  31. Dale Miller and Jui-Hsuan Wu. A positive perspective on term representations. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1-3:21, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.3.
  32. Jan Platovon Plato. Proof theory of classical and intuitionistic logic. In Leila Haaparanta, editor, The Development of Modern Logic. Oxford University Press, 2009. Google Scholar
  33. Gordin Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(1):125-159, 1976. Google Scholar
  34. Dag Prawitz. Natural Deduction. Almqvist & Wiksell, Uppsala, 1965. Google Scholar
  35. Harold Schellinx. Some syntactical observations on linear logic. J. of Logic and Computation, 1(4):537-559, September 1991. URL: https://doi.org/10.1093/logcom/1.4.537.
  36. Robert J. Simmons. Structural focalization. ACM Trans. on Computational Logic, 15(3):21, 2014. URL: https://doi.org/10.1145/2629678.
  37. A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 2nd edition, 2000. Google Scholar
  38. Anne S. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992. Google Scholar
  39. Keven Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: The propositional fragment. In Post-proceedings of TYPES 2003 Workshop, number 3085 in LNCS, pages 355-377. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24849-1_23.
  40. Jui-Hsuan Wu. Proof theory, syntactic representations, logic, and sharing. PhD thesis, Institut Polytechnique de Paris, December 2023. Google Scholar
  41. Jui-Hsuan Wu. Proofs as terms, terms as graphs. In Chung-Kil Hur, editor, Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings, volume 14405 of Lecture Notes in Computer Science, pages 91-111. Springer, 2023. URL: https://doi.org/10.1007/978-981-99-8311-7_5.
  42. Noam Zeilberger. Focusing and higher-order abstract syntax. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 359-369. ACM, 2008. URL: https://doi.org/10.1145/1328897.1328482.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact