[Prev][Next][Index][Thread]
Refutation in Linear Logic
Date: Mon, 6 Jan 92 10:25:09 PST
Return-Path: <@Sunburn.Stanford.EDU:pratt@coraki.Stanford.EDU>
To: linear@cs.stanford.edu
Oops, that message on theoremhood in linear logic escaped prematurely.
Even Dan Quayle wouldn't have said "the theorems are those terms
denoting the top element of the Boolean or Heyting algebra constituting
the given model."
The simplest and clearest way to ask my question is probably in terms
of refutations. A refutation of a classical (intuitionistic)
proposition is a valuation of it in a Boolean (Heyting) algebra
yielding non-top. A refutation of a relevance logic proposition is a
valuation of it in a suitable model of relevance logic yielding a
nonreflexive element, one not >= t.
(The two-element lattice always suffices for classical refutations but
larger ones are required for those intuitionistic or relevant ones that
happen to be Boolean theorems.)
Would someone please enlighten me by completing the following
sentence?
A refutation of a linear logic proposition is a valuation of it in ...
yielding ...
(Bonus points for using "coherence space", but if you prefer another
model I won't object. Points off for "phase space" unaccompanied by
rationale.)
Vaughan Pratt