Hostname: page-component-cd9895bd7-gbm5v Total loading time: 0 Render date: 2024-12-26T13:07:46.938Z Has data issue: false hasContentIssue false
  • English
  • Français

The geometry of non-distributive logics

Published online by Cambridge University Press:  12 March 2014

Greg Restall  and
Francesco Paoli
Greg Restall
Affiliation:
Department of Philosophy, The University of Melbourne, Victoria 3010, Australia, E-mail: [email protected]
Francesco Paoli
Affiliation:
Dipartimento di Scienze Pedagogiche e Filosofiche, Università di Cagliari, Via Ls Mirrionis 1, 09123 Cagliari, Italy, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper we introduce a new natural deduction system for the logic of lattices, and a number of extensions of lattice logic with different negation connectives. We provide the class of natural deduction proofs with both a standard inductive definition and a global graph-theoretical criterion for correctness, and we show how normalisation in this system corresponds to cut elimination in the sequent calculus for lattice logic. This natural deduction system is inspired both by Shoesmith and Smiley's multiple conclusion systems for classical logic and Girard's proofnets for linear logic.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 70 , Issue 4 , December 2005 , pp. 1108 - 1126
Copyright
Copyright © Association for Symbolic Logic 2005

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Battilotti, G. and Sambin, G., Basic logic and the cube of its extensions, Logic and foundations of mathematics (Cantini, A.et al., editors), Kluwer, 1999, pp. 165–185.CrossRefGoogle Scholar
[2]Belnap, Nuel D., Display logic, Journal of Philosophical Logic, vol. 11 (1982), pp. 375–417.CrossRefGoogle Scholar
[3]Birkhoff, Garrett, Lattice theory, American Mathematical Society Colloquium Publications, Rhode Island, 1973.Google Scholar
[4]Carbone, A., Duplication of directed graphs and exponential blow up of proofs, Annals of Pure and Applied Logic, vol. 100 (1999), pp. 1–67.CrossRefGoogle Scholar
[5]Cockett, J. R. B. and Seely, R. A. G., Finite sum-product logic, Theory and Applications of Categories, vol. 8 (2001), no. 5, pp. 63–99.Google Scholar
[6]Chiara, M. L. Dalla and Giuntini, R., Paraconsistent quantum logics, Foundations of Physics, vol. 19 (1989), pp. 891–904.CrossRefGoogle Scholar
[7]Chiara, M. L. Dalla, Quantum logics, Handbook of philosophical logic (Gabbay, D. and Guenthner, F., editors), vol. 6, Kluwer, 2002.Google Scholar
[8]Danos, Vincent and Reignier, Laurent, The structure of multiplicatives, Archive of Mathematical Logic, vol. 28 (1989), pp. 181–203.CrossRefGoogle Scholar
[9]Davey, B. A. and Priestley, H. A., Introduction to lattices and order, Cambridge University Press, Cambridge, 1990.Google Scholar
[10]Diestel, Reinhard, Graph theory, second ed., Graduate Texts in Mathematics, vol. 173, Springer Verlag, 2000, Text available at http://www.math.uni-hamburg.de/home/diestel/books/graph.theory/.Google Scholar
[11]Dunn, J. Michael and Hardegree, Gary M., Algebraic methods in philosophical logic, Clarendon Press, Oxford, 2001.CrossRefGoogle Scholar
[12]Girard, Jean-Yves, Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–101.CrossRefGoogle Scholar
[13]Girard, Jean-Yves, Proof-nets: the parallel syntax for proof theory, Logic and algebra (New York), Dekker, 1996, pp. 97–124.Google Scholar
[14]Grätzer, George, General lattice theory, Academic Press, 1978.CrossRefGoogle Scholar
[15]Hughes, D. J. D. and van Glabbeek, R. J., Proof nets for unit-free multiplicative-additive linear logic, Proceedings of the 18th Annual IEEE Symposium on Logic and Computer Science (Ottawa), 06 2003, extended abstract, pp. 1–10.Google Scholar
[16]Nishimura, H., Sequential method in quantum logic, this Journal, vol. 45 (1980), pp. 339–352.Google Scholar
[17]Oliveira, A. G. and de Queiroz, R. J. G. B., Geometry of deduction via graphs of proof Logic for concurrency and synchronization (de Queiroz, R. J. G. B., editor), Kluwer, 2003, pp. 3–88.CrossRefGoogle Scholar
[18]Restall, Greg, An introduction to substructural logics, Routledge, 2000.CrossRefGoogle Scholar
[19]Monting, J. Schülte, Cut elimination and word problem for varieties of lattices, Algebra Universalis, vol. 12 (1981), pp. 290–321.CrossRefGoogle Scholar
[20]de Falco, L. Tortora, The additive multiboxes, Annals of Pure and Applied Logic, vol. 120 (2003), pp. 65–102.CrossRefGoogle Scholar
[21]de Falco, L. Tortora, Additives of linear logic and normalization. Part I: A (restricted) Church-Rosser property, Theoretical Computer Science, vol. 294 (2003), pp. 489–524.CrossRefGoogle Scholar