Hostname: page-component-586b7cd67f-r5fsc Total loading time: 0 Render date: 2024-11-29T11:18:46.607Z Has data issue: false hasContentIssue false
  • English
  • Français

Kripke models for linear logic

Published online by Cambridge University Press:  12 March 2014

Gerard Allwein  and
J. Michael Dunn
Gerard Allwein
Affiliation:
Computer Science Department, Center for Innovative Computer Applications, Indiana University, Bloomington, Indiana 47405, E-mail: [email protected]
J. Michael Dunn
Affiliation:
Philosophy Department, Computer Science Department, Indiana University, Bloomington, Indiana 47405, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We present a Kripke model for Girard's Linear Logic (without exponentials) in a conservative fashion where the logical functors beyond the basic lattice operations may be added one by one without recourse to such things as negation. You can either have some logical functors or not as you choose. Commutativity and associativity are isolated in such a way that the base Kripke model is a model for noncommutative, nonassociative Linear Logic. We also extend the logic by adding a coimplication operator, similar to Curry's subtraction operator, which is residuated with Linear Logic's cotensor product. And we can add contraction to get nondistributive Relevance Logic. The model rests heavily on Urquhart's representation of nondistributive lattices and also on Dunn's Gaggle Theory. Indeed, the paper may be viewed as an investigation into nondistributive Gaggle Theory restricted to binary operations. The valuations on the Kripke model are three valued: true, false, and indifferent. The lattice representation theorem of Urquhart has the nice feature of yielding Priestley's representation theorem for distributive lattices if the original lattice happens to be distributive. Hence the representation is consistent with Stone's representation of distributive and Boolean lattices, and our semantics is consistent with the Lemmon-Scott representation of modal algebras and the Routley-Meyer semantics for Relevance Logic.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 58 , Issue 2 , June 1993 , pp. 514 - 545
Copyright
Copyright © Association for Symbolic Logic 1993

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]Allwein, Gerard, Duality of algebras for nonstandard logics and their topological models, Dissertation, Indiana University, Bloomington, 1992.Google Scholar
[2]Anderson, A. R. and Belnap, N. D., Entailment: the logic of relevance and necessity, vol. 1, Princeton University Press, Princeton, New Jersey, 1975.Google Scholar
[3]Avron, Arnon, The semantics and proof theory of linear logic, Theoretical Computer Science, vol. 57 (1988), pp. 161–184.CrossRefGoogle Scholar
[4]Białynicki-Birula, and Rasiowa, , On the representation of quasi-Boolean algebras, Bulletin de l'Académie Polonaise des Sciences, vol. 5 (1957), pp. 259–261.Google Scholar
[5]Birkhoff, Garrett, Lattice theory, American Mathematical Society, Providence, Rhode Island, 1940, 1948, 1967.Google Scholar
[6]Curry, Haskell B., Foundations of mathematical logic, McGraw-Hill, New York, 1963.Google Scholar
[7]Dunn, J. Michael, Relevance logic and entailment, Handbook of philosophical logic, vol. III (Gabbay, D. and Guenthner, F., editors), D. Reidel Publishing Company, Dordrecht, The Netherlands, 1986, pp. 117–224.CrossRefGoogle Scholar
[8]Dunn, J. Michael, Gaggle theory: an abstraction of Galois connections and residuation with applications to negation and various logical operations, Logics in AI, proceedings european workshop JELIA 1990, Lecture Notes in Mathematics, vol. 478, Springer-Verlag, Berlin, 1991, pp. 31–51.Google Scholar
[9]Girard, J.-Y., Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.CrossRefGoogle Scholar
[10]Jónsson, B. and Tarski, A., Boolean algebras with operators I–II, American Journal of Mathematics, vol. 73–74 (1951–1952), pp. 891–939, pp. 127–162.Google Scholar
[11]Lemmon, E. J.(in collaboration with Scott, Dana S.), An introduction to modal logic: The ‘Lemmon notes’ (Segerberg, Krister, editor), American Philosophical Quarterly Monograph Series, no. 11, Basil Blackwell, Oxford, 1977.Google Scholar
[12]Meyer, Robert K., Topics in modal and many-valued logics, Doctoral Dissertation, University of Pittsburgh, Pittsburgh, Pennsylvania, 1966.Google Scholar
[13]Priestley, H. A., Ordered topological spaces and the representation of distributive lattices, Proceedings of the London Mathematical Society, vol. 24 (1972), pp. 507–530.CrossRefGoogle Scholar
[14]Routley, Richardet al., Relevant logics and their rivals, Ridgeview Publishing Company, Atascadero, California, 1982.Google Scholar
[15]Urquhart, Alasdair, A topological representation theory for lattices, Algebra Universalis, vol. 8 (1978), pp. 45–58.CrossRefGoogle Scholar