Theoremhood in linear logic

To: types
Subject: Theoremhood in linear logic
From: Vaughan Pratt <pratt@cs.Stanford.EDU>
Date: Mon, 06 Jan 92 11:05:20 EST
Sender: meyer@theory.lcs.mit.edu

Date: Sat, 4 Jan 92 00:15:09 PST
To: linear@cs.stanford.edu

While there are a good many models claimed by now for linear logic,
I don't recall seeing any used to provide a semantic criterion for
theoremhood.

The analogous situation for models of propositional logic, whether
classical or intuitionistic, is that the theorems are those terms
denoting the top element of the Boolean or Heyting algebra constituting
the given model.

For sufficiently strong relevance logic, the theorems are those
denoting the "reflexive" elements of the model, those A satisfying
t -> A (or t < A) where t is the tensor unit (this is the definition of
"reflexive" in the binary relation interpretation).

What if anything is the appropriate semantic criterion of theoremhood
for a model of linear logic?  Presumably something reminiscent of
"inhabited", but I haven't seen anything claiming even this much, let
alone a precise definition.  Is there one?

If one can do no better than to say that a theorem is a morphism with a
proof, is not "model of linear logic" a misnomer for what is really
just good clean proof theory?

Pointers to where this issue is discussed would be greatly appreciated.

	Vaughan Pratt