Document

# Proof Nets for First-Order Additive Linear Logic

## File

LIPIcs.FSCD.2019.22.pdf
• Filesize: 0.66 MB
• 22 pages

## Acknowledgements

We would like to thank the anonymous referees for their constructive feedback. Dominic Hughes thanks his hosts, Wes Holliday and Dana Scott, at the UC Berkeley Logic Group.

## Cite As

Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Proof Nets for First-Order Additive Linear Logic. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.22

## Abstract

We present canonical proof nets for first-order additive linear logic, the fragment of linear logic with sum, product, and first-order universal and existential quantification. We present two versions of our proof nets. One, witness nets, retains explicit witnessing information to existential quantification. For the other, unification nets, this information is absent but can be reconstructed through unification. Unification nets embody a central contribution of the paper: first-order witness information can be left implicit, and reconstructed as needed. Witness nets are canonical for first-order additive sequent calculus. Unification nets in addition factor out any inessential choice for existential witnesses. Both notions of proof net are defined through coalescence, an additive counterpart to multiplicative contractibility, and for witness nets an additional geometric correctness criterion is provided. Both capture sequent calculus cut-elimination as a one-step global composition operation.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Proof theory
• Theory of computation → Linear logic
##### Keywords
• linear logic
• first-order logic
• proof nets
• Herbrand’s theorem

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Samson Abramsky. Sequentiality vs. Concurrency in Games and Logic. Mathematical Structures in Computer Science, 13(4):531-565, 2003.
2. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of LNCS, pages 222-236, 2010.
3. Robin Cockett and Luigi Santocanale. On the Word Problem for ΣΠ-Categories, and the Properties of Two-Way Communication. In Computer Science Logic (CSL), 18th Annual Conference of the EACSL, pages 194-208, 2009.
4. Vincent Danos. La Logique Linéaire appliquée à l'étude de divers processus de normalisation (principalement du Lambda-calcul). PhD thesis, Université Paris 7, 1990.
5. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181-203, 1989.
6. Didier Galmiche and Jean-Yves Marion. Semantic Proof Search Methods for ALL - a first approach -. Short paper in Theorem Proving with Analytic Tableaux, 4th International Workshop (TABLEAUX'95). Available from the first author’s webpage, 1995.
7. Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50(1):1-102, 1987.
8. Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. Logic and Algebra, pages 97-124, 1996.
9. Stefano Guerrini and Andrea Masini. Parsing MELL proof nets. Theoretical Computer Science, 254(1-2):317-335, 2001.
10. Willem Heijltjes. Classical proof forestry. Ann. Pure Appl. Logic, 161(11):1346-1366, 2010.
11. Willem Heijltjes. Proof nets for additive linear logic with units. In 26th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 207-216, 2011.
12. Willem Heijltjes and Dominic J. D. Hughes. Complexity bounds for sum-product logic via additive proof nets and Petri nets. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 80-91, 2015.
13. Willem Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Proof nets for first-order additive linear logic. Technical Report RR-9201, INRIA, 2018. URL: https://hal.inria.fr/hal-01867625/.
14. Jacques Herbrand. Investigations in proof theory: The properties of true propositions. In Jean van Heijenoort, editor, From Frege to Gödel: A source book in mathematical logic, 1879-1931, pages 525-581. Harvard University Press, 1967.
15. Stefan Hetzl. A sequent calculus with implicit term representation. In Computer Science Logic (CSL), volume 6247 of LNCS, pages 351-365, 2010.
16. Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In European Symposium on Programming, pages 122-138, 1998.
17. Dominic J. D. Hughes. Proofs Without Syntax. Annals of Mathematics, 164(3):1065-1076, 2006.
18. Dominic J. D. Hughes. Unification nets: canonical proof net quantifiers. In 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2018.
19. Dominic J. D. Hughes. First-order proofs without syntax. Available at arXiv.org, 2019.
20. Dominic J. D. Hughes and Willem Heijltjes. Conflict nets: efficient locally canonical MALL proof nets. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016.
21. Dominic J. D. Hughes and Rob van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. Transactions on Computational Logic, 6(4):784-842, 2005.
22. Andre Joyal. Free Lattices, Communication and Money Games. Proc. 10th Int. Cong. of Logic, Methodology and Philosophy of Science, 1995.
23. Joachim Lambek. Deductive Systems and Categories I, II, III. Theory of Computing Systems (I), Lecture Notes in Mathematics (II, III), 1968-1972.
24. Roberto Maieli. Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic. In 14th Int. Conf. Logic for Programming Artificial Intelligence and Reasoning (LPAR), pages 363-377, 2007.
25. Dale Miller. A Compact Representation of Proofs. Studia Logica, 46(4):347-370, 1987.
26. Samuel Mimram. The Structure of First-Order Causality. Mathematical Structures in Computer Science, 21(1):65-110, 2011.
27. Lutz Straßburger. A Characterisation of Medial as Rewriting Rule. In Franz Baader, editor, Term Rewriting and Applications, RTA'07, volume 4533 of LNCS, pages 344-358, 2007.
28. Philip Wadler. Propositions as Sessions. Journal of Functional Programming, 24(2-3):384-418, 2014.