[Prev][Next][Index][Thread]
Kripke Models for Linear Logic
Date: Tue, 7 Jan 92 14:22:03 EST
To: linear@cs.stanford.edu
Folks, we have written a paper entitled "Kripke Models for Linear Logic"
which will be available (later today) via anonymous ftp at cica.indiana.edu
in the /pub/gtall subdirectory of the ftp directory. This paper has been
submitted to JSL (and some of you have copies from us). We post this abstract
as the paper may be of interest to some of you. There are serveral files in
that directory, you will need them all. Please contract us if you have any
problem.
Gerard Allwein
J.Michael Dunn
------------------------------------------------------------------------
Kripke Models for Linear Logic
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. Commutativity and associativity are isolated in such a way that the
base Kripke model is a model for non-commutative, non-associative Linear Logic.
The model rests heavily on Urquhart's representation of non-distributive
lattices and also on Dunn's Gaggle Theory. Indeed, the paper may be viewed as
an investigation into non-distributive Gaggle Theory restricted to binary
operations. The valuations on the Kripke model are three valued: true, false,
and indifferent. One can extract Priestley's representation theorem for
distributive lattices if the original lattice happens to be distributive. Hence
the representation is similar to 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.
We conservatively add contraction to get nondistributive Relevance
Logic of Robert Meyer's thesis (1966) (the logic of the automated theorem
prover in Thistlewaite, et.al). But we also extend Linear Logic by adding a
coimplication operator, similar to Curry's subtraction operator, which is
residuated with Linear Logic's cotensor product. And there are intensional
analogues to Sheffer's stroke and dagger operators. These extra operators
help to fill in the usual formulation of Linear Logic. They arise naturally
>from Gaggle theory and, without DeMorgan negation, are not interdefinable.
Negation is added in the Routley-Meyer way with a star operator instead of the
perp relation.
J. Michael Dunn - Gaggle Theory: "An Abstraction of Galois
Connections and Residuation, With Applications to Negation, Implication,
and Various Logical Operators", {LNAI 478, European Workshop JELIA '80}
P.B. Thistlewaite, M.A. McRobbie, R.K. Meyer - Automated Theorem Proving
in Non-Classical Logics {Research Notes in Theoretical Computer Science,
John Wiley & Sons, Inc., New York, Toronto and Pitman, London}
------
Date: Tue, 7 Jan 92 15:09:01 EST
Small addendum: we used (in the ftpable version) the tex symbol \Im for
Girard's upside down/horizontal mirror image ampersand for the co-tensor
product. And the ftp version of the paper is now available.
Gerard Allwein
J.Michael Dunn