SEMANTICAL INVESTIGATIONS OF LINEAR LOGIC

ALDO URSINI

Abstract. We deal with propositional linear logic. We present semantics of connectives for commutative, cyclic, noncommutative intuitionistic, classical linear logic with exponentials. The first semantic is on quasi ordered binars (“linear frames”), the second one deals with relational binars (“phasoids” and Kripke semantics), the third is algebraic linear logic (“girales”), the fourth is obtained by dumping the tensor and putting linear implications on the spotlight (“quivers”).

to Elena, who suffered the most because of it.

Dixi et servavi animam meam

(K. Marx.

Randglossen zum Programme des Deutschen Arbeitspartei Neue Zeit 9(I) 561, 1875)

Introduction

This paper deals with linear logic: [6],[2],[28], commutative, cyclic, non-commutative, with exponentials, and is devoted to the semantic of the logical operations (connectives and exponentials). Thus by “semantic” we mean here the old style assignment of “values” to formulas in suitable mathematical structures, as distinct from denotational semantic, or from semantic of computation (= cut-elimination procedure).

(i) The first trigger was the wish to clarify the meaning of the connective ⅋ which J.-Y. Girard himself qualifies as “mysterious” in a couple of occasions [7],[8]. We anticipate the following, in terms of Kripke models:

p ⊩ A ⅋ B iff ∀x∀y(p R xy → (∃u(u R x ∧ u ⊩ A) ∨ ∃v(v R y ∧ v ⊩ B)))

(think of p,x,y as phases [6], · as phase composition, and R is a “compatibility” binary relation on phases, with certain properties)

This is pretty satisfying : it shows the nature of the connective as a parallel disjunction indeed, but, because of the appeal to “x·y”, also its links with a tensoresque conjunction.

Another thorny connective which gets a satisfying explanation, in the same terms, is ⊕:

p ⊩ A ⊕ B iff ∀x(p R x → ∃y(y R x ∧ (y ⊩ A ∨ y ⊩ B)).

Exponentials come down first order, via the notion of base for exponentials W, a set of phases with certain properties, so that for instance:

p ⊩!A iff ∀x(p R x → ∃y(y R x ∧ y ∈ W ∧ y ⊩ A)).

(ii) The starting point occurred a few years ago [25], with the stubborn idea of a “linear negation” interpreted exactly as Kripke did for intuitionistic negation in [13]:

p ⊩ A^{⊥} iff ∀x(p R x → x ⊮ A).

But, alas, we wanted that negation to be involutive... Thus R could not be any (quasi) order and had to have special properties.

(iii) In the meanwhile, also the impaired version iLL of linear logic came into the picture [9], [1]: loosely speaking you get it from the full system LL by restricting to impaired sequents i.e. no more then one formula allowed on the right side. Thus we went back to (quasi)orders after all (Sec. 2.7 below).

(iv) As with any semantic, we want to show that in the end the quantifier ∀ is tantamount as the quantifier ∃; even if you better do not tell this to your students as frankly as stated a completeness theorem sounds like:

“For all models S in a class C, a formula A holds in S” iff “There is a proof of formula A”

The theoretician wants perhaps C to be as wide as possible, to rejoice of the power of his logic. The manager of the National Research Council wants better C to be as narrow as possible, and a two element set is considered the best of all, in the expectation of being able to produce by semantical means some spendable logical truth. (The manager has to be very patient with LL , because ([16]) propositional linear logic with exponentials is undecidable: no room for people who like to have the machine perform the work in their place). However, there may be other attitudes in between...

(v) We had in mind the following guidelines :

1. To get completeness by a number of different classes of structures; this could perhaps help with our main aim in (i) above. By the same token, these classes of structure have a side after which they are equivalent: they all modelize the same logic. On the other side, any semantic at all is nothing else than a translating device from one language into another; hence the two languages are “equivalent”; yet the result may be worth of the fatigue ... If you are not convinced, try to make sense of hieroglyphics encoded over Egyptian obelisks, without any key.

2. To keep the structures as low level as possible: no infinitary operations, no second order axioms, even for exponentials. We guess that anybody likes very much having Heyting Algebras instead of something like: “The class C of all algebras which are subalgebras of the algebras of open sets of T_{0} topological spaces having a base of compact open sets”. On the contrary, you may get an advancement in your career once you discover that equivalence, but most probably you go on making your formal intuitionistic calculations on plain, old, dear Heyting Algebras don’t you? (I do ..., unless I am looking for a counterexample.)

3. To find solutions to the proportions :

Boolean Algebras : PC =
X : LL =
Y : iLL =

and their non commutative or cyclic counterparts; PC is classical propositional calculus. (This, if well dressed, may positively affect even your not-that-warm friend, the manager.)

The springouts we like to anticipate here are: • a Kripke semantic for iLL (Sec 5 );

• a Kripke semantic for LL:

(a) as an extension of that for iLL (Sec 7);

(b) by a direct study of the relations on formulas: “⊢ A, B is provable”

((b) amounts to give an inductive definition of that relation, by induction on the complexity of formula A. So that if you happen to know everything on

“⊢ P, B is provable”

for all atoms P, then you know everything for all formulas A.)

• algebraic and quasi-algebraic semantic (Sec 10): in the first case we want plain, first order, algebras; quasi-algebra is a new brand, invented to cope with Girard’s idea of a “turbo monoid” explained in [8], p. 24 - after you insert a footnote in order to make the proof on that page work-. (A quasi-algebra is an algebra with a somehow ”compatible” quasi order on it; the mother of all ordered structures, in Babylonian terms: the obstetrician is a passage to the quotient.)

• and finally an approach to semantic focused directly on linear implication, leaving the tensoresque conjunction behind the scene.

Among the possible further developments, we underline : a. First order logics; the logic for finite structures (see [14]). b. Try the method with LU, LC, LLL and whatever else Girard will have produced in

the meanwhile. c. Embeddings and translations semantically unveiled. d. Try to make sense of the proportion:

SETS : PC = MULTISET : LL

which will be dealt with in a subsequent paper. The appendices are there to help the reader, hopefully:

A. lists the logics considered.

B. lists the main definitions, a few examples and applications.

C. contains a few comments on the connections with the existing literature on the subject, up to the best of our knowledge.

With regard to App. C: the author has many debts to many people. Thus the notion of linear frame, Sec.2, is obtained by a vampiric feeding on Dedekind’s idea of dealing with non existing things, typically “the supremum of all rationals whose square is at most twelve”, or, in our case, the “implication” a −^{}b of two phases a, b, AS IF they really existed. The novelty, if any, is that we literally keep on the wedge, and try to resist as long as possible from making them exist by some kind of “quotient”, as it is usual to do. (Any way, this is a very old technique to avoid unwanted pregnancies...)

Similarly, girales (Sec 10) were in the air: [4], [17], etc. The novelty, if any, is that we do not want any infinitary operations around. (We doubt they are needed for the first order case too..., it should be enough that you have some suprema to exist, not necessarily that they have all to exist: overpopulation is avoidable,whatever His Holiness preaches about.)

Such a list of acknowledgments would soon become an attempt to Brazilian forests: therefore let us submit the following WARNING: “That on no result or idea in the present paper the author has any claim to priority, except, perhaps, Sec 11”. At this point we must give a motivation for reading this paper. It may be found in the so-called

Archimede’s Principle

namely: “A big enough number of very small improvements might achieve a non trivial advancement”. Above, in fact, we have paid our tribute to the scientific “société du spectacle” [5], by advertising on some of the improvements presented in this paper.

1. Preliminaries and notations

1.1. Given a set M, let K be a closure operator on M, i.e. for every X, Y ⊆ M 1. X ⊆ K(X);

2. K(X) ⊆ K(Y) if X ⊆ Y;

3. K(K(X)) = K(X). A set X ⊆ M is K-closed if K(X) = X and K-open if M ∖ X is K-closed.

A mapping f : M ⟶ M is K-continuous if f^{−1}(K(X)) is K-closed for every X ⊆ M (or equivalently if f^{−1}(X) is K-open whenever X is K-open). This notion extends to n-ary mapping componentwise: g : M × M ⟶ M is K-continuous if for every a ∈ M both mappings

g_{a}(x) = g(a, x) _{a}g(x) = g(x, a)

are K-continuous.

Let B be a base of K-open sets, namely a set of K open sets such that, whenever X is K-open and p ∈ X, then there is some Y ∈ B such that p ∈ Y ⊆ X. Then of course a mapping f is K-continuous iff f^{−1}(Y) is K-open whenever Y ∈ B.

1.2. Let M be a set and R be a binary relation on M; R^{⌣} will denote the converse of R. Let us define for a ∈ M and X ⊆ M

Ra ≡ R(a) = {y : a R y}
R(X) = ⋃{R(x) : x ∈ X}
Cl^{R}(X) = {y : R(y) ⊆ R(X)}
X^{R} = {y : R(y) ∩ X = ∅}.

Then one easily shows that

X^{R} = M ∖ R^{⌣}(X)
Cl^{R}(X) = (X^{R^{⌣}})^{R}
Cl^{R} is a closure operator on M

The Cl^{R}-closed subsets will be called R-closed and their complements are called R^{⌣}- open. It is readily seen that X is R-closed iff X = Y^{R} for some Y ⊆ M and X is R^{⌣}-open if, whenever p ∈ X, then for some g, p ∈ R^{⌣}(g) ⊆ X. Thus {R^{⌣}(g) : g ∈ M} is a base of R^{⌣}-open sets. In other words R^{⌣}-open subsets are exactly those of the form R^{⌣}(X) for some X ⊆ M. Notice that a ∈ R^{⌣}(M) iff Ra ≠ ∅.

Remarks. 1. A closure operator K on M is tame if there is a binary relation R on M such that K = Cl^{R}. Of course K is tame iff there is a base of K-open sets of cardinality not greater then Card(M), iff there is a mapping t from M into the set of K-open subsets of M such that t(M) is a base of K-open subsets. (Define R by a R b iff a ∈ t(b)).

2. Any (infinite) topological space of weight (see [12]) not bigger than its cardinality is tame. Thus any infinite first countable or metrizable topological space is tame.

1.3. If R ⊆ M × M, let R^{c} be the complement of R, i.e. a R^{c} b iff a R̸ b. A mapping f : M ⟶ M is Cl^{R^{c}}-continuous iff for any a, b, p ∈ M, if

∀q(∀z(f(z) R a → z R b) → p R b) then f(a) R p.

In fact a base of Cl^{R^{c}}-open sets is {R^{c⌣}a : a ∈ M}; if you make explicit the fact that f^{−1}(R^{c⌣}a) be still Cl^{R^{c}}-open, you get 1.3.

For a mapping from M × M into M we get a similar statement (componentwise).

1.4. Given R ⊆ M × M, define ≤_{R} (or simply ≤) by

a ≤ b iff Rb ⊆ Ra iff b ∈ Cl^{R}({a}) (∘)

Then ≤ is clearly a quasi-order (i.e. reflexive and transitive). Of course ≤ is a quasiorder iff there is a relation R such that (∘). The equivalence relation associated to ≤, namely a ∼ b iff a ≤ b and b ≤ a, is then defined by Ra = Rb.

Of course if K is any closure operator, b ∈ K({a}) defines a quasi-order a ≤ b.

1.5. Given a tame closure operator Cl^{R} observe that

(i) R(Y) = R(Cl^{R}(Y)); (ii) X is R^{⌣}-open iff X = R(Y) for some R-closed Y. (iii) For every X ⊆ M, the set X^{+R} = (M ∖ X)^{R} = {p : Rp ⊆ X} is R-closed. (iv) X = R(Y) iff Cl^{R}(Y) = X^{+R}, i.e. (R(Y))^{+R} = Cl^{R}(Y).

(v) The mapping X ⟼ X^{+R} is a bijection from the set O^{R^{⌣}}(M) of the R^{⌣}-open subsets of M onto the set C^{R}(M) of R-closed subsets of M.

The proof is left as an exercise. Thus a tame closure operator Cl^{R}(X) = X^{R^{⌣}R}. Notice that

Cl^{R}(X^{R}) = X^{R}

which is awkward, because one would like to have

Cl^{R}(X^{R^{⌣}}) = X^{R^{⌣}},

so that in fact one would have

X^{R^{⌣}R} = X^{RR^{⌣}}.

Let us see how to make this happen; the following are equivalent:

1. Cl^{R^{⌣}}(X) ⊆ Cl^{R}(X) for all X ⊆ M;

2. R^{⌣}(X) ⊆ R^{⌣}(Y) implies R(X) ⊆ R(Y) for all X, Y ⊆ M;

3. for all X ⊆ M, if X = Cl^{R^{⌣}}(X), then X = Cl^{R}(X);

4. a R b iff there is a u ∈ R^{⌣}a such that Ru ⊆ R^{⌣}b;

5. for all X ⊆ M, R^{⌣}(X) = R(X^{RR});

6. for all a ∈ M, R^{⌣}a = (R^{⌣}a)^{+R};

7. for all a ∈ M, R^{⌣}a is R^{⌣}-open;

8. for all X ⊆ M, R^{⌣}(X) is R^{⌣}-open. 1., 2. and 3. are obviously equivalent. Assume 1. and show 4.: one direction is trivial, so assume ∀u ∈ R^{⌣}a, Ru ⊈ R^{⌣}b. Set X = {h : h R̸ b}; then R^{⌣}a ⊆ R^{⌣}(X), hence a ∈ Cl^{R}(X), hence by 1., Ra ⊆ R(X), i.e. a R̸ b.

Next 4. implies 5. Let a R b for some b ∈ X; then ∃u ∈ R^{⌣}a such that Ru ⊆ R^{⌣}b ⊆ R^{⌣}(X). Then u ∈ X^{RR} i.e. a ∈ R(X^{RR}); conversely if a ∈ R(X^{RR}) and u R a for some a ∈ X^{RR}, then Ru ⊆ R^{⌣}(X), hence a ∈ R^{⌣}(X).

It is trivial that 5. implies 6. implies 7.; 7. implies 8. simply because

R^{⌣}(⋃_{i∈I} Y_{i}) = ⋃_{i∈I} R^{⌣}(Y_{i}).

Next 8. implies 4.: if a R b, then a ∈ R^{⌣}b = R(Y) for some Y ⊆ M, thus there is a u ∈ Y such that u R a and Ru ⊆ Ry ⊆ R^{⌣}b. Finally 4. implies 1.: let R^{⌣}p ⊆ R^{⌣}(X). Then for p R z, let U ∈ R^{⌣}p such that Ru ⊆ R^{⌣}z. Then u R x for some x ∈ X; hence x R z and z ∈ R(X), namely Rp ⊆ R(X).

1.6. Of course if we want to have for X ⊆ M

X^{RR^{⌣}} = X^{R^{⌣}R}

we have to take the conjunction of any of the properties listed above with the “dual” one (i.e. replacing R with R^{⌣}). This might be called semi-symmetry for R; while it is a first order property (see 4. in 1.5 above) it is rather cumbersome. Thus, since it will be enough for our aim, we stick to a somehow stronger condition. We say that R is quasi-symmetric if

{Ru : u ∈ M} = {R^{⌣}u : u ∈ M}

i.e. if for all a ∈ M there are a′, a′′ such that

∀b((a R b ↔ b R a′) ∧ (b R a ↔ a′′ R a)).

Remark. In the list in 1.5 item 2. cannot be weakened to “R^{⌣}a ⊆ R^{⌣}b → Ra ⊆ Rb” for all a, b ∈ M, as simple examples show.

One property we will use below is the following: assume R is quasi-symmetric and also that there is a binary operation · in M such that for all a, b, c ∈ M, a R bc iff ab R c; then

Ra ⊆ R(X) and Rb ⊆ R(Y) imply R(ab) ⊆ R(X · Y)

where X · Y = {xy : x ∈ X, y ∈ Y }. The proof is a nice exercise in quasi-symmetry.

1.7. If R is quasi-symmetric, Cl^{R} and Cl^{R^{⌣}} collapse. We set

Q(X) = Cl^{R}(X) = Cl^{R^{⌣}}(X)

thus X is Q-closed iff X = Y^{R} for some Y iff X = Y^{R^{⌣}} for some Y.

(i) When R is quasi symmetric a kind of duality principle applies, namely one can safely substitute R with R^{⌣} in most true assertions (we do not bother to formulate it precisely).

(ii) If ≤ is a quasi-order, we should officially write ≤^{⌣} x for the set {a : a ≤ x}; instead

we use the notation x̂. Thus a ∼ b means â = b̂. (iii) If R is quasi-symmetric, the partial order ≤_{R} coincides with ≤_{R^{⌣}}. The quotient

structure via the equivalence ∼ is still quasi-symmetric.

2. Linear frames

2.1. By a (commutative) linear frame we mean a structure ⟨M, ·, e, ≤ ⟩ where

1. ≤ is a quasi-order on the set M (i.e. ≤ is reflexive and transitive); let us put x ∼ y for x ≤ y and y ≤ x;

2. · is a binary operation on M which is quasi-associative: for a, b, c ∈ M, a(bc) ∼ (ab)c;

3. · is quasi-commutative, i.e. x · y ∼ y · x;

4. · preserves ≤ : for a, x, y ∈ M, x ≤ y implies ax ≤ ay;

5. · is continuous: for a, b, p ∈ M, if

∀q(∀z(az ≤ b → z ≤ q) → p ≤ q)

then ap ≤ b;

6. e ∈ M.

Notice that is ≤ is antisymmetric (i.e. ⟨M, ≤⟩ is a poset), then ⟨M, ·⟩ is a semigroup. The linear frame is then called reduced: it is a (commutative) partially ordered semigroup satisfying 5. and 6.

2.2. Remarks. (1) To define a general (not necessarily commutative) linear frame, drop the assumption that · is quasi-commutative and double 3.,4. and 5. to cover both possibilities (in Section 7 we will deal in outline with the matter of noncommutativity).

(2) The notion of continuity is a true notion of continuity: it means that · is S-continuous, where a S b iff a ≰ b.

2.3. If X ⊆ M, a ∈ M we write X ≤ a to mean: x ≤ a for all x ∈ X. Also recall that â = {x : x ≤ a}, so that X ≤ a is the same as X ⊆ â.

The operator Cl^{≤⌣}, simply denoted by Cl, is the Dedekind-McNeilly operator (adapted to the quasi-ordering case): for X ⊆ M

p ∈ Cl(X) ↔ ∀g(X ≤ g → p ≤ g).

Observe that X ≤ a iff Cl(X) ≤ a. The Cl-closed subsets of M, simply called M-closed, form a set, denoted by C(M). Notice that x ≤ x′ ∈ Cl(X) → x ∈ Cl(X).

2.4. For X, Y ⊆ M, we define as usual X · Y = {x · y : x ∈ X, y ∈ Y } and X ⊗ Y = Cl(X · Y); by a · Y we mean {a} · Y.

Observe that for a ∈ M, â ∈ C(M). Moreover, for a, b ∈ M

â ⊗ b̂ = âb.

In fact ab ∈ â ⊗ b̂ and conversely, if l ≤ a, m ≤ b, then lm ≤ ab, i.e. â · b̂ ≤ âb, which is closed; thus â ⊗ b̂ ≤ âb.

2.5. For X, Y ⊆ M let us define X −^{}Y by

p ∈ X −^{}Y iff ∀q∀z(q ∈ X ∧ z ≤ pq → z ∈ Y).

Then observe that for a, b ∈ M

â −^{}b̂ = {p : pa ≤ b}.

In fact if pa ≤ b and q ≤ a, z ≤ pq, then z ≤ pa ≤ b, hence p ∈ â −^{}b̂. Conversely if p ∈ â −^{}b̂, take z = pa to conclude pa ≤ b.

It follows in particular that the axiom of continuity is equivalent to

∀a, b ∈ M : â −^{}b̂ is closed.

Therefore X ≤ â −^{}b̂ iff Cl(X) ≤ â −^{}b̂ for X ⊆ M. Hence for any a, b ∈ M, X, Y ⊆ M:

a · X ≤ b iff a · Cl(X) ≤ b
a · X ⊆ Y ⇒ a ∈ X −^{}Cl(Y).

2.6. For X, Y ⊆ M

Cl(X) · Cl(Y) ⊆ X ⊗ Y.

In fact, if X · Y ≤ t and u ∈ Cl(X), v ∈ Cl(Y), we have to show that uv ≤ t. If a ∈ X, b ∈ Y we have a ∈ b̂ −^{}t̂, namely

X ⊆ ⋂_{b∈Y} b̂ −^{}t̂,

which is closed. Thus u ∈ b̂ −^{}t̂for every b ∈ Y, i.e. ub ≤ t for every b ∈ Y, i.e. uY ≤ t, whence Y ⊆ û −^{}t̂, which is closed. Thus v ∈ û −^{}t̂ and finally uv ∈ t̂. It follows that for X, Y ⊆ M:

Cl(X) ⊗ Cl(Y) = X ⊗ Y.

2.7. For X, Y, Z ⊆ M

X ⊗ Y ⊆ Z implies Y ⊆ X −^{}Cl(Z).

In fact, if p ∈ Y, q ∈ X and Z ≤ pq, then for any t such that Z ≤ t, we get pq ≤ t, hence z ≤ t, i.e. z ∈ Cl(Z).

It follows that for X, Y, Z ∈ M:

if Z ∈ C(M) and X · Y ⊆ Z then Y ⊆ X −^{}Z.

2.8. For X, Y ⊆ M, b ∈ M:

if Y ≤ b then X · (X −^{}Y) ≤ b.

In fact if a ∈ X, c ∈ X −^{}Y, we have ac ∈ Y, hence ac ≤ b.

It follows that for X, Y ⊆ M

X ⊗ (X −^{}Y) ⊆ Cl(Y).

In fact let p ∈ X ⊗ (X −^{}Y), i.e. ∀z(X · (X −^{}Y) ≤ z → p ≤ z); hence for every b, if Y ≤ b then p ≤ b, i.e. p ∈ Cl(Y).

2.9. For X, Y, Z ⊆ M

if X ⊆ Y −^{}Z then X · Y ⊆ Cl(Z).

In particular

if Z is closed, X · Y ⊆ Z iff Y ⊆ X −^{}Z,

and if p ∈ M

if Z is closed, p ∈ X −^{}Z iff p · X ⊆ Z.

In fact from X ⊆ Y ⊗ Z we get (via 2.8)

X · Y ⊆ Y · (Y −^{}Z) ⊆ Cl(Z).

2.10. For X, Y ⊆ M

Cl(X −^{}Y) ⊆ Cl(X) −^{}Cl(Y).

In fact

Cl(X) ⊗ Cl(X −^{}Y) = X ⊗ (X −^{}Y) ⊆ Cl(Y)

thus

Cl(X −^{}Y) ⊆ Cl(X) −^{}Cl(Cl(Y))
= Cl(X) −^{}Cl(Y).

It follows that

if X, Y ∈ C(M) then X −^{}Y ∈ C(M).

2.11. We further define for X, Y ∈ M

X & Y = X ∩ Y
X ⊕ Y = Cl(X ∪ Y)
T = M
0 = {p : p ≤ y for all y ∈ M}
1 = {p : px ≤ x for all x ∈ M}

Trivially, if X, Y ∈ C(M), then X & Y and X ⊕ Y belong to C(M). Of course 0 = Cl(∅) and T are closed; also 1 is closed, in fact (by 2.5)

1 = ⋂_{a∈M}(â −^{}â)

(p ∈ 1 iff ∀a, pa ≤ a iff ∀a, p ∈ â −^{}â).

2.12. To deal with negation we define

⊥ = {p : p ≤ e} = ê
COMP = {p : p ≰ e},

and for X ⊆ M we define X^{⊥} by

p ∈ X^{⊥} iff ∀q(pq ∈ COMP → q ∉ X).

If we define a γ b to mean ab ∈ COMP we get

X^{⊥} = X^{γ}

in the notation of Sec. 1. Thus γ is an “accessibility relation” in M. Observe also that ⊥ is closed.

2.13. For X ⊆ M,

X^{⊥} = X −^{}⊥.

In fact let p ∈ X, i.e. ∀q(pq ≰ e → q ∉ X), thus if q ∈ X and z ≤ pq then z ≤ e, hence p ∈ X −^{}⊥. Conversely let p ∈ X −^{}⊥. If q ∈ X: then pq ≤ e. Hence p ∈ X^{⊥}.

2.14. 1 = ⊥^{⊥}.

In fact if pe ≤ e and q ≤ e, then pq ≤ pe ≤ e. Conversely if p ∈ ⊥^{⊥}, of course pe ≤ e.

2.15. For X, Y ⊆ M we define X ⅋ Y by

p ∈ X ⅋ Y iff ∀x∀y(X ≤ x and Y ≤ y then p ≤ xy).

Then for every X, Y ⊆ M,

X ⅋ Y is closed.

In fact, assume p ∈ Cl(X ⅋ Y), X ≤ x, Y ≤ y. Then if u ∈ X ⅋ Y, u ≤ xy; namely X ⅋ Y ≤ xy. Thus p ≤ xy and hence p ∈ X ⅋ Y.

Observe also that

X ⅋ Y = Cl(X) ⅋ Cl(Y)

and that {a} ⅋ {b} = â ⊗ b̂ = âb. This operation may deserve further investigation in iLL.

12 ALDO URSINI

2.16. Properties of a (commutative) linear frame ⟨M, ·, e, ≤⟩.

(i) ∀X ⊆ M, X ⊗ 0 = 0. In fact let p ≤ x for all x ∈ M, a ∈ M. We have, by continuity, ap ≤ x for all x ∈ M, since p ≤ q for all q. (ii) ∀X ⊆ M, 1 ⊗ X ⊆ Cl(X). In fact 1 · X ⊆ Cl(X): let p ∈ 1, x ∈ X. Then px ≤ x, hence px ∈ Cl(X). (iii) In C(M), ⊗ is associative (and commutative). For the proof, first observe that for X, Y ⊆ M and a ∈ M

X · Y ≤ u iff X · Cl(Y) ≤ u.

In fact, assume X · Y ≤ u. Let x ∈ X, y ∈ Cl(Y): to prove xy ≤ u use continuity. Thus assume ∀z(xz ≤ u → z ≤ q) and show that y ≤ q. In fact in particular Y ≤ q and hence y ≤ q.

Now p ∈ X ⊗ (Y ⊗ Z) = Cl(X · Cl(Y · Z)) iff ∀u(X · Cl(Y · Z) ≤ u → p ≤ u) iff ((X · Cl(Y · Z)) ≤ u → p ≤ u) iff (using quasi-associativity) ∀u((X · Y) · Z ≤ u → p ≤ u) iff p ∈ (X ⊗ Y) ⊗ Z. (And similarly for commutativity). 2.17. Given a frame ⟨M, ·, e ≤, ⟩ fix a subset N ⊆ M. For every X ⊆ M define

!^{N}(X) = Cl(X ∩ N)

?^{N}(X) = {p : ∀x((X ≤ x ∧ x ∈ N) implies p ≤ x}.

Observe that if X ≤ x ∈ N, then ?^{N}(X) ≤ x. So, if g ∈ Cl(?^{N}(X)) then ?^{N}(X) ≤ x implies g ≤ x. Thus if X ≤ x ∈ N, then g ≤ x, i.e. g ∈?^{N}(X). Hence

(i) ?^{N}(X) ∈ C(M) for every X ⊆ M. Also we have for any X, Y ⊆ M (ii) if X ⊆ Y then !^{N}(X) ⊆!^{N}(Y) and ?^{N}(X) ⊆?^{N}(Y); (iii) X ⊆?^{N}(X) = ?^{N}Cl(X). In fact the equality stems from X ≤ a iff Cl(X) ≤ a and the inclusion is obvious. (iv) X ∩ N ⊆!^{N}(X) ∩ N and !^{N}(X) ⊆!^{N}(!^{N}(X)). The first inclusion is trivial. Hence

!^{N}(X) ⊆ Cl(!^{N}(X) ∩ N) = !^{N}!^{N}(X).

(v) If X is closed, then !^{N}(X) = !^{N}!^{N}(X). (In fact we have !^{N}(X) ⊆ X.) (vi) ?^{N}?^{N}(X) = ?^{N}(X). One inclusion follows from (iii), the other again since X ≤ x ∈ N implies ?^{N}(X) ≤ x. (vii) !^{N}(X) = Cl(N) if X ⊆ N; ?^{N}(∅) = ?^{N}(0) = {p : p ≤ x for all x ∈ N}. Not much more can be said in general on ?^{N} and !^{N}. More must be assumed to get further properties. Thus (viii) ⊥ ⊆?^{N}(∅) (i.e. ⊥ ⊆?^{N}(X) for every X) iff e ≤ x for every x ∈ N. (ix) ?^{N}⊥ = ⊥ iff there exists a g ∈ N such that e ∼ g.

(x) !^{N}(M) ⊆ 1 (i.e. !^{N}(X) ⊆ 1 for every X) iff Cl(N) ⊆ 1. (xi) !^{N}1 = 1 (i.e. 1 ⊆!^{N}1) iff 1 ⊆ Cl(N ∩ 1).

2.18. We define a base for exponentials on the linear frame ⟨M, ·, e, ≤⟩ to be a pair of subsets ⟨W, N⟩ of M such that

1. W ⊆ 1 and for every u, v ∈ W there is a w ∈ W such that w ∼ uv, and uu ∼ u (W is an ϵ-base);

2. there is a g ∈ N such that e ∼ g;

3. (connection axiom) whenever u ∈ W and v ∈ N, there is a g ∈ N such that

û −^{}v̂ = ĝ, (namely: g ∈ N, ug ≤ v and ux ≤ v implies x ≤ g). This complication is needed only to deal with interrogation in the intuitionistic case; otherwise an ϵ-base W is perfectly enough.

If B = ⟨W, N⟩ is a base for exponentials on the linear frame M, we say that ⟨M, B⟩ is a full linear frame. In such a case we define for X ⊆ M

?^{B}(X) = ?^{N}(X)
!^{B}(X) = !^{W} (X).

2.19. In view of the validity theorem, we list some properties of a full linear frame ⟨M, B⟩. To save room we use ! and ? instead of !^{B} and ?^{B}. Of course we have still the properties listed in 2.17.

(i) !X ⊆!1 = 1 for every X ⊆ M; (ii) !X ⊗!X = !X. In fact !X ⊗!X ⊆!X ⊗!1 ⊆!X. Conversely if p ∉!X ⊗!X, then there is a y such that !X ·!X ≤ y and p ≰ y. By contradiction let p ∈ !X: then X ∩ W ≰ y i.e. there is a u ∈ X ∩ W with u ≰ y, uu ≤ y. But u ∈!X and !X ·!X ≤ y, thus uu ≤ y. (iii) !(X & Y) ⊆!X ⊗!Y. In fact, assume ∀y(X ∩ Y ∩ W ≤ y → p ≤ y), and let !X ·!Y ≤ a. To prove p ≤ a, let u ∈ X ∩ Y ∩ W. Then X ∩ W ≤ z implies u ≤ z and similarly for Y. Thus uu ≤ a, u ∈ W, hence u ≤ a. Thus X ∩ Y ∩ W ≤ a. Thus p ≤ a, i.e. p ∈!X ⊗!Y. (iv) !X ⊗!Y ⊆!(!X ⊗!Y), (i.e. they are equal). In fact from 2.6, !X ⊗!Y = (X ∩ W) ⊗ (Y ∩ W). So it suffices to show that

(X ∩ W) ⊗ (Y ∩ W) ⊆ (!X ⊗!Y) ∩ W.

If u ∈ X ∩ W, v ∈ Y ∩ W, let g ∈ W, g ∼ uv. Then uv ∈ !X ⊗!Y and g ≤ uv, hence g ∈ (!X ⊗!Y) ∩ W; but uv ≤ g, hence g ∈ (!X ⊗!Y) ∩ W. (vi) If X, Y are closed subsets,

!X ⊗!Y ⊆!(X & Y).

In fact !X ⊗!Y ⊆!X ⊗!1 ⊆!X, i.e. !X ⊗!Y ⊆ X ∩ Y, hence !(!X ⊗!Y) ⊆!(X & Y). We conclude by (v); thus (vi) For X, Y closed !(X ⊗!Y) = !(X & Y).

Remarks. (1) The point in (iii)-(vi) above is that !X ⊗!Y = !Z for some Z. Thus (v) suffices. Hence in the axioms for an ε-base, the requirement of quasi-idempotence is only needed to obtain (ii).

(2) Notice that to prove (i)-(vi), we have only used the fact that W is an ε-base.

(vii) ⊥ = ?⊥ ⊆?X for every X ⊆ M. (ix) !X ⊗?(!X −^{}?Y) ⊆?Y for every X, Y ⊆ M. In fact it is enough to show that

(X ∩ W) ·?(Cl(X ∩ W) −^{}?Y) ⊆?Y.

So let Z = ?(Cl(X ∩W) −^{}?Y), let p ∈ Z and m ∈ X ∩W. We need to prove pm ∈?Y; thus let z ∈ N, Y ≤ z and let us show that pm ≤ z.

By the connection axiom, there is a g ∈ N, such that ĝ = m̂ −^{}ẑ. Thus we want to prove p ≤ g. But p ∈ Z, thus it is enough to show Cl(X ∩ W) −^{}?Y ≤ g. Let then u ∈ Cl(X ∩ W) −^{}?Y, i.e. u · (X ∩ W) ⊆ ?Y. In particular um ∈ ?Y; but z ∈ N, Y ≤ z, hence um ≤ z, i.e. u ∈ m̂ −^{}ẑ. Thus u ≤ g.

3. Reduction, unity and noncommutativity

The foregoing section does of course require a passage to the quotient.

Let ⟨M, ·, e, ≤⟩ be a full linear frame, with B = ⟨W, N⟩ as a base for exponentials. A linear frame has been called reduced (or a RELFfor short) when ≤ is a partial order.

3.1. RELFs are enough in the following sense: for any full linear frame there is a RELF such that the algebras of their closed sets (under operation ⊗, ⊕, −^{}, &, 1,T, 0, ! and ?) are isomorphic (even completely isomorphic as complete lattices, quantales, etc.). When such algebras of closed sets of two frames are isomorphic we will say that the two frames are equivalent.

In fact recall that a ∼ b iff a ≤ b and b ≤ a and set ∂M = M/∼. Let a/∼ be the equivalence class of a under ∼. Define

a/∼ ·b/∼ = (ab)/∼
a/∼ ≤ b/∼ iff a ≤ b
a/∼ ∈ W′ iff a ∈ W
a/∼ ∈ N′ iff a ∈ N
∂B = ⟨W′, N′⟩.

This is sound, the structure ⟨∂M, ·, e/∼, ≤⟩ is a RELF with base of exponentials ∂B and it is routine to check that such a frame is equivalent to M. The isomorphism works as follows: for a closed subset X of M, define ∂X = {p/∼ : p ∈ X}; for Y a closed subset of ∂M, define Y ∂ = {p : p/∼ ∈ Y }. Then one easily sees that

(∂X)∂ = X ∂(Y ∂) = Y

and for the principal closed sets we even have

∂â = â/∼  â/∼∂ = â.

Next one shows that ∂ preserves all the operations and arbitrary intersections of closed sets.

3.2. Notice that when M is a RELF, it is isomorphic with the full linear frame of the principal closed subsets PC(M) = {â : a ∈ M}, under ⊗, 1, ⊆, B^{∗}, where B^{∗} = ⟨{â : a ∈ W }, {â : a ∈ N}⟩.

3.3. If two full linear frames are isomorphic, then their algebras of closed sets are isomorphic (and the principal closed sets correspond too).

3.4. If M is a RELF, then M really lives inside its algebra of closed sets (as a subreduct: identify a ∈ M with â).

3.5. We have avoided (for the sake of generality) to postulate in a linear frame an element 1 such that 1x ∼ x1 ∼ x (or 1x = x1 = x in the RELFcase). But really this gives nothing new; just throw in a 1 and add the relevant properties so that

1 = Cl(1) = ˆ1.

Such a frame will be called unital and its algebra of closed facts is in fact isomorphic to the one of its non unital reduct.

3.6. If we drop the assumption of quasi-commutativity we get a noncommutative linear frame (a g-frame). In this case preservation and continuity have to be doubled while notions defined in terms of the quasi-order do not change. In any other case we have a duplication: two “implications” −^{}and ^{}−, two “negations” ( )^{⊥} and ^{⊥}( ). Nevertheless we insist on just one 1, thus we require

(∗) px ≤ x for all x iff xp ≤ x for all x.

There are in fact a lot of things that have to be fixed properly, but there is no difficulty involved. For instance, the other side of the continuity axiom will take care of showing that ^{⊥}X is always a closed set; in the notion of ε-base we have to take care both of uv and vu and in the connection axiom for a base we have to take care of û ^{}− v̂ as well. We will not go into further details.

4. Matters of freedom and natural noncommutativity

4.1. By a word linear frame over a set S we mean a unital full linear frame of the form

⟨S^{∗}, ∘, e^{∗}, ≤^{∗}, B^{∗}⟩

where S^{∗} is the free monoid over S, ∘ the composition and the axioms for ≤ and B^{∗} are fulfilled (of course the empty word Λ is the unit).

(i) Given any unital g-linear frame M there is a word linear frame M^{∗} over M such that ∂M and ∂M^{∗} are isomorphic (hence their algebras of closed sets are principally isomorphic).

In fact, for k ∈ M^{∗} define πk by induction

πΛ = 1 (1 is the unit of M and Λ the empty word) π(k ∘ ⟨a⟩) = πk · .

Notice that π⟨a⟩ = 1 · a ∼ a and π(k ∘ h) ∼ πk ∘ πk (by quasi-associativity).

Next, if B = ⟨W, N⟩ is the base for exponentials of M, define e^{∗} = ⟨e⟩ and for k, h ∈ M^{∗}

k ≤^{∗} h iff πk ≤ πh
k ∈ W^{∗} iff for some u ∈ W, πk ∼ u
k ∈ N^{∗} iff for some v ∈ N, πk ∼ v

Next we check that

⟨M^{∗}, ·, e^{∗}, ≤^{∗}, B^{∗}⟩

is a unital full linear frame where B^{∗} = ⟨W^{∗}, N^{∗}⟩.

• ≤^{∗} is a quasi-order: trivial.

• ∘ preserves ≤^{∗}: for k, h, l ∈ M^{∗}

k ≤^{∗} h ⇒ πk ≤ πh ⇒ πk · πl ≤ πh · πl, .

But π(k ∘ l) ∼ πk · πl, π(h ∘ l) ∼ πh · πl, thus π(k ∘ l) ≤ π(h ∘ l), i.e. k ∘ l ≤^{∗} h ∘ l (and similarly for l ∘ k).

• ∘ is continuous. Assume a, b, p ∈ M^{∗} and

∀q ∈ M^{∗}(∀z ∈ M^{∗}(a ∘ z ≤^{∗} b → z ≤^{∗} q) → p ≤^{∗} q).

To prove that a ∘ p ≤^{∗} b, we got to show that π(a ∘ p) ≤ πb and it is enough to show that πa · πb ≤ πb.

We will use continuity in M. Given q′ ∈ M assume

∀z′ ∈ M(πa · z′ ≤ πb → z′ ≤ q′);

we want to prove πp ≤ q′. Since q′ ∼ π⟨q⟩, we are assuming

∀z′ ∈ M(πa · z′ ≤ πb → z′ ≤ π⟨q′⟩).

Let z ∈ M^{∗} and πa · πz ≤ πb; then (z′ = πz) we have πz ≤ π⟨q′⟩. Thus

∀z ∈ M^{∗}(πa · πz ≤ pib → πz ≤ π⟨q′⟩).

But πa · πz ∼ π(a ∘ z), thus πa · πz ≤ πb iff a ∘ z ≤^{∗} b, and πz ≤ π⟨q′⟩ iff z ≤^{∗} q′. Thus

∀z ∈ M^{∗}(a ∘ z ≤^{∗} b → z ≤^{∗} ⟨q′⟩).

By the principal assumption, p ≤^{∗} ⟨q′⟩, whence πp ≤ π⟨q′⟩ ∼ q′. For the specular case there is no novelty.

• W^{∗} is an ε-base for M^{∗}. This is routine.

• Since e ∼ g for some g ∈ N, then πe^{∗} = π⟨e⟩ ∼ e ∼ g ∼ π⟨g⟩, whence e^{∗} ∼ ⟨g⟩ ∈ N^{∗}.

• The connection axiom holds (we will show only one half of it). Let k ∈ W^{∗}, h ∈ N^{∗} (of length ≠ 1). Then πk ∼ k′ ∈ W, πh ∼ h′ ∈ N and so there is a g ∈ N such that k′ · g ≤ h′ and

∀x ∈ M(πh · u ≤ πh → u ≤ g).

Now one easily checks that ⟨g⟩ ∈ N^{∗} does the job, namely k ∘ ⟨g⟩ ≤ h and

∀z ∈ M^{∗}(k ∘ z ≤^{∗} h → z ≤^{∗} ⟨g⟩).

The other cases are similar. Now define F from ∂M^{∗} into ∂M by

F (k/∼) = πk/∼ .

Then F is a well-defined bijection and it is in fact an isomorphism from ∂M^{∗} onto ∂M. It is well-defined and one-to-one since

k ∼ h iff πk ∼ πh

and onto since a/∼ = F (⟨a⟩/∼) for a ∈ M. F preserves the structure:

• F (k/∼ ·h/∼) = F ((k ∘ k)/∼) = π(k ∘ h)/∼ = (πk · πh)/∼ = πk/∼ ·πh/∼ = F (k/∼) · F (h/∼).

• k/∼ ≤ h/∼ iff k ≤^{∗} h iff πk ≤ πh iff πh/∼ ≤ πk/∼.

• F (Λ/∼) = πΛ/∼ = 1/ ∼.

• F (e^{∗}/∼) = πe^{∗}/∼ = e/∼.

• k ∈ (W^{∗})′ iff F (k) ∈ W′ and k ∈ (N^{∗})′ iff F (k) ∈ N” are also trivial.

4.2. The g-frame M^{∗} built above may be called the free expansion of M. Observe that if M is a reduced unital g-frame (i.e. ≤ is antisymmetric), then M is isomorphic to ∂M^{∗}.

Moreover if M is a unital g-frame and ⟨M, ·⟩ is a monoid, then in fact M is a quotient of ∂M^{∗}. Just define h Π k iff πh = πk: this is a congruence on M^{∗} and M^{∗}/Π ≈ M.

In conclusion reduced unital word frames are enough to represent all possible algebras of closed sets of g-frames (hence all Girard’s quantales, etc...).

4.3. In case M is a commutative unital linear frame, instead of M^{∗} one will take the set ∫ M of all finite multisets over M.

To be precise a finite multiset over M is defined as a mapping f from M into ω such that supp(f) = {a : f(a) ≠ 0} is finite. Thus ∫ M inherits a rich structure from ω. In particular we have the componentwise operation of multiunion (i.e. sum)

(f + g)(x) = f(x) + g(x)

and the null multiset \overline{0}(x) = 0. The singleton of a ∈ M is [a], defined by [a](x) = δ_{ax} (Kronecker’ delta) and of course ⟨∫ M, +, \overline{0}⟩ is the free commutative monoid, freely generated by its singletons.

Thus the construction of 4.1 transfers to this case; a function π from ∫ M to M can be defined on singletons π[a] = a and extended to ∫ M by freeness etc... The results in 4.1 hold mutatis mutandis.

5. Kripke semantics

5.1. We will consider the propositional language L_{i} with a set of atomic formulas AT = {P_{i} : i ∈ ω} and with the following connectives and constants:

⊕, &, ⊗, −^{}, ( )^{⊥},!,?, ⊥, 1, 0, T. (σ)

If we have also ^{}− and ^{⊥}( ) we get NC − L_{i}, if we have also ⅋ we get L, if we have also ⅋, ^{}− and ^{⊥}( ) we get NC − L. FORM_{i} is the set of formulas of L_{i} (see Appendix A).

Given a full linear frame ⟨M, ·, e, ≤, ⟨W, N⟩⟩ an interpretation (or forcing) on M is a mapping ⊩ from AT into C(M).

FORM_{i} is as usual the absolutely free algebra of signature σ generated by ω generators. Since C(M) is an algebra of that signature, a forcing ⊩ on M will admit a (unique) extension to a homomorphism from FORM_{i} into C(M), still denoted by ⊩.

If we write |A| (or better |A|_{⊩}) for {p ∈ M : p ∈⊩ A} and p ⊩ A for p ∈ |A| we may translate the identities

|A| ∗ |B| = |A ∗ B| (∗ = ⊕, ⊗, −^{}, &)
|A|^{⊥} = |A^{⊥}| ?|A| = |?A| !|A| = |!A|

and the fact that ⊩ preserves the constants into an inductive definition of the forcing relation for all formulas.

We recall that if X ∈ C(M), p ≤ q ∈ X implies p ∈ X and other results from Sec. 2. Thus we get

p ⊩ A ⊗ B  iff p ∈ Cl(|A| · |B|)
p ⊩ A −^{}B  iff ∀q(q ⊩ A → pq ⊩ B)
p ⊩ A^{⊥}  iff ∀q(pq ∈ COMP → q ⊮ A)

(recall that pq ∈ COMP iff pq ≰ e)

p ⊩ A & B  iff p ⊩ A and p ⊩ B
p ⊩ A ⊕ B  iff p ∈ Cl(|A| ∪ |B|)
p ⊩?A  iff p ∈?|A|
p ⊩!A  iff p ∈ Cl(|A| ∩ W)
p ⊩ ⊥  iff p ≤ e
p ⊩ 1  iff px ≤ x for every x ∈ M
p ⊩ T  always
p ⊩ 0  iff p ≤ x for every x ∈ M.

5.2. We will see that this allows a soundness and completeness result for iLL, but no “accessibility” relation is in sight. Thus we now consider S =≤^{c}, namely, for a, b ∈ M

a S b iff a ≰ b.

Observe that for X ⊆ M

Cl^{S}(X) = Cl(X)

where Cl^{S} is defined as in 1.2 and Cl is the usual in the linear frame M.

Given a forcing ⊩ on M sometimes we put “p E A” to mean ∃z(z S p∧z ⊩ A). Using S we easily obtain the following clauses for a forcing ⊩:

(1.)  p ⊩ P, P ∈ AT  iff ∀q(p S q → q E P) (closure)
(2.)  p ⊩ A ⊗ B  iff ∀q(p S q → ∃u, v(uv S q ∧ u ⊩ A ∧ v ⊩ B))
(3.)  p ⊩ A −^{}B  iff ∀q(q ⊩ A → pq ⊩ B)
(4.)  p ⊩ A^{⊥}  iff ∀q(pq S e → q ⊮ A)
(5.)  p ⊩ A & B  iff p ⊩ A and p ⊩ B
(6.)  p ⊩ A ⊕ B  iff ∀q(p S q → ∃v(v S q ∧ (v ⊨ a ∨ v ⊩ B)))
(7.)  p ⊩?A  iff ∀q(p S q ∧ q ∈ N → q E A)
(8.)  p ⊩!A  iff ∀q(p S q → ∃z(z S q ∧ z ∈ W ∧ z ⊩ A))

(9.) \begin{cases}p ⊩ ⊥ iff p S̸ e; p ⊩ 1 iff for no x ∈ M, px S x \\ p ⊩ T always; p ⊩ 0 iff S(p) = ∅. \end{cases}

5.3. Some of the clauses in 5.2 read as follows:

(2.)  p ∈ |A ⊗ B|  iff Sp ⊆ S(|A| · |B|)
(3.)  p ∈ |A −^{}B|  iff p ∈ |A| −^{}|B|
(4.)  p ∈ |A^{⊥}|  iff p ∈ |A| −^{}|⊥|
(6.)  p ∈ |A ⊕ B|  iff Sp ⊆ S(|A| ∪ |B|)
(7.)  p ∈ |?A|  iff N ∩ Sp ⊆ S(|A|)
(8.)  p ∈ |!A|  iff Sq ⊆ S(W ∩ |A|).

Here it appears that −^{}and ( )^{⊥} have a rather asocial behavior. This will be fixed in LL proper.

6. Validity and the soundness theorem for iLL

6.1. A finite sequence of formulas Δ ∈ FORM_{i}^{∗} is short if its length is ≤ 1. Recall that a sequent of L_{i} is an ordered pair (Γ, Δ) of finite sequence of formulas where Δ is short.

(i) Given a full linear frame M, a forcing ⊩ on M and a formula A of L_{i} we say that A is valid in (M, ⊩) iff 1 ⊆ {p ∈ M : p ⊩ A}; A is valid in M iff it is valid in (M, ⊩) for every forcing ⊩ on M; A is valid iff it is valid in all full linear frames.

Note that if M is unital, it is equivalent to say that 1 ⊩ A for A to be valid in (M, ⊩).

(ii) Recall that |A| (or |A|_{⊩}) was defined as {p : p ⊩ A}. We extend | | to FORM_{i}^{∗} (for

a given forcing ⊩) as follows |Λ| = 1 (Λ the empty sequence)

|Γ ∘ ⟨A⟩| = |Γ| ⊗ |A|. We say that a sequent (Γ, Δ) of L_{i} is valid in (M, ⊩) if either Δ = Λ and |Γ|_{⊩} ⊆ ⊥ or else Δ = ⟨A⟩ and |Γ|_{⊩} ⊆ |A|.

Thus a formula A is valid in (M, ⊩) iff the sequent (Λ, A) is valid in (M, ⊩) and a sequent (⟨B⟩, ⟨A⟩) is valid in (M, ⊩) iff |B| ⊆ |A|. Finally the sequent (Λ, Λ) is valid in (M, ⊩) iff 1 ⊆ ⊥. Validity in M and validity tout-court are defined in the obvious way.

(iii) In matters of notation we avoid of course the cumbersome sequence formalism; thus a sequent will be written as everybody does:

A_{1}, …, A_{k} ⊢ A

or as

A_{1}, …, A_{k} ⊢ etc.

This is traditional, but not without dangers. For instances all attempts to define “|A_{1}, …, A_{k}|_{⊩}” in a meaningful way will abort, unless you make again appeal in some way to sequences and their inductive definition. We also use incomprehensible notations like “Γ, A ⊢ B”, because they are too friendly.

6.2. We should now prove that if a sequent Γ ⊢ Δ is provable in iLL, then it is valid. The proof is already contained in Sec. 2 really, but let us consider some cases. Fix any full linear frame M.

\frac{Γ_{1} ⊢ A Γ_{2}, A ⊢ Δ}{Γ_{1}, Γ_{2} ⊢ Δ} (CUT)

We use here commutativity and associativity of ⊗ in C(M): thus |Γ ∘ Γ′| = |Γ| ⊗ |Γ′| for any two sequences of formulas Γ, Γ′. Now if X, Y, Z ∈ C(M) and X ⊆ Y, Y ⊗ Z ⊆ W we get X ⊗ Z ≤ W. (This follows by the compatibility of · with ≤ in M).

\frac{A, Γ ⊢}{Γ ⊢ A^{⊥}}  \frac{Γ ⊢ A}{A^{⊥}, Γ ⊢}

(NEGATION)

The first is valid, because in C(M), X ⊗ Y ⊆ ⊥ iff Y ⊆ X −^{}⊥ = X^{⊥} (2.9, 2.12). For the second if X ⊆ Y in C(M), then X ⊗ Y^{⊥} ⊆ Y ⊗ Y^{⊥} = Y ⊗ (Y −^{}⊥) ⊆ ⊥ (2.8, 2.12). Notice that conversely from X ⊗ Y^{⊥} ⊆ ⊥ we get at most X ⊆ Y^{⊥⊥}.

\frac{A,!Γ ⊢?Δ}{?A,!Γ ⊢?Δ} (6.1)

By 2.18(vi), |!Γ|_{⊩} = !| &(Γ)|, where &( ) is defined by

&(Λ) = 1
&(Γ ∘ ⟨A⟩) = |(&(Γ)) & A|

Then take X = |A|, Y = |Δ|, Z = | &(Γ)|. The assumption is that

X ⊗!Z ⊆ Y

namely

X ⊆!Z −^{}?Y.

Whence

?X ⊆?(!Z −^{}?Y) ⊆!Z −^{}?Y

by 2.18(ix). Hence

?X ⊗!Z ⊆?Y.

7. Completeness theorem for iLL

7.1. Consider the structure

F_{i} = ⟨FORM_{i}, ⊗, ⊥, ≤, ⟨W, N⟩⟩

where A ≤ B means that A ⊢ B is provable in iLL, W = {!A : A ∈ FORM_{i}}, N = {?A : A ∈ FORM_{i}}.

Lemma 1. F_{i} is a unital full linear frame of base ⟨W, N⟩.

In fact first observe that A ∼ B just means that A and B are Lindenbaum-equivalent. Now

1. ≤ is a quasi-order by the axioms and the CUT rule;

2. ⊗ is quasi-associative: trivial;

3. ⊗ is quasi-commutative by the exchange rule;

4. ⊗ preserves ≤. Assume A ⊢ B provable; then of course A ⊗ C ⊢ B ⊗ C is provable as well.

5. ⊗ is continuous. Just remark that

Â −^{}B̂ = (A −^{}B) .

(By 2.5 this implies continuity). In fact C ∈ Â −^{}B̂ means that whenever Q ⊢ A and Z ⊢ C ⊗ Q are provable, then Z ⊢ B is provable. Thus C ⊗ A ⊢ B is provable, whence as usual C ⊢ A −^{}B is provable, i.e. C ∈ (A −^{}B) .

Conversely C ∈ (A −^{}B) means that C ⊢ A −^{}B is provable. Assume then Q ⊢ A and Z ⊢ C ⊗ Q are provable and compute a proof of Z ⊢ B.

6. Of course A ⊗ 1 ∼ 1 ∼ 1 ⊗ A. Observe also that

∀B(A ⊗ B ≤ B) iff A ≤ 1,

thus 1 = {A : A ≤ 1} (see 7.2 below).

7. W is an ε-base. For any formula A, !A ≤ 1 by the weakening rule. Also as usual one shows that

!A ⊗!B ∼!(A & B)
!A ⊗!A ∼!A.

8. There is a G ∈ N such that ⊥ ∼ G. Just take G to be ?⊥.

9. Connection axiom. For A, B formulas, we have to find a solution X ∈ FORM_{i} to

the quasi-equation

(!A −^{}?B) ∼?X.

We claim that one solution is X := !A −^{}?B, i.e. we need to prove

!A −^{}?B ∼?(!A −^{}?B).

Since !A −^{}?B ≤?(!A −^{}?B) is obvious, it suffices to show

!A ⊗?(!A −^{}?B) ≤?B.

In fact !A ⊗ (!A −^{}?B) ≤?B is obvious and so we conclude by the rule on ?.

7.2. Consider now FORM_{i} as an algebra of signature (σ) (absolutely free on AT). We have the mapping ( ) from FORM_{i} into C(F_{i})

Â = {B : B ⊢ A is provable in iLL}.

Lemma 2. ( ) is a homomorphism of signature (σ).

Proof. This is an exercise in iLL. One instance (for −^{}) has been shown above in 7.1(5). Let us consider three more cases: ⊗, ? and the constant 1.

Â ⊗ B̂ = (AB)

holds because of 2.4.

?B̂ = (?B) .

In fact let A ≤ ?B; to prove that A ∈ ?B̂ (see 2.16) let C ∈ N, say C = ?K. Assume B̂ ≤ C (i.e. B ≤ C, by CUT) and show that A ≤ C. In fact

\frac{A ⊢?B \frac{B ⊢?K}{?B ⊢?K}}{A ⊢?K}

Conversely, if A ∈ ?B̂, since ?B ∈ N and B ≤ ?B (thus B̂ ≤ ?B) we have A ≤ ?B (again by 2.16).

ˆ1 = 1.

In fact assume A ≤ 1 and let B any formula:

\frac{A ⊢ 1 \frac{B ⊢ B}{1, B ⊢ B}}{\frac{A, B ⊢ B}{A ⊗ B ⊢ B}}

Conversely if ∀B(A ⊗ B ≤ B), then A ⊗ 1 ≤ 1 an then

\frac{\frac{A ⊢ A  ⊢ 1}{A ⊢ A ⊗ 1}  A ⊗ 1 ⊢ 1}{A ⊢ 1}

Corollary 1. The principal closed sets of C(F_{i}) form a subalgebra of C(F_{i}) that is isomorphic with the Lindenbaum algebra of iLL.

In fact the first sentence follows from the Lemma, and the second from the fact that Â = B̂ iff A ∼ B.

7.3. On the full frame F_{i} of formulas we now define the master forcing by

⊩ (P) = {A : A ⊢ P is provable}
= {A : A ≤ P } = P̂

for P ∈ AT.

As usual this extends uniquely to a morphism from all formulas to C(F_{i}) and, by the previous Lemma, we have ⊩ = ( ) . Namely for any formulas A, B

A ⊩ B iff A ≤ B iff A ⊢ B is provable.

Thus in particular A is valid in (F_{i}, ⊩) iff 1 ⊢ A is provable, iff ⊢ A is provable. Hence the completeness:

Theorem 1. A sequent Γ ⊢ Δ is provable in iLL iff it is valid.

In fact, if for Γ ∈ FORM_{i}^{∗} we define ⊗Γ by: ⊗1 = 1, ⊗(Γ ∘ ⟨A⟩) = (⊗Γ) ⊗ A. If Δ is short define Δ^{0} = A if Δ = ⟨A⟩ and Λ^{0} = ⊥. Then it is routine to check that Γ ⊢ Δ is provable iff ⊢ ⊗Γ −^{}Δ^{0} is provable.

7.4. Using g-frames, there is no big difficulty in extending these results to the intuitionistic linear logic without the exchange rule (see [1]). As far as the free expansion of F_{i} (see Sec. 4) is concerned one will take sequences in the g-case, multisets in the commutative case.

Thus for instance in the g-case,

Γ ≤^{∗} Δ  means  ⊗ Γ ≤ ⊗Δ;

thus if Δ is short

Γ ≤^{∗} Δ  iff  Γ ⊢ Δ is provable in iLL.

Thus the notion of g-frame captures “local” derivability in iLL, while free expansions of g-frames capture usual derivability in iLL (similarly for full linear frames in iLL).

7.5. We might drop completely the element e from linear frames (and from g-frames as well); thus we will also dump the negations ^{⊥}( ) and ( )^{⊥}. This way we get a complete semantic for ILL (see [9]) and one for its noncommutative version as well.

7.6. The popular way to obtain (a version of) linear logic from iLL is to force the element e in a linear frame to be such that for closed sets one has X^{⊥⊥} = X.

This can be achieved by stipulating that the following holds

∀x(px ≤ e → qx ≤ e) → q ≤ p. (∗)

A linear frame ⟨M, ·, e, ≤⟩ satisfying (∗) will be called a web. (We could cover the non commutative case by doubling (∗)).

By a full web we mean a web M together with an ε-base for exponentials W (see 2.17). We here sketch some developments:

(i) If X is a closed set in a web M, then X^{⊥⊥} = X.

In fact let q ∈ X^{⊥} −^{}⊥ and let X ≤ p; we need to show that q ≤ p. By (∗) it will be enough to show:

∀z(pz ≤ e → qz ≤ e)

In fact if pz ≤ e, then xz ≤ e for all x ∈ X, hence z ∈ X^{⊥}, thus qz ≤ e. (ii) For X, Y ∈ C(M), M a web, then

X −^{}Y = (X ⊗ Y^{⊥})^{⊥}
X ⊕ Y = (X^{⊥} & Y^{⊥})^{⊥}
?X = (!(X^{⊥}))^{⊥}.

In fact X −^{}Y ⊆ (X ⊗ Y^{⊥})^{⊥} holds in any linear frame. For the converse by (i) it suffices to show

(X −^{}Y)^{⊥} ⊆ X ⊗ Y^{⊥}.

Thus let p ∈ (X −^{}Y)^{⊥}, X · Y^{⊥} ≤ t and let us show that p ≤ t. Equivalently we show that ∀z(tz ≤ e → pz ≤ e). So let tz ≤ e; it suffices to show that z · X ⊆ Y. But for x ∈ X, xuz ≤ e for all u ∈ Y^{⊥}, thus xz ∈ Y^{⊥}^{⊥} = Y. The rest of the proof is a similar exercise.

In a full web one defines for X, Y closed

X ⅋ Y = (X^{⊥} ⊗ Y^{⊥})^{⊥}

and hence, by the above X ⅋ Y = X^{⊥} −^{}Y = Y^{⊥} −^{}X. (iii) From here on, everything goes smoothly toward a completeness theorem for LL with

regard to the semantic of full webs. We will not bother the reader with details; it is not very rewarding for our aims, since the connective ⅋ is simply defined as above. This gives as it stands no clue at all about its meaning. Anyway notice:

(iv) The clauses of the forcing relation for an interpretation of formulas of L_{i} into the closed sets of a full web M are exactly those of 5.2, where, if you want, you may even omit −^{}, ⊕ and ? (because of the properties of LL on one side and the remarks in (ii) above on the semantic side). Conversely you may like to add a clause for ⅋ which will eventually read as follows (after some elaboration)

p ⊩ A ⅋ Biff ∀q(∀j(qj S e → j ⊮ A) → pq ⊩ B)
iff ∀q(∃j(qj S e ∧ j ⊩ A) ∨ pq ⊩ B).

This is not bad, but it is still not the best we can get: ⅋ will fall on a side with the other asocial guys ( )^{⊥} and −^{}.

7.7. When LL is treated as a strengthening of iLL in the language L_{i} one has to add the rule

\frac{Γ, A^{⊥} ⊢}{Γ ⊢ A}.

Next, if you want a ⅋ you define it by A ⅋ B = A^{⊥} −^{}B. Sequents however keep their limitation to a short right side, thus all this is nothing else than a way to avoid problems (instead of facing them) with the parallel disjunction. Anyway we easily check that the added rule holds in any forcing on any web M: just note that X ⊗ Y^{⊥} ⊆ ⊥ implies X ⊆ Y^{⊥⊥} = Y, i.e. X ⊆ Y for X, Y ∈ C(M).

As for completeness you do as before (see 7.2, 7.3) and you have to check just a few details (everything boils down to the fact that now X^{⊥⊥} = X for X ∈ C(M) and that A^{⊥⊥} ⊢ A is provable in this LL).

7.8. There are reasons not to be very satisfied by this approach to LL:

1. No solution to our curiosity about ⅋.

2. The concocted approach to two sided sequents is really a mess.

3. While for X ⊆ M, M a web, X^{⊥⊥} ⊆ Cl(X), it is not the case that X^{⊥⊥} = Cl(X)

always. Thus there are two closures around. To us the greatest defect is (1). We will stubbornly try again in order to give our mind peace, in Sec. 8.

7.9. In the intuitionistic case, however, the approach based on the slogan <<study the relation “A ⊢ B is provable”>> works fine. Notice, amongst the features of a Kripke semantics, the total modularity of the clauses. If you want to drop (or add) a connective, you just forget about it (or throw it in).

Moreover one can easily obtain (once more) a semantic for Lambek calculus (see [15], [22]). We leave the details to the reader: you have to take now sequences which are really pairs of formulas A ⊢ B (and to adjust the rules). Thus our approach to the semantics is just what you want to do the job.

7.10. We refrain also from going to noncommutative webs, which is a matter of red tape, to obtain a semantic for niLL.

8. Phasoids and LL proper

To get a Kripke semantic for LL proper, we prefer to work with ncLL, the noncommutative (i.e. no-exchange) linear logic [2], because first we succeeded in simplifying the “phase semantic” presented in [2] and also because in this way we cover automatically also cyclic LL and plain LL (as in [6], [28]).

Now ⅋ is in the forefront and we do not allow it to disappear beneath the curtains; in fact the slogan is

“study the relation “⊢ A, B is provable” ”

(In fact we will consider the complement, but this is only a technicality). The basic idea is: take a phase space and define a relation R by

a R b iff ab ∉ ⊥.

It is strange how this triviality may give anything good.

8.1. A phasoid is a structure ⟨M, R, ·, 1⟩ such that for all a, b, c ∈ M,

1. R is quasi-symmetric (see 1.6);

2. · is R-associative, i.e.

R(a · (b · c)) = R((a · b) · c);

3. R(a) = R(1 · a) = R(a · 1);

4. a · b R 1 iff a R b.

A subset W ⊆ M is a base for exponentials if

5. R(1) = R(W); for a ∈ W, R(1) = R(aa) and for a, b ∈ W, R(ab) ⊆ R(W).

6. If a ∈ W there are a′, a′′ ∈ W such that R(a) = R^{⌣}(a′) and R^{⌣}(a) = R(a′′) (relative quasi-symmetry).

A pair ⟨M, W ⟩ where M is a phasoid an W a base for exponentials is called a full phasoid. A phasoid M is cyclic if R is symmetric and commutative if · is commutative. Obviously commutative implies cyclic and cyclic implies that axioms 1. and 6. are useless.

Note that in any phasoid ab R c iff (ab)c R 1 iff a(bc) R 1 iff a R bc. Thus

a R bc iff ab R c (∗)

One can check that (∗) and 3. above already imply 4.; R-associativity will only be needed below to prove that ⊗ is associative on Q-closed sets.

8.2. Given a phasoid M let us define as usual

a ≤ b iff R(b) ⊆ R(a)

(equivalently R^{⌣}(b) ⊆ R^{⌣}(a)) and

a ∼ b  ⟺  a ≤ b and b ≤ a.

It is routine to check that ∼ is a congruence on M. A phasoid M is called reduced if a ∼ b implies a = b; thus the quotient M/∼, denoted by ∂M, is reduced.

In a reduced phasoid, ⟨M, ·, 1⟩ is a monoid and the axioms boil down to

• ab R 1 iff a R b;

• R is quasi symmetric

and for W to be a base

• R(1) = R(W), W is closed under · and W is a set of idempotents.

8.3. By the “duality principle”, from axioms 2.-6. of a phasoid we get true assertions by interchanging R with R^{⌣}. In fact ⟨M, R^{⌣},ˆ ·, 1⟩ is still a phasoid if one defines xˆ ·y to be y · x.

Since R is quasi-symmetric, we have the associated closure operator Q on M (see 1.6): for X ⊆ M

Q(X) = Cl^{R}(X) = Cl^{R^{⌣}}(X) = {x : R(x) ⊆ R(X)}
= {x : R^{⌣}(x) ⊆ R^{⌣}(X)} = X^{R^{⌣}R} = X^{RR^{⌣}}

Let C(M) be the set of the Q-closed subsets of M; from a remark in 1.6 we get that, for X, Y ⊆ M

Q(x) · Q(Y) ⊆ Q(X · Y).

Notice that (writing Qa for Q({a})) we have a ∼ b iff Qa = Qb.

Another basic property of phasoids is that

· is Q-continuous.

Recall that a subbase of the Q-open sets is {R(c) : c ∈ M}; fix a ∈ M and let g_{a}x = ax. Then b ∈ g_{a}^{−1}(R(c)) means that ab R c. Take z = ca and use (∗) in 8.1 to prove that

b ∈ R(z) and g_{a}[R(z)] ⊆ R(c).

Thus we have a sort of “uniform continuity”.

8.4. Besides the usual operation X · Y and the residuations X −^{}Y and X ^{}− Y, in P(M) we also define a pair of proto-PARs, namely

X ⅋_{1} Y = {x : for all u, v, if u · v R x then u ∈ R^{⌣}(Y) or v ∈ R^{⌣}(X)}
X ⅋_{2} Y = {x : for all u, v, if x R u · v then u ∈ R(Y) or v ∈ R(X)}

We have that, for all X, Y ⊆ M

(i) X ⅋_{1} Y and X ⅋_{2} Y are Q-closed; (ii) if X, Y are Q-closed then

1. X −^{}Y = X^{R^{⌣}} ⅋_{1} Y,

2. Y ^{}− X = Y ⅋_{2} X^{R},

3. X ^{}− Y^{R^{⌣}} = X^{R} −^{}Y,

4. X ⅋_{1} Y = X ⅋_{2} Y.

(i) is immediate. For 1. the following are equivalent:

u ∈ X −^{}Y

for all x: (x · u ∉ Y) ⟹ (x ∉ X)

for all x: (x · u ∈ R(Y^{R})) ⟹ (x ∈ R^{⌣}(X^{R^{⌣}}))

for all x, y: (y ∉ R^{⌣}(Y) and y R x · u) ⟹ (x ∈ R^{⌣}(X^{R^{⌣}})) for all x, y: (y · x R u) ⟹ (x ∈ R^{⌣}(X^{R^{⌣}})) or (y ∈ R^{⌣}(Y)) u ∈ X^{R^{⌣}} ⅋_{1} Y.

2. is similar.

3. Let x ∈ X ^{}− Y^{R^{⌣}}. Let u ∈ X^{R}, {x} · Y^{R} ⊆ X: to show that u · x ∈ Y it suffices to show that R(u · x) ⊆ R(Y). Let u · x R t; then u R x · t, hence x · t ∉ X, t ∉ Y^{R^{⌣}}, hence t ∈ R(Y). Conversely, let x ∈ X^{R} −^{}Y, v ∈ Y^{R^{⌣}}, X^{R} · {x} ⊆ Y.

It is enough to show that R^{⌣}(x · v) ⊆ R^{⌣}(X): let t R x · v, hence t · x R v, t · x ∉ Y, t ∉ X^{R} and finally t ∈ R^{⌣}(X).

4. First observe that from 1. and 2. we get

5. X^{R} −^{}Y = X ⅋_{1} Y;

6. X ^{}− Y^{R^{⌣}} = X ⅋_{2} Y (Since (X^{R})^{R^{⌣}} = X and X^{R} is a fact, etc..) Now by 3. we get 4.

So we have a “parallel” reading for the PAR operation, defined of course on Q-closed sets by

X ⅋ Y = X ⅋_{1} Y = X ⅋_{2} Y

The structure of Q-closed sets is completed as expected by:

X ⊗ Y = Q(X · Y)
X ⊕ Y = Q(X ∪ Y)
X^{⊥} = X^{R^{⌣}}
⊥X = X^{R}
X & Y = X ∩ Y
⊥ = M ∖ R(1) = {1}^{R} = {1}^{R^{⌣}} = 1^{⊥} = ^{⊥}1
1 = Q(1) = ⊥ −^{}⊥ = ⊥ ^{}− ⊥
0 = Q(∅) = {x : R(x) = ∅} = {x : R^{⌣}(x) = ∅}
T = M = ∅^{R} = ∅^{R^{⌣}} = 0^{⊥} = ^{⊥}0

(iii) For X ⊆ M, X^{⊥} = X −^{}⊥, ^{⊥}X = ⊥ ^{}− X and

Q(X) = X ⅋_{1} ⊥ = ⊥ ⅋_{1} X.

Also

Q(X) ⊗ Q(Y) = Q(X · Y).

(iv) (De Morgan laws) If X, Y are Q-closed sets

X ⅋ Y = ^{⊥}(Y^{⊥} ⊗ X^{⊥}) = (^{⊥}Y ⊗^{⊥}X)^{⊥}
X ⊗ Y = ^{⊥}(Y^{⊥} ⅋ X^{⊥}) = (^{⊥}Y ⅋ ^{⊥}X)^{⊥}

and similarly for ⊕, ⅋.

(v) Since ^{⊥}X = ^{⊥}Q(X) and X^{⊥} = Q(X)^{⊥} we have R(X) = R(Q(X)). Also

R(Q(X) · Q(Y)) = R(Q(X) ⊗ Q(Y)) = R(Q(X · Y)) = R(X · Y).

In particular, by R-associativity of ·, we get that ⊗ (hence ⅋) is associative on closed sets.

8.5. In particular, in a phasoid

Qa ⊗ Qb = Q(a · b),

thus the set PC(M) = {Qa : a ∈ M} of principal Q-closed sets becomes a phasoid ⟨PC(M), R′, ⊗, 1⟩, where 1 = Q(1) and Qa R′ Qb iff a R b (i.e. iff Qb ∩ R(Qa) ≠ ∅). Easily we get that the phasoid PC(M) is isomorphic with ∂M (see 8.1).

Let C(M) be the algebra of Q-closed sets of the phasoid M (with operations of signature L_{nc}).

(i) C(M) and ∂M are isomorphic via the map sending F ∈ C(M) to {p/∼ : p ∈ F }. The principal closed sets correspond as well and the isomorphism preserves even the structure of complete lattice.

(ii) If two phasoids are isomorphic, then so are their algebras of closed sets. (iii) Thus if M is a reduced phasoid, C(M) ≅ C(PC(M)), hence M is (isomorphic with)

a subreduct of C(M).

8.6. A ∗-phasoid is a structure ⟨H, ≤, ·, 1, ( )^{⊥}, ( )^{⊥}⟩, where ⟨H, ·, 1⟩ is a monoid, ≤ a partial order an the following hold for any a, b, c ∈ M:

1. a = ^{⊥}(a^{⊥}) = (^{⊥}a)^{⊥};

2. b · c ≤ a iff a · b ≤ c^{⊥}. A ∗-quantale is a ∗-phasoid in which ≤ induces the structure of a complete lattice and moreover

3. x · sup_{i∈I}z_{i} · y = sup_{i∈I}(x · z_{i} · y).

(i) One easily shows that in a ∗-phasoid, • b ≤ a^{⊥} iff a ≤ ^{⊥}b iff ab ≤ 1^{⊥} = ^{⊥}1 (thus set ⊥ = ^{⊥}1 = 1^{⊥});

• a ≤ b iff ^{⊥}b ≤ ^{⊥}a iff b^{⊥} ≤ a^{⊥};

• bc ≤ a^{⊥} iff c ≤ (ab)^{⊥};

• · is compatible with ≤.

• ^{⊥}(bc)b ≤ ^{⊥}c and b(ab)^{⊥} ≤ a^{⊥}.

Given a ∗-phasoid put

a R^{∗} b iff b ≰ a^{⊥}.

Then H^{∗} = ⟨H, R^{∗}, ·, 1⟩ is a reduced phasoid. (ii) Conversely, if M is any phasoid, then

⟨C(M), ⊆, ⊗, 1, ( )^{⊥},^{⊥}( )⟩

is a ∗-quantale. (iii) A representation theorem holds: if H is a ∗-quantale, then H is isomorphic with

C(H^{∗}) (as a ∗-phasoid).

In fact, for X ⊆ H, if a_{X} = supX, then

X^{⊥} = {y : y ≤ (a_{X})^{⊥}}.

Hence if X ∈ C(H), then X = â_{X} = Q(a_{X}) (where the Q-closure is performed in C(H)). In fact a_{X} ∈ X, otherwise R(a_{X}) ⊈ R(X), thus for some y, a R y ∉ R(X), hence y ∈ X^{⊥}, i.e. both y ≰ (a_{X})^{⊥} and y ≤ (a_{X})^{⊥}. Also X ∈ C(H) implies X ⊆ â_{X}. Conversely, if y ∈ X, i.e. R(y) ⊆ R(X), then

∀z ∈ H(∀h ∈ X(z ≤ h^{⊥} → z ≤ y^{⊥})).

But h ≤ a_{X} for h ∈ X, therefore (a_{X})^{⊥} ≤ y^{⊥}, i.e. y ≤ a_{X}; thus C(H) = PC(H). Finally the mapping a ⟼ â is an isomorphism from H into C(H), which is onto by the above remark.

Recall that a quantale (not necessarily commutative) is a monoid ⟨H, ≤, ·, 1⟩ such that ≤ induces a complete lattice and axiom 3. holds. Thus ∗-quantales are quantales (suited for ncLL).

In particular we have that the full theory of quantales is at our disposal. Recall in particular the definitions for residuations

a −^{}b = sup(x : ax ≤ b)
a ^{}− b = sup(x : xb ≤ a)

and the PAR operation

a ⅋ b = ^{⊥}(b^{⊥} · a^{⊥}).

Of course the isomorphism a ⟼ â preserves these operations and thus ⅋ is associative, ⊥ ⅋ a = a = a ⅋ ⊥ and various identities hold:

(sup_{i∈I}b_{i})^{⊥} = inf_{i∈I}(b_{i})^{⊥} and dually;
a ⅋ inf_{i∈I} ⅋ b = inf_{i∈I}(a ⅋ b_{i} ⅋ b).

Moreover sup_{i∈I}a_{i} R^{∗} sup_{j∈I} iff ∃i, j with a_{i} R^{∗} b_{j}.

8.7. Let ⟨K, ≤⟩ be a poset, R ⊆ K × K; we say that R is continuous w.r. to ≤ if whenever Y, Z ⊆ K and supY, supZ exists then

supY R supZ iff ∃y ∈ Y, z ∈ Z s.t. y R z.

By a prequantale we mean a quantale without the assumption of associativity for ·.

Let R be a binary relation in a prequantale ⟨K, ≤, ·, 1⟩; set ⊥ = sup(x : 1 R̸ x). Then the following are equivalent: R1 ∀a, b ∈ K, a R̸ b iff ab ≤ ⊥. R2 i. R is continuous;

ii. ∀a, b ∈ K, a R b iff ab R 1 iff 1 R ab;

iii. ∀a, b, c ∈ K, a R b ≤ c implies a R c.

R3 i. 1 R̸ ⊥;

ii. iii. as in R2. The proof is routine. Only notice that from R1 we get in turn

a. 1 R̸ b iff b ≤ ⊥ iff b R̸ 1 (hence 1 R̸ ⊥).

b. If 1 R a ≤ b then 1 R b.

c. a R b iff 1 R ab.

d. ⊥ = sup(x : x R̸ 1).

e. If a R b ≤ c then a R c; if a R c and a ≤ b, then b R c. Thus to prove R2 we have to check continuity. In fact a ∉ R^{⌣}(Y) iff 1 R̸ ay for all y ∈ Y iff 1 R̸ sup({a} · Y) = a · supY iff a R̸ supY. Thus R^{⌣}(Y) = R^{⌣}(supY) etc.

Hence ∗-quantales can be presented as quantales with a relation R which is extensional (Ra = Rb → a = b) and satisfies R1 (an R-quantale).

8.8. Conversely if ⟨K, R⟩ is an R-quantale, then K becomes a ∗-quantale in which R^{∗} = R and

a^{⊥} = sup(x : a R̸ x)
⊥a = sup(x : x R̸ a).

In fact 1. a R̸ a^{⊥} and ^{⊥}a R̸ a ( because aa^{⊥} ≤ ⊥ and 1 R̸ ⊥).

2. a R̸ b iff b ≤ a^{⊥} iff a ≤ ^{⊥}b iff ab ≤ ⊥.

3. a ≤ b iff Ra ⊆ Rb.

If Ra ⊆ Rb then Rb = Ra ∪ Rb = R(a ∨ b) (where ∨ is the join in H); by extensionality we get b = a ∨ b, hence a ≤ b.

4. a^{⊥} ≤ b^{⊥} iff b ≤ a iff ^{⊥}a ≤ ^{⊥}b.

5. a = ^{⊥}(a^{⊥}) = (^{⊥}a)^{⊥}.

Now ^{⊥}(a^{⊥}) = sup(y : y a̸^{⊥}); by 2. y R̸ a^{⊥} iff a^{⊥} ≤ y^{⊥} iff y ≤ a. Thus ⊥(a^{⊥}) = sup(y : y ≤ a) = a.

6. bc ≤ a^{⊥} iff ab ≤ ^{⊥}c.

(Here we use associativity!) bc ≤ a^{⊥} iff a R̸ bc iff abc R̸ 1 iff ab R̸ c iff ab ≤ ^{⊥}c. A noteworthy corollary is that if ⟨K, R⟩ is an R-quantale, then R is quasi-symmetric

and so ⟨K, R, ·, 1⟩ is a reduced phasoid.

Remark. It is easy to show that in fact all R-quantales are reduction of quantales endowed with a quasi-symmetric relation enjoying R1.

8.9. We finish by showing that phase spaces are nothing but phasoids in disguise (and conversely): this is trivial for the commutative and cyclic cases.

For the noncommutative case recall the main notion from [2]: a seed is a monoid ⟨M, ·, 1⟩ with a subset ⊥ which is suitable i.e.^{1}

(^{⊥⊥}{z})^{⊥} ⊆ ^{⊥}{z} and ^{⊥}({z}^{⊥⊥}) ⊆ {z}^{⊥}

for all z ∈ M. Here of course one has the usual residuations −^{}and ^{}− for monoids and X^{⊥} = X −^{}⊥, ^{⊥}X = ⊥ ^{}− X.

The facts are the subsets of M such that X = ^{⊥}(X^{⊥}) = (^{⊥}X)^{⊥}; the map K(X) = ⊥(X^{⊥}) is a closure operator and operations are in fact defined in the obvious way. Thus we get an algebra of facts F(M) of signature L_{nc}. Now it is not difficult to see that phasoids and seeds are semantically equivalent.

1The author should admit that the desire to simplify that bad looking axiom was also a trigger to his research.

(i) For any phasoid ⟨M, R, ·, 1⟩ there is a seed ⟨M′, ·, 1, ⊥⟩ such that

C(M) ≈ F(M′)

as algebras with the usual operations. (ii) For any seed ⟨M, ·, 1, ⊥⟩, by defining x R y iff xy ∉ ⊥, we get a (reduced) phasoid

⟨M, R, ·, 1⟩ such that for every X ⊆ M, (X^{R})^{R^{⌣}} = ^{⊥}(X^{⊥}). Thus the algebra of closed sets in the phasoid coincides with the phase space over the seed.

For the proof of (i), we may assume that the phasoid ⟨M, R, ·, 1⟩ is reduced; then define ⊥ = M ∖ R(1). This is a suitable subset, thus ⟨M, ·, 1, ⊥⟩ is a seed and the algebra of closed set in the phasoid coincides with the phase space over the seed (we leave the painful checking to the reader).

The proof of (ii) is also routine; notice that ⊥ is cyclic (i.e. xy ∈ ⊥ iff yx ∈ ⊥) iff R is symmetric. This has some interest in that it should allow us to use the completeness theorem proved in [2] for ncLL (i.e. without exponentials) and hence to avoid a good amount of redtape.

8.10. To deal with exponentials we use a full phasoid ⟨M, W ⟩; we define for X ⊆ M

p ∈?X iff Rp ∩ W ⊆ R(X)
!X = Q(Q(X) ∩ W).

We have

(i) For any X ⊆ M 1. P ∈?X iff R^{⌣}p ∩ W ⊆ R^{⌣}(X);

2. ?X = ^{⊥}(W ∩ X^{⊥}) = (W ∩^{⊥}X)^{⊥};

3. ?X is always a Q-closed subset of M and ?X = ?Q(X);

4. if X is a Q-closed subset of M then

⊥(?(X^{⊥})) = (?(^{⊥}X))^{⊥}.

To prove 1. let us show that

Rp ∩ W ⊆ R(X) iff R^{⌣}p ∩ W ⊆ R^{⌣}(X) (∗)

Assume R^{⌣}p ∩ W ⊆ R^{⌣}(X) and let p R z for some z ∈ W; pick z′′ ∈ W such that R^{⌣}z = Rz′′. Then z′′ R p hence z′′ ∈ R^{⌣}(X), namely z′′ R x for some x ∈ X. Now x R z, i.e. z ∈ R(X). The converse is similar.

2. follows from (∗) above:

p ∈?X iff Rp ∩ (W ∩ X^{⊥}) = ∅
iff R^{⌣}p ∩ (W ∩^{⊥}X) = ∅.

3. follows from 2. (recall that X^{⊥} = (Q(X))^{⊥}).

4. Let p ∈ ^{⊥}(?(X^{⊥})); then Rp ∩?(X^{⊥}) = ∅, namely if p R u, then there is a g ∈ W such that r R u and g ∉ R^{⌣}(X^{⊥}). But R^{⌣}(X^{⊥}) = M ∖^{⊥}X^{⊥}, i.e. g ∈ X, if X is a Q-closed subset.

To show that R^{⌣}p ∩?(^{⊥}X) = ∅, let v R p. Take u such that Rv = R^{⌣}u. Then p R u and therefore there is a g ∈ W ∩ X such that g R u. Then v R g, g ∈ X hence g ∈ ^{⊥}X^{⊥}, i.e. g ∉ R(^{⊥}X). Thus Rv ∩ W ⊈ R(^{⊥}X), namely v ∉?(^{⊥}X). The converse is proved by duality.

(ii) Let X, Y ⊆ M where ⟨M, R, ·, 1, W ⟩ is a full phasoid. Then 1. X ⊆?X;

2. ⊥ ⊆?X and if X ⊆ Y then ?X ⊆?Y;

3. ?⊥ = ⊥;

4. ?X ⅋?X = ?X;

5. ?X ⅋?Y ⊆?(X ⊕ Y);

6. ??X = ?X;

7. X^{⊥} ∩ W ⊆ (?X)^{⊥} ∩ W and ^{⊥}X ∩ W ⊆ ^{⊥}(?X) ∩ W;

8. ?(?X ⅋?Y) ⊆?X ⅋?Y;

9. ?(X ⊕ Y) = ?X ⅋?Y;

1. holds by 4.1(ii): ?X = ^{⊥}(W ∩ X^{⊥}) ⊇ Q(X) ⊇ X.

For 2., if p ∈ ⊥, then p R̸ 1, then p R̸ d for any d ∈ W; hence Rp ∩ W = ∅. Therefore p ∈?X for any X.

3. is proved by absurd. Let p ∈?⊥ and p ∉ ⊥, i.e. p R 1. Then p R x for some x ∈ W, hence R^{⌣}x ⊆ R^{⌣}1 and x ∈ R(⊥), i.e. q R x for some q ∈ ⊥. Then q R 1 and q R̸ 1.

For 4. let p ∈ ?X ⅋ ?X. If p R d, d ∈ W, then also p R dd; by the definition of ⅋, one gets d ∈ R(?X), hence there is a u ∈ ?X such that u R d. But Ru ∩ W ⊆ R(X), hence d ∈ R(X). Thus p ∈?X.

For the converse use 2. and 4.1(iii):

?X = ?X ⅋ ⊥ ⊆ X ⅋?X.

To see 5. notice that R(X ∪ Y) = R(X ⊕ Y). Let p ∈ ?X ⅋ ?Y and p R d for d ∈ W. Then p R dd, hence d ∈ R(?X) or d ∈ R(?Y), hence, as in 4., d ∈ R(X) or d ∈ R(Y), i.e. d ∈ R(X ⊕ Y).

To see 6. note that R(?X) ∩ W ⊆ R(X). If p ∈ ??X, then Rp ∩ W ⊆ R(?X), hence Rp ∩ W ⊆ R(?X) ∩ W ⊆ R(X). Hence p ∈?X.

For 7., if p ∈ X^{⊥} ∩ W, then p ∈ W and p ∉ R(X). If d ∈ R^{⌣}p ∩?X, then d R p and Rd ∩ W ⊆ R(X). But p ∈ Rd ∩ W and hence a contradiction. So R^{⌣}p ∩?X = ∅, i.e. p ∈ (?X)^{⊥}.

To see 8. assume p ∉ ?X ⅋ ?Y. Then there are u, v such that p R uv and R^{⌣}u ∩?Y = ∅ = R^{⌣}v ∩?X. Since pu R v we get pu ∉?X; hence there is t′ ∈ W such that pu R t′ and t′ ∉ R(X), i.e. t′ ∈ X^{⊥}.

Pick t ∈ W such that Rt = R^{⌣}t′. Then Rt ∩ X = ∅, hence t ∈ ^{⊥}X ∩ W and by 7. t ∈ ^{⊥}(?X) ∩ W. Since pu R t′, we get t R pu i.e. tp R u. Since R^{⌣}u ∩?Y = ∅, tp ∉ ?Y. Hence there is s ∈ W, s R tp and s ∉ R^{⌣}(Y): namely st R p and a ∈ ^{⊥}T ∩ W, hence a ∈ ^{⊥}(?Y) ∩ W.

Let w ∈ W such that R(st) = R(w). We have st R p, hence w R p. Moreover st ∈ ⊥(?Y) ⊗^{⊥}(?X), hence R(st) ⊆ R(^{⊥}(?Y) ·^{⊥}(?X)), hence Rw ⊆ R(^{⊥}(?Y) ·^{⊥}(?X)), hence w ∈ ^{⊥}(?Y) ·^{⊥}(?X)). Therefore

R^{⌣}p ∩ W ∩ (^{⊥}(?Y) ⊗^{⊥}(?X)) ≠ ∅,

namely

R^{⌣}p ∩ W ∩^{⊥}(?X ⅋?Y) ≠ ∅

namely

R^{⌣}p ∩ W ⊈ R^{⌣}(?X ⅋?Y)

i.e.

p ∉?(?X ⅋?Y).

One inclusion in 9. is obtained by 6. On the other side, because of 1. and 2.

X ⊆?X = ?X ⅋ ⊥ ⊆?X ⅋?Y

and

Y ⊆?Y = ⊥ ⅋?Y ⊆?X ⅋?Y,

Hence X ∪ Y ⊆?X ⅋?Y and so X ⊕ Y ⊆?X ⅋?Y. Therefore, by 8.

?(X ⊕ Y) ⊆?(?X ⅋?Y) ⊆?X ⅋?Y.

(iii) Note that in any phasoid M, if X ⊆ M then p ∈ ^{⊥}X iff X ⊆ {p}^{⊥} and then

X^{⊥} = ⋂{{p}^{⊥} : p ∈ X}.

Therefore 4.1(ii) gives

?X = ⋂{{p}^{⊥}; p ∈ W, X ⊆ {p}^{⊥}}
= ⋂{^{⊥}{p} : p ∈ W, X ⊆ ^{⊥}{p}}.

(iv) If F is a Q-closed subset of a full phasoid ⟨M, W ⟩ then

!F = ^{⊥}(?(F^{⊥})) = (?^{⊥}F)^{⊥}.

For the proof, use 4.1(iv) and observe that

p ∈?(F^{⊥}) iff p ∈ (W ∩ F)^{⊥}.

From 4.4 and 4.2 one will then obtain a number of properties of ! on Q-closed subsets; for instance !(F & G) = !F ⊗!G.

(v) Next we give a look at the reduction procedure. Let ⟨M, R, ·, 1, W ⟩ be a full phasoid; in the reduced phasoid ∂M (see Sec. 2) we define ∂W by

a/∼ ∈ ∂W iff a ∈ W.

The fact that ∂W is a base for exponentials in ∂M is totally routine. The full phasoid ⟨M/∼, R, ·, 1′, ∂W ⟩ will be called the reduction of M and will be denoted by ∂M (of course 1′ = 1/∼).

Thus we get easily: the full algebras of facts on M and ∂M are isomorphic.

8.11. (At least for the commutative case) a recent idea of J.-Y. Girard [8] will simplify the treatment of exponentials. This will work as follows in the present context.

Assume that ⟨M, R, ·, 1⟩ is a commutative phasoid. By gib(M) we mean

{z ∈ M : z = z · z and R(1) ⊆ R(z)}.

This is a base for exponentials (the canonical base). Notice that if z_{1}, z_{2} ∈ gib(M) then also z_{1} · z_{2} ∈ gib(M) (because of commutativity). The semantic of commutative phasoids (with their canonical bases) is complete for LL (with exponentials).

8.12. Phasoids ≡ webs. A final remark to shed some light on the equivalence of the notions of phasoid (8.1) and webs (7.6) from the point of view of their algebras of closed sets. Since webs were mainly studied in the quasi-commutative case, we will refer here to commutative phasoids. (A) Given a phasoid M consider the structure

M^{∞} = {C(M), ≤, ⅋, 1}

where X ≤ Y means Y ⊆ X. M^{∞} is in fact a web.

Let us check continuity; for X, Y, Z closed, remembering that X ⅋ Y = (X^{⊥} ⊗ Y^{⊥})^{⊥}, we have to show that if

∀Q(∀Z(Z ⊗ X ⊆ Y → Z ⊆ Q) → F ⊆ Q)

then X ⊗ F ⊆ Y. This is trivial, since X ⊗ Z ⊆ Y iff Z ⊆ X ^{}− Y etc.

Now C(M^{∞}), the algebra of closed sets of this web, is not as monstrous as it may appear; as a matter of fact

C(M^{∞}) ≈ C(M).

In fact, if H ⊆ C(M) and Cl^{∞} is the closure operator on M^{∞}, then Cl^{∞}(H) = {Z : ⋂ H ⊆ Z} = {Z : Z ≤ ⋂ H}. Namely, the closed sets in C(M^{∞}) are the principal closed sets, i.e. C(M^{∞}) = PC(M^{∞}).

Then the mapping which takes X ∈ C(M) into X = {Z ∈ C(M) : X ⊆ Z} is an isomorphism: just check that it preserves ⊗, ( )^{⊥}, ⊥, 0, since the other operations are defined equationally.

For instance (X^{⊥}) = {Z : X^{⊥} ⊇ Z}. But ⊥_{∞} = {Z : Z ⊇ 1}, so if Z ∈ (X )^{⊥}, then Z ⅋ Y ∈ ⊥_{∞} for every Y ∈ X . In particular Z ⅋ X ⊇ 1, i.e. Z^{⊥} ⊗ X^{⊥} ⊆ ⊥, then Z^{⊥} ⊆ X^{⊥⊥} = X and Z ⊃ X^{⊥}, i.e. Z ∈ (X^{⊥}) . The rest is similarly obvious.

(B) Given a web ⟨M, ·, e, ≤⟩ we get a phasoid ^{0}M such that the full algebras of closed sets of M and ^{0}M are isomorphic. Consider

0M = ⟨C(M), ⅋, ⊥, R⟩

where X R Y means 1 ⊈ X ⅋ Y. It is easy to check that it is a phasoid. Next the closure operator Q in ^{0}M associates to H ⊆ C(M) the set

Q(H) = {Z : R(Z) ⊆ R(H)}
= {Z : ⋂ H ⊆ Z}.

Thus H is a Q-closed subset of ^{0}M iff ⋂ H ⊆ Z → Z ∈ H, i.e. H = (⋂ H) , the principal Q closed subset generated by ⋂ H. The closed sets in F(^{0}M) are exactly the principal closed subsets and thus, similarly to the above, the mapping sending X ∈ C(M) into X is an isomorphism.

Remarks. 1. This “tour de force” could have been avoided by assuming in the basic notion of linear frame some more axioms, leading to the fact that â ^{}− b̂ be equal to some ĝ. But this again would draw us back, too close to the logical syntax.

2. This theory could be framed inside the theory of ∗-phasoids and ∗-quantales, if one wishes to do so (we leave the details to the reader).

3. In the noncommutative case things are more or less the same, there are only more detours to follow.

9. Kripke semantics for ncLL. Completeness

9.1. Things are now ready for defining a forcing for formulas of L_{nc}; it is a mapping ⊩ from the set AT of atomic formulas into C(M) where ⟨M, W ⟩ is any full phasoid. It will extend uniquely to the set FORM of all formulas of L_{nc}, as usual, and the clauses are as follows:

p ⊩ A^{⊥} iff ∀y(p R y → y ⊮ A)
p ⊩ ^{⊥}A iff ∀y(y R p → y ⊮ A)
p ⊩ A ⊗ B  iff ∀y(p R y → ∃u, v(vu R y ∧ u ⊩ A ∧ v ⊩ B))
p ⊩ A ⅋ B  iff ∀x, y(p R xy → ∃u((u R x ∧ u ⊩ A) ∨ ∃v(v R y ∧ v ⊩ B)))
p ⊩ A ⊕ B  iff ∀x(p R x → ∃y(y R x ∧ (y ⊩ A ∨ y ⊩ B)))
p ⊩ A & B  iff p ⊩ A ∧ p ⊩ B
p ⊩?A iff ∀x((p R x ∧ x ∈ W) → ∃y(y R x ∧ y ⊩ A))
p ⊩!A iff ∀x(p R x → ∃y(y ⊩ A ∧ y ∈ W ∧ y R x))
p ⊩ ⊥ iff p R̸ 1
p ⊩ 0 iff Rp = ∅
p ⊩ 1 iff Rp ⊆ R1
p ⊩ T iff always.

Remark. In the cyclic case (i.e. R symmetric) p ⊩ A^{⊥} iff p ⊩ ^{⊥}A as it has to be. This holds a fortiori in the commutative case. We were just forgetting about implications:

p ⊩ A −^{}B  iff ∀x(x ⊩ A → xp ⊩ B)
p ⊩ A ^{}− B  iff ∀x(x ⊩ B → px ⊩ A)

9.2. In the assignment of the set |P | = {a : a ⊩ P } to any atomic formula P (notice that this set is just {P }^{⊥}), these clauses are the translation of the usual definition of interpretation into a phase space (see 8.9). Thus for the fragment without exponentials we already have a soundness and completeness theorem ([2]). A more direct proof of completeness is sketched below (for the full system, including exponentials).

As to soundness (by the way, as expected, A is valid in ⟨M, ⊩⟩ whenever 1 ⊩ A; a sequent Γ ⊢ Δ is valid in ⟨M, ⊩⟩ iff | ⊗ Γ| ⊆ | ⅋ Δ|) this is obtained by appealing to the relevant properties presented in 8.3, 8.4, 8.5, 8.6 and 8.10.

9.3. We will now show that ncLL proves every sequent Γ ⊢ Δ which is valid in all full phasoids.

Consider the following structure:

⟨FORM, ⅋, ⊥, R, W ⟩

where FORM is the set of all formulas of L_{nc}, W = {?A : A ∈ FORM} and A R B iff ⊢ A, B is not provable.

First we check that it is a phasoid. In fact ⊢ A, B is provable iff ⊢ B^{⊥⊥}, A is provable, thus B ∈ R(A) iff A ∈ R(B^{⊥⊥}). Similarly ⊢ A, B is provable iff ⊢ B,^{⊥⊥}A is provable. Hence R is quasi-symmetric.

That ⅋ is R-associative is trivial. Also ⊢ A, B is provable iff ⊢ A ⅋ B, ⊥ is provable. Finally W is a base for exponentials: in fact ⊢ 1, A is provable iff ⊢ A is provable. But ⊢!1 is provable, thus if 1 R A then ?⊥ R A. Also ?A R B implies ⊥ R B because from ⊢ ⊥, B we get ⊢ B and ⊢?A, B.

For the other properties, recall that ⊢?A ⅋?A, B is provable iff ⊢?A, B is provable; that ⊢?A ⅋?B, C is provable iff ⊢?(B ⊕A), C is provable and that ⊢?A, C is provable iff ⊢ C,?(^{⊥⊥}A) is provable....

Next define, for P atomic and C ∈ FORM

C ⊩ P  iff  ⊢ C, P is provable.

First observe that |P | is a Q-closed set for P atomic (because |P | = {P }^{R}). Then observe that

C ⊩ A iff ⊢ C, A.

This is proved by induction on the complexity of A and implies completeness. For brevity’s sake we will write ⊢ A, B for “⊢ A, B is provable”.

(1)  C ⊩ A^{⊥} iff ∀B(C R B → B ⊮ A)
iff ∀B(⊢ B, A →⊢ C, B)
iff ⊢ C, A^{⊥}

(2)  C ⊩ A^{⊥} iff ∀B(B R C → B ⊮ A)
iff ∀B(⊢ B, A →⊢ B, C)

Thus assume C ⊩ ^{⊥}A and take B = A^{⊥}. We get

\frac{A ⊢ ^{⊥}(A^{⊥}) \frac{⊢ A^{⊥}, C}{^{⊥}(A^{⊥}) ⊢ C}}{\frac{A ⊢ C}{⊢ C,^{⊥}A}}

Assume ⊢ C,^{⊥}A and compute

\frac{A ⊢ (^{⊥}A)^{⊥}  \frac{⊢ C,^{⊥}A}{(^{⊥}A)^{⊥} ⊢ C}}{A ⊢ C}  \frac{⊢ B, A}{^{⊥}B ⊢ A}

\frac{\frac{^{⊥}B ⊢ C}{⊢ (^{⊥}B)^{⊥}, C} (^{⊥}B)^{⊥} ⊢ B}{⊢ B, C}

(3) C ⊩ A ⊗ B  iff  ∀X(C R X → ∃U, V (V ⅋ U R X ∧ U ⊩ A ∧ V ⊩ B))

iff ∀X(∀U, V (⊢ U, A∧ ⊢ V, B →⊢ V, U, X) →⊢ C, X).

If C ⊩ A ⊗ B, then

\frac{\frac{⊢ U, A ⊢ V, B}{⊢ V, U, A ⊗ B}}{⊢ V ⅋ U, A ⊗ B}

hence ⊢ C, A ⊗ B. Conversely if C ⊮ A ⊗ B, let X be such that ⊬ C, X and

∀U, V (⊢ U, A∧ ⊢ V, B →⊢ V ⅋ U, X).

In particular from ⊢ A^{⊥}, A, ⊢ B^{⊥}, B we get ⊢ B^{⊥} ⅋ A^{⊥}, X, i.e. ⊢ (A ⊗ B)^{⊥}, X. If ⊢ C, A ⊗ B we could compute

\frac{\frac{A ⊗ B ⊢ ^{⊥}(A ⊗ B^{⊥}) ^{⊥}((A ⊗ B)^{⊥}) ⊢ X}{A ⊗ B ⊢ X} ⊢ C, A ⊗ B}{⊢ C, X}

C ⊩ A ⅋ B  iff ∀X, Y (∀U(⊢ U, A →⊢ U, X) ∧ ∀V (⊢ V, B →⊢ V, Y) →⊢ C, X ⅋ Y) (4)

Assume C ⊩ A ⅋ B and take X = A, Y = B to get ⊢ C, A ⅋ B. Conversely, assume C ⊮ A ⅋ B and let X, Y testify this. Then in particular ⊢ A^{⊥}, X and ⊢ B^{⊥}, Y and ⊬ C, X ⅋ Y. Then however ⊢ B^{⊥} ⊗ A^{⊥}, X ⅋ Y, i.e. ⊢ ^{⊥}(A ⅋ B), X ⅋ Y, thus by CUT, ⊬ C, A ⅋ B.

The cases of & and ⊕ are similarly routine and the cases of constants are trivial.

(5)  C ⊩?A iff ∀X(X ∈ W ∧ ∀Y (⊢ Y, A →⊢ Y, X) →⊢ C, X)

If C ⊩?A, take X = ?A and get ⊢ C,?A by dereliction.

If C ⊮ ?A, let X ∈ W testify this (X = ?B). For Y = A^{⊥}, if ⊢ A^{⊥}, X, then ⊢ (?A)^{⊥}, X. Thus if ⊢ C,?A we would get ⊢ C, X by CUT.

(6)  C ⊩!A iff ∀X(∀Y (Y ∈ W ∧ ⊢ Y, A →⊢ Y, X))

If C ⊩ !A, take Y = ?B ∈ W; then ⊢ ?B,!A, thus ⊢ C,!A. If C ⊮ !A, let X testify this. For Y = ?A^{⊥} one gets !A ⊢ X; thus ⊬ C,!A by CUT.

9.4. Validity in a phasoid tout court refers of course to validity in the phasoid with the canonical base for exponentials. For the commutative case, i.e. LL proper, we get (in a two-sided formulation of LL) that Γ ⊢ Δ is provable in LL iff it is valid in all phasoids (or webs).

We present here a direct checking of this result. Soundness is obvious; so let us build a web

⟨FORM, ×, ⊥, ≤⟩

as follows: FORM is the set of formulas of L.

• The operation × is the naked tensor, defined by

A × B = \begin{cases}!D if A = B = !D \\ !(C & D) if A = !C, B = !D, C ≠ D \\ A ⊗ B otherwise. \end{cases}

• ⊥ is the constant ⊥.

• A ≤ B iff A ⊢ B is provable in LL. Notice that both A × B ⊢ A ⊗ B and A ⊗ B ⊢ A × B are provable in LL.

Let us check that this structure is a web (7.6). Trivially × preserves ≤ and it is quasicommutative and quasi-associative. To check continuity (2.1) observe that A × Z ≤ B iff A ⊗ Z ≤ B. Thus assume

∀Q(∀Z(A ⊗ Z ≤ B → Z ≤ Q) → P ≤ Q)

for A, B, X, Z, P, Q ∈ FORM: then trivially A ⊗ P ≤ B, hence A × P ≤ B. Now for the axioms proper of a web assume

∀X(P × X ≤ ⊥ → Q × X ≤ ⊥);

thus P ⊢ X^{⊥} → Q ⊢ X^{⊥} for all X; hence Q ⊢ P.

Fix the canonical base

gib(FORM) = {A : A × A = A and A ⊢ 1}
= {!B : B ∈ FORM},

since A × A = A means A = !B for some B.

Finally the interpretation: for P and atomic formula and A ∈ FORM define

A ⊩ P iff A ≤ P.

It is routine to check that for all formulas A, B

A ⊩ B iff A ≤ B.

Consider for instance the case of !; by definition

A ⊩!B iff ∀C(∀Z((Z ∈ gib(FORM) ∧ Z ⊢ B) → Z ⊢ C) → A ⊢ C).

Assume A ⊩ !B and take C = !B. If Z = !D and !D ⊢ B is provable, so is !D ⊢ !B, hence A ⊢!B.

Conversely assume A ⊢!B. Let C ∈ FORM and assume

∀Z((Z ∈ gib(FORM) ∧ Z ⊢ B) → Z ⊢ C).

In particular Z = !B ∈ gib(FORM) and !B ⊢ B; thus !B ⊢ C; by CUT we get A ⊢ C.

There is something magic in this proof: logically the naked tensor is just another name for the tensor. But it allows to forget about bases of exponentials, which is a semantical nicety of first class.

10. Quasi algebraic and algebraic semantic for LL

10.1. We start with a few definitions.

(i) A (quasi-bounded) quasi-lattice is a structure

⟨M, ≤, ∨, ∧, 0, T ⟩

where ≤ is a quasi order on M and

1. a ∨ b is a quasi-join of a and B, namely a ≤ a ∨ b, b ≤ a ∨ b and ∀x(x ≤ a ∧ x ≤ b → x ≤ a ∨ b);

2. a ∧ b is a quasi-meet of a and b, namely a ∧ b ≤ a, a ∧ b ≤ b and ∀x(a ≤ x ∧ b ≤ x → a ∧ b ≤ x);

3. 0 ≤ x ≤ T for all x ∈ M. One may like to formulate a quasi-duality principle for quasi-lattices (a good amount of lattice theory transfers to quasi-lattices: we postpone a closer investigation of this situation). If we put, as usual, a ∼ b for a ≤ b and b ≤ a, then ∼ is a congruence of the quasi-lattice (i.e. a ∼ a′ and b ∼ b′ imply a ∨ b ∼ a′ ∨ b′, a ∧ b ∼ a′ ∧ b′ and a ≤ b iff a′ ≤ b′.).

Thus in the quotient M/ ∼ we can define

a/∼ ≤ b/∼ iff a ≤ b
a/∼ ∨b/∼ = (a ∨ b)/∼
a/∼ ∧b/∼ = (a ∧ b)/∼
0 = 0/∼ T = T/∼

and M/∼ becomes a (bounded) lattice. Thus a lattice is nothing else then a reduced quasi-lattice (i.e. a ∼ b iff a = b) (I apologize to the late Garret Birkhoff).

(ii) A structure

⟨M, ·, ≤, e, ∨, ν, 0⟩

is a quasi-arabesque if

• ≤ is a quasi-order;

• a ∨ b is a quasi-join of a and b;

• ⟨M, ·, ≤ e⟩ is a (commutative) web; • ν is unary and obeys the laws

a · νa ≤ e
a ∼ ννa
if a · b ≤ e then a ≤ νb.

Here are a few properties of a quasi-arabesque M.

(a) a(b ∨ c) ∼ ab ∨ ac;

(b) νa ≤ νb iff b ≤ a;

(c) if we define a ∧ b = ν(νa ∨ νb) and T = ν0, then ⟨M, ≤, ∨, ∧, 0, T ⟩ is a quasilattice;

(d) if we define a −^{}b = ν(a · νb), then

x ≤ a −^{}b iff ax ≤ b

and a(a −^{}b) ≤ b.

(e) if we define 1 = νe, then a ∼ 1a ∼ a1;

(f) if we define x π y = ν(νx · νy), then

x π e ∼ x, x · 0 ∼ 0
x π T ∼ T
x π (y ∧ z) = (x π y) ∧ (x π Z)
1 ≤ x π νx

(g) 0 −^{}a ∼ T, a −^{}T ∼ T;

(e) a(h ∧ k) ≤ ah ∧ ak (a π h) ∨ (a π k) ≤ a π (h ∨ k).

For the proof: (a) Since a ≤ b ∨ c, c ≤ b ∨ c, then ab ≤ a(b ∨ c) and ac ≤ a(b ∨ c). Thus ab ∨ ac ≤ a(b ∨ c). The converse uses continuity: assume ab ≤ d, ac ≤ d. To prove a(b ∨ c) ≤ d it is enough to prove that

∀q(∀z(az ≤ d → z ≤ q) → (b ∨ c) ≤ q).

In fact, since in particular ab ≤ d, ac ≤ d, then b ≤ q, c ≤ q hence b ∨ c ≤ q.

(b) Let b ≤ a ≤ ννa; thus b · νa ≤ e, thus νa ≤ νb (by axiom ii-1 and because a ≤ ννa).

Assume νa ≤ νb. From ννb ≤ b, by what we have just seen, we get νb ≤ νννb. Thus νa ≤ νννb, hence ννb · νa ≤ e. But b ≤ ννb, thus b · νa ≤ ννb · νa by compatibility, hence b · νa ≤ a and finally b ≤ ννa ≤ a.

(c) Let x ∈ M, thus 0 ≤ x hence νx ≤ T. Thus for every x, x ≤ ννx ≤ T. To prove that a ∧ b is a quasi-meet of a, b, since trivially νa ≤ νa ∨ νb, we get a ∧ b ≤ ννa ≤ a (and ≤ b as well). Thus let d ≤ a, b: then νa, νb ≤ νd and thus νa ∨ νb ≤ νd, hence d ≤ ννd ≤ ν(νa ∨ νb) = a ∧ b.

(d) x ≤ ν(a · νb) iff x(a · νb) ≤ e iff (xa)νb ≤ a iff xa ≤ ννb. Then to prove that a(a −^{}b) ≤ b observe that a −^{}b ≤ a −^{}b.

(e) a · νa ≤ e, hence νe ≤ ν(a · νa), i.e. 1 ≤ a −^{}a. Thus 1a ≤ a and a1 ≤ a. Now a(a −^{}e) ≤ e by (d), hence a ≤ ν(a −^{}e) = a · νe = a · 1 etc..

(f) x π e = ν(νx · νe) = ν(νx · 1) ∼ ννx ∼ x. 0 ≤ νx thus 0x ≤ 0, hence 0x ∼ 0. Finally x π T = ν(νx · νT) = ν(νx · 0) ∼ ννx ∼ x; x · νx ≤ e, thus 1 ≤ ν(x · νx) ∼ x π νx.

(g) 0 −^{}a = ν(0 · νa) ∼ ν0 = T; a −^{}T = ν(a · νT) = ν(a · 0) = ν0 = T.

(e) Trivially a(h ∨ k) ≤ ah, ak, because · preserves ≤. Then use the definitions.

Remarks. (1) The definition of a quasi-arabesque can be simplified: if we require that · be quasi associative and quasi commutative and continuous (2.1), then ⟨M, ·, ≤, e⟩ is an arabesque.

(2) One also sees easily that the axiom “a ∼ ννa” could be substituted by property (b) above.

(v) Given a quasi-arabesque M, set

EX(a) = gib(M) ∩ â

where as usual â = {x : x ≤ a}. Then M is an archarabesque if EX(a) ≠ ∅ for all a ∈ M.

By a canonical exponentiation on an archarabesque M, we mean any mapping E ∈ ∏_{a∈M} EX(a) such that

(a) E is monotone: a ≤ b implies Ea ≤ Eb;

(b) Ea = a if a ∈ gib(M). By CANEX(M) we mean the set of all canonical exponentiations on M. The following properties of a canonical exponentiation E are useful. For a, b ∈ M

4. E(Ea) = Ea ≤ a;

5. E(Ea · Eb) = Ea · Eb;

6. E(a ∧ b) = Ea · Eb. For the proof: (4) holds because Ea ∈ gib(M). (5) holds, because gib(M) is closed under products; thus Ea · Eb ∈ gib(M).

(6) holds since E(x ∧ y) ≤ E(x) and E(x ∧ y) ≤ Ey then E(x ∧ y) · E(x ∧ y) ≤ Ex · Ey, i.e. E(x ∧ y) ≤ Ex · Ey. On the other side Ex · Ey ≤ Ex · 1 ≤ Ex ≤ x and Ex · Ey ≤ y, thus Ex · Ey ≤ x ∧ y. Hence E(Ex · Ey) = Ex · Ey ≤ E(x ∧ y).

We say that E^{0} ∈ CANEX(M) is a quasi-maximum if Ea ≤ E^{0}a for all a ∈ M and for all E ∈ CANEX(M). We say that the archarabesque M is a turbo archarabesque if it has a quasi-maximum canonical exponentiation E^{0} and gib(M) is closed under ·.

Now, given an archarabesque M with a canonical exponentiation E we can interpret formulas of L in M in the natural way: an assignment | | : AT ⟶ M extends uniquely to a morphism from FORM into M that is considered as an algebra of signature L as follows:

\frac{⊗ ⊕ ⅋ & −^{}( )^{⊥} 0 1 T ⊥}{· ∨ π ∧ −^{}ν 0 1 T e}

where a π b = ν(νa · νb), a −^{}b = ν(a · νb), T = ν0, 1 = νe.

If M is an archarabesque a formula A is

c-valid in ⟨M, E⟩ when 1 ≤ |A| for all assignments | |; c-valid in M, if it is c-valid in ⟨M, E⟩ for all E ∈ CANEX(M); c-valid if it is c-valid in all archarabesques.

(vi) A quasi-arabesque is after all a (special; kind of) linear frame, thus by a full quasiarabesque we mean a quasi-arabesque together with an ε-base for exponentials. Thus the notion of validity in a full linear frame applies to quasi-arabesques as well.

Finally a turbo arabesque is a special kind of archarabesque with any quasimaximum canonical exponentiation. We say that a formula is turbo valid if it is valid in all turbo arabesque (with any of their quasi-maximum canonical exponentiations).

10.2. Now we enter the realm of algebraic linear logic proper. By an arabesque we mean a reduced quasi-arabesque (i.e. a ∼ b implies a = b). By a girale we mean an arabesque with a further operation ! such that

!x ≤ x ∧ 1
!!x = !x
!x ·!y = !(x ∧ y).

Observe that an arabesque can be also defined as a lattice ordered commutative monoid ⟨M, ·, 1, ≤⟩ and moreover

a(b ∨ c) = ab ∨ ac
a · νa ≤ e
a = ννa
if ab ≤ e then a ≤ νb.

The proof of the equivalence is a matter of routine. Notice that arabesques (and girales) form quasivarieties (i.e. class of structure closed under the formations of subalgebras and direct products). The only axiom which is not equational is that from ab ≤ e one concludes a ≤ νb. We postpone to another occasion a closer investigation of these algebras.

10.3. The master completeness theorem. We can now summarize a good deal of our results on LL as follows:

For a formula A of L the following are equivalent:

1. A is valid in all full commutative webs;

2. A is valid in all full commutative phasoids;

3. A is valid in all full commutative word linear frames;

4. A is valid in all full commutative word webs;

5. A is valid in all webs (with the canonical base for exponentials);

6. A is valid in all full quasi-arabesques;

7. A is c-valid in all archarabesques;

8. A is turbo valid in all turbo arabesques;

9. A is valid in all girales;

10. ⊢ A is provable in LL.

Most of the implications are already in the previous sections, explicitly or implicitly in representation theorems.

We propose the following paths toward a proof:

(2) ⇔ (1) cfr. 8.12;

(1) ⇔ (3) cfr. 4.3;

(1) ⇒ (4) trivial and (4) ⇒ (9) cfr. 9.4;

(1) ⇒ (5) trivial and (5) ⇒ (6) because if ⟨M, E⟩ is an archarabesque with a canonical exponentiation E, define W ⊆ M by

a ∈ M iff a = Ex for some x ∈ M.

This is an ε-base over M, considered as a linear frame;

(6) ⇒ (7) trivial and (7) ⇒ (9) is really Girard’s device: in our setting, show that formulas of LL (as a web) are in fact a turbo-arabesque, when the canonical exponentiation is defined by the canonical base (cfr. 9.4);

(5) ⇒ (8) because in a girale, considered as a full quasi-arabesque, define en ε-base by taking W = !M;

(8) ⇒ (9) because the Lindenbaum algebra of LL is a girale;

(9) ⇒ (2) by: 9.1, 8.3-8.6 and 8.10.

10.4. The notion of a quasi-arabesque, based on that of quasi-lattice, naturally suggests a generalization to categorical setting: every proposition “a ≤ b” should come together with morphisms or “proofs” from a into b.

10.5. We leave to the reader the cases of cyclic quasi-arabesques and noncommutative as well.

11. The last metamorphosis of linear frames: quivers

11.1. The starting idea is: forget about · and ≤ in a linear frame and charge all the work on linear implication(s). Accordingly the slogan here is

“study the solutions of ax = b (and xa = b) in a binar”

A binar in universal algebra is a set with a binary operation ·. This used to be called a “groupoid” by group theorists before powerful categorical people bent this word into a different usage. Notice that these equations are linear equations, if any!!

The idea is quite simple. Given a binar ⟨L, ·⟩ let a → b be the set of solutions of the equation ax = b (and dually for b ← a) so that

ac = b iff c ∈ a → b
ca = b iff c ∈ b ← a.

This allows a magnification of the usual residuations in P(L)

X −^{}Y = ⋂_{x∈X} ⋃_{y∈Y} (x → y) (i)

X ^{}− Y = ⋂_{y∈Y} ⋃_{x∈X}(x ← y) (ii)

Now assume L is a nonempty set and let →, ← be two mappings from L × L into P(L) and let U be a subset of L. Define X −^{}Y and X ^{}− Y by using (i) and (ii). Further simplify “{a} ^{}− Y ”, “X −^{}{a}” by writing instead a −^{}Y and X ^{}− a; thus a ^{}− {b} is another name for a → b. So we will soon drop “→” in favor of “−^{}”already at the molecular level of elements of L which, following the useful mistake of G. Peano (he amended it finally, however) we are “identifying” with singletons. Next use U to introduce the right and left shadows of any element a ∈ L by defining

ρa = a −^{}U
ρ^{⌣}a = U ^{}− a

In the sequel we concentrate on LL proper(leaving iLL for another occasion).

A quiver is a structure ⟨A, ^{}−, −^{}, U⟩ where ^{}− and −^{}are mappings from L × L into P(L), U is a subset of L and the following axioms hold. L1. For all a, b ∈ L, there is a c ∈ L such that a ∈ b −^{}c; L2. If (a −^{}b) ∩ (a −^{}c) ≠ ∅ then b = c; L3. b ∈ a −^{}c iff a ∈ c ^{}− b; L4. If (a −^{}t) ^{}− c ∩ (a −^{}(t′ ^{}− c)) ≠ ∅ then ρ(t) = ρ(t′); L5. {ρa : a ∈ L} = {ρ^{⌣}a : a ∈ L}. A quiver is cyclic if ρa = ρ^{⌣}a for all a ∈ L, commutative if a −^{}b = b ^{}− a for all a, b ∈ L. Notice that commutative implies cyclic and that L5. is useless is a cyclic quiver (here commutativity seems rather unnatural).

The following properties of a quiver L are noteworthy: for a, b, c ∈ L, X, Y, Z ⊆ L and Z_{i} ⊆ L for all i ∈ I:

(i) L ∖ (a −^{}Z) = a −^{}(L ∖ Z); (ii) a −^{}(⋂_{i∈I} Z_{i}) = ⋂_{i∈I}(a −^{}Z_{i}); (iii) a ∈ b −^{}X iff b ∈ X ^{}− a; (iv) (a −^{}X) ^{}− c = a −^{}(X ^{}− c);

(v) L ∖ (a ^{}− b) = (L ∖ {a}) ^{}− b L ∖ (X ^{}− b) = (L ∖ Z) ^{}− b

(vi) (⋂_{i∈I} Z_{i}) ^{}− A = ⋂_{i∈I}(Z_{i} ^{}− A); (vii) (b ^{}− a) ∩ (c ^{}− a) ≠ ∅ implies b = c; (viii) If X ⊆ Y then: Z −^{}X ⊆ Z −^{}Y, X ^{}− Z ⊆ Y ^{}− Z, Y −^{}Z ⊆ X −^{}Z and

Z ^{}− Y ⊆ Z ^{}− X; (ix) X −^{}(⋂_{i∈I} Z_{i}) = ⋂_{i∈I}(X −^{}Z_{i}) and (⋂_{i∈I} Z_{i}) ^{}− X = ⋂_{i∈I}(Z_{i} ^{}− X).

Maybe only (i) deserves a word of proof; we can show in fact that (i) is equivalent to the conjunction of L1 and L2. Notice that (i) implies (ii):

a −^{}⋂_{i∈I} Z_{i} = a −^{}(L ∖ ⋃_{i∈I}(Z_{i}))

= L ∖ (a −^{}⋃_{i∈I}(Z_{i})) = L ∖ ⋃_{i∈I}(a −^{}(L ∖ Z_{i}))

= L ∖ ⋃_{i∈I}(L ∖ (a −^{}Z_{i})) = ⋂_{i∈I}(a −^{}Z_{i}).

Thus assume, (i): then L = L ∖ (a ^{}− ∅) = a −^{}L. thus L1. follows. Moreover if b ≠ c, we have {b} ∩ {c} = ∅, thus a −^{}({b} ∩ {c}) = ∅ and by (ii) (a −^{}b) ∩ a −^{}c = ∅.

Conversely assume L1., L2. Let y ∉ a −^{}(L ∖ Z) (i.e. whenever y ∈ a −^{}u then u ∈ Z); by L1 there is such a u ∈ Z, hence y ∈ a −^{}Z. On the other hand, let y ∈ a −^{}z for some z ∈ Z. Then by L2., for any t ≠ z, y ∉ a −^{}t. Thus y ∉ a −^{}(L ∖ {z}); but L ∖ {z} ⊇ Z, thus y ∉ a −^{}(L ∖ Z).

11.2. (i) In the case of a binar ⟨L, ·⟩, axioms L1. and L2. correspond to the totality and single valuedness of the binary operation. And in fact in any quiver we can recover, if we need it, a binary operation by defining

a · b = c iff b ∈ a −^{}c (iff a ∈ c ^{}− b)

and of course −^{}and ^{}− are just the residuations of singletons.

(ii) Really quivers are metamorphoses of phasoids. In fact, given a quiver, define · as above and then define a R b iff b ∈ ρa (iff a ∈ ρ^{⌣}b, by 11.1(iii)). Finally let U = R(1) = R^{⌣}(1).

Thus we really get a phasoid in case ⋂_{a∈L}(a −^{}a) ≠ ∅; then this set is a singleton and so in this case we have also 1 defined by

1 = ιx(x ∈ ⋂_{a∈L}(a −^{}a)) (Hilbert’s ι).

Notice that axiom L4. takes care of R-associativity and L5. of quasi symmetry of R.

Conversely a phasoid gives raise to a quiver if we define a → b = {a} −^{}{b}, U = R(1) etc. We spare the Brazilian forest, by avoiding the construction of a semantic with quivers (the notion of a base for exponentials gets its natural rephrasing in quiver’s setting). Also a soundness and completeness theorem can be obtained to supplement the list in 10.3. Rather we note the following

(iii) Axioms L1. and L2. transfer from −^{}to ^{}− because of L3., which in turn is based on the fact that we insist on one multiplication and two implications (in the “noncommutative” case).

(iv) The villain of the situation is axiom L4., which has to take care of associativity (of R-associativity to be precise).

Thus we envisage some possibilities for further inquiries in the following directions:

A. Avoiding explicit associativity would be possible by allowing a (conservative) extension of LL with a language admitting omnivorous connectives (i.e. a binary ⊗, a ternary ⊗, etc.) with obvious rules. Thus we may finally gain control over the stubborn ability of commas (both on the left and the right side of a sequent) to be desperately “associative”.

Technically, this would mean to consider not only ρa but also

ρ(a, b) = b −^{}ρa
ρ(a, b, c) = c −^{}ρ(a, b)
⋮
ρ^{⌣}(a, b) = ρ^{⌣}b ^{}− a
ρ^{⌣}(a, b, c) = ρ^{⌣}(a, b) −^{}c
⋮

and similarly

ρ(X) = ⋃_{z∈X} ρz

ρ(X, Y) = ⋃{ρ(x, y) : x ∈ X, y ∈ Y }

⋮

ρ^{⌣}(X) = ⋃_{z∈X} ρ^{⌣}z

ρ^{⌣}(X, Y) = ⋃{ρ^{⌣}(x, y) : x ∈ X, y ∈ Y }

⋮

This way we recover the power of the comma , “inside ρ” (i.e. inside R). B. As to (iii) one might perhaps attempt at a duplication of the tensor, thus inventing

a double linear logic: this should however get a real motivation in other contexts (proof theory). But this may contribute to the question (of Girard): “Which is the real noncommutative linear logic?”

C. Also connected to (iii) is our next remark . For obtaining completeness, it is in fact enough to consider flat quivers: a quiver is called flat if

Card(a −^{}b) ≤ 1 for all a.b ∈ L

and Card(a ^{}− b) ≤ 1 too. In fact the quiver of formulas (cfr. 9.3, the phasoid of formulas) is obtained by (here we must use →)

A → B = \begin{cases}\{X\} if B is A ⊗ X \\ ∅ otherwise \end{cases}

and similarly for A ← B, which is of course a flat quiver.

Now a flat quiver is a pretty friendly structure, in the following approach: we have two partial operations −^{}and ^{}− in L (usual operations, partial mappings from L × L into L and U ⊆ L). Thus we can use Kleene’s “almost identity” symbol: a −^{}b ≈ c means a −^{}b exists and it is c. Then the axioms for a flat quiver boil down to the following first order sentences (ρx is now defined as {y : ∃u ∈ U with y ≈ x −^{}u}, a −^{}X = {x : ∃z ∈ X with x ≈ a −^{}z}, etc.) Q1. ∀a, b∃c : a ≈ b −^{}c; Q2. if b ≠ c then a −^{}b ≉ b −^{}c; Q3. b ≈ a −^{}c iff a ≈ c ^{}− b; Q4. = L4.; Q5. = L5.

D. To deal with exponentials one may (provisionally) work with a base of exponentials W, i.e. a subset W of a quiver L such that ρ(W) = U, for a ∈ W, a ≈ a −^{}a and for a, b ∈ W ∃c ∈ W such that a ≈ b −^{}c.

E. One may as well enlarge quivers to allow the consideration of equations in several

unknowns:

∑ a_{i}x_{i} = c.

(and of course, you may then consider linear systems of equations too..., once you give a meaning to summation).

APPENDIX A

Propositional languages:

Atoms: P_{i}, i ∈ ω. L_{i} : ⊕, &, ⊗, −^{}, ( )^{⊥}, !, ?, ⊥, 1, 0, T. NC − L_{i} : ⊕, &, ⊗, −^{}, ( )^{⊥}, !, ?, ⊥, 1, 0, T, ^{}−, ^{⊥}( ). L : ⊕, &, ⊗, −^{}, ( )^{⊥}, !, ?, ⊥, 1, 0, T, ⅋. NC − L : ⊕, &, ⊗, −^{}, ( )^{⊥}, !, ?, ⊥, 1, 0, T, ⅋, ^{}−, ^{⊥}( ).

Logical systems: Γ, Δ are finite sequences of formulas.

[A.1] LL: Girard’s formulation [6], one sided; linear negation allowed only on atoms; language L.

LOGICAL AXIOMS

⊢ A, A^{⊥}

CUT RULE

\frac{⊢ A, Γ ⊢ A^{⊥}, Δ}{⊢ Γ, Δ}

EXCHANGE RULE

ADDITIVE RULES

\frac{⊢ A, Γ  ⊢ B, Γ}{⊢ A & B, Γ}  \frac{⊢ A, Γ}{⊢ A ⊕ B, Γ}  \frac{⊢ B, Γ}{⊢ A ⊕ B, Γ}

\frac{⊢ Γ}{⊢ Δ}  where Δ is obtained by permuting the formulas of Γ.

⊢ T, Γ Γ arbitrary

52 ALDO URSINI

MULTIPLICATIVE RULES

⊢ 1 \frac{⊢ Γ}{⊢ ⊥, Γ}

\frac{⊢ A, Γ  ⊢ B, Δ}{⊢ A ⊗ B, Γ, Δ}  \frac{⊢ A, B, Γ}{⊢ A ⅋ B, Γ}

EXPONENTIAL RULES

\frac{⊢ A, Γ}{⊢?A, Γ}  \frac{⊢ Γ}{⊢?A, Γ}  \frac{⊢?A,?A, Γ}{⊢?A, Γ}  \frac{⊢ A,?Γ}{⊢!A,?Γ}.

[A.2] tLL: two sided linear logic [6], language L.

LOGICAL AXIOMS

A ⊢ A

CUT RULE

\frac{Γ_{1} ⊢ Δ_{1}, A A, Γ_{2} ⊢ Δ_{2}}{Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2}}

EXCHANGE RULES

\frac{Γ ⊢ Δ_{1}, A, B, Δ_{2}}{Γ ⊢ Δ_{1}, B, A, Δ_{2}}  \frac{Γ_{1}, A, B, Γ_{2} ⊢ Δ}{Γ_{1}, B, A, Γ_{2} ⊢ Δ}

NEGATION RULES

\frac{A, Γ ⊢ Δ}{Γ ⊢ Δ, A^{⊥}}  \frac{Γ ⊢ Δ, A}{A^{⊥}, Γ ⊢ Δ}

ADDITIVE RULES

Γ ⊢ Δ, T 0, Γ ⊢ Δ
\frac{Γ ⊢ Δ, A  Γ ⊢ Δ, B}{Γ ⊢ Δ, A & B}  \frac{A, Γ ⊢ Δ}{A & B, Γ ⊢ Δ}  \frac{B, Γ ⊢ Δ}{A & B, Γ, Δ}
\frac{Γ ⊢ Δ, A}{Γ ⊢ Δ, A ⊕ B}  \frac{Γ ⊢ Δ, B}{Γ ⊢ Δ, A ⊕ B}  \frac{A, Γ ⊢ Δ B, Γ ⊢ Δ}{A ⊕ B, Γ ⊢ Δ}

MULTIPLICATIVE RULES

⊢ 1  \frac{Γ ⊢ Δ}{1, Γ ⊢ Δ}  ⊥ ⊢  \frac{Γ ⊢ Δ}{Γ ⊢ Δ, ⊥}

SEMANTICAL INVESTIGATIONS OF LINEAR LOGIC 53

\frac{Γ_{1} ⊢ Δ_{1}, A  Γ_{2} ⊢ Δ_{2}, B}{Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2}, A ⊗ B}  \frac{A, B, Γ ⊢ Δ}{A ⊗ B, Γ ⊢ Δ}
\frac{Γ ⊢ Δ, A, B}{Γ ⊢ Δ, A ⅋ B}  \frac{A, Γ_{1} ⊢ Δ_{1}  B, Γ_{2} ⊢ Δ_{2}}{A ⅋ B, Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2}}
\frac{A, Γ ⊢ Δ, B}{Γ ⊢ Δ, A − B}  \frac{Γ_{1} ⊢ Δ_{1}, A  B, Γ_{2} ⊢ Δ_{2}}{A − B, Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2}}

EXPONENTIAL RULES

\frac{Γ ⊢ Δ}{!A, Γ ⊢ Δ}  \frac{!A,!A, Γ ⊢ Δ}{!A, Γ ⊢ Δ}  \frac{A, Γ ⊢ Δ}{!A, Γ ⊢ Δ}  \frac{!Γ ⊢?Δ, A}{!Γ ⊢?Δ,!A}
\frac{Γ ⊢ Δ}{Γ ⊢ Δ,?A}  \frac{Γ ⊢ Δ,?A,?A}{Γ ⊢ Δ,?A}  \frac{Γ ⊢ Δ, A}{Γ ⊢ Δ,?A}  \frac{A,!Γ ⊢?Δ}{?A,!Γ ⊢?Δ}

[A.3] iLL : intuitionistic linear logic [1], language L_{i}. Δ is a short sequence.

LOGICAL AXIOMS

A ⊢ A

CUT RULE

\frac{Γ_{1} ⊢ A A, Γ_{2} ⊢ Δ}{Γ_{1}, Γ_{2} ⊢ Δ}

EXCHANGE RULE

\frac{Γ_{1}, A, B, Γ_{2} ⊢ Δ}{Γ_{1}, B, A, Γ_{2} ⊢ Δ}

NEGATION RULES

\frac{A, Γ ⊢}{Γ ⊢ A^{⊥}}  \frac{Γ ⊢ A}{Γ, A^{⊥} ⊢}

ADDITIVE RULES

Γ ⊢ T 0, Γ ⊢ Δ
\frac{Γ ⊢ A Γ ⊢ B}{Γ ⊢ A & B}  \frac{A, Γ ⊢ Δ}{A & B, Γ ⊢ Δ}  \frac{B, Γ ⊢ Δ}{A & B, Γ ⊢ Δ}
\frac{Γ ⊢ A}{Γ ⊢ A ⊕ B}  \frac{Γ ⊢ B}{Γ ⊢ A ⊕ B}  \frac{A, Γ ⊢ Δ B, Γ ⊢ Δ}{A ⊕ B, Γ ⊢ Δ}

54 ALDO URSINI

MULTIPLICATIVE RULES

⊢ 1  \frac{Γ ⊢ Δ}{1, Γ ⊢ Δ}  \frac{Γ ⊢}{Γ ⊢ ⊥}  ⊥ ⊢
\frac{Γ_{1} ⊢ A  Γ_{2} ⊩ B}{Γ_{1}, Γ_{1} ⊢ A ⊗ B}  \frac{A, B, Γ ⊢ Δ}{A ⊗ B, Γ ⊢ Δ}
\frac{A, Γ ⊢ B}{Γ ⊢ A − B}  \frac{Γ_{1} ⊢ A  B, Γ_{2} ⊢ Δ}{A − B, Γ_{1}, Γ_{2} ⊢ Δ}

EXPONENTIAL RULES

\frac{Γ ⊢ Δ}{!A, Γ ⊢ Δ}  \frac{!A,!A, Γ ⊢ Δ}{!A, Γ ⊢ Δ}  \frac{A, Γ ⊢ Δ}{!A, Γ ⊢ Δ}  \frac{!Γ ⊢ A}{!Γ ⊢!A}
\frac{Γ ⊢}{Γ ⊢?A}  \frac{Γ ⊢ A}{Γ ⊢?A}  \frac{A,!Γ ⊢?Δ}{?A,!Γ ⊢?Δ}

[A.3] nciLL : non commutative intuitionistic linear logic [1], language NC − L_{i}. Δ is a short sequence.

LOGICAL AXIOMS

A ⊢ A

CUT RULE

\frac{Γ ⊢ A Γ_{1}, A, Γ_{2} ⊢ Δ}{Γ_{1}, Γ, Γ_{2} ⊢ Δ}

NEGATION RULES

\frac{A, Γ ⊢}{Γ ⊢ A^{⊥}}  \frac{Γ ⊢ A}{Γ, A^{⊥} ⊢}  \frac{Γ, A ⊢}{Γ ⊢ ^{⊥}A}  \frac{Γ ⊢ A}{^{⊥}A, Γ ⊢}

ADDITIVE RULES

Γ ⊢ T Γ_{1}, 0, Γ_{2} ⊢ Δ
\frac{Γ ⊢ A Γ ⊢ B}{Γ ⊢ A & B}  \frac{Γ_{1}, A, Γ_{2} ⊢ Δ}{Γ_{1}, A & B, Γ_{2} ⊢ Δ}  \frac{Γ_{1}B, Γ_{2} ⊢ Δ}{Γ_{1}, A & B, Γ_{2} ⊢ Δ}
\frac{Γ ⊢ A}{Γ ⊢ A ⊕ B}  \frac{Γ ⊢ B}{Γ ⊢ A ⊕ B}  \frac{Γ_{1}A, Γ_{2} ⊢ Δ Γ_{1}, B, Γ_{2} ⊢ Δ}{Γ_{1}, A ⊕ B, Γ_{2} ⊢ Δ}

SEMANTICAL INVESTIGATIONS OF LINEAR LOGIC 55

MULTIPLICATIVE RULES

⊢ 1  \frac{Γ_{1}, Γ_{2} ⊢ Δ}{Γ_{1}, 1, Γ_{2} ⊢ Δ}  \frac{Γ ⊢}{Γ ⊢ ⊥}  ⊥ ⊢
\frac{Γ_{1} ⊢ A  Γ_{2} ⊢ B}{Γ_{1}, Γ_{2} ⊢ A ⊗ B}  \frac{Γ_{1}, A, B, Γ_{2} ⊢ Δ}{Γ_{1}, A ⊗ B, Γ_{2} ⊢ Δ}
\frac{A, Γ ⊢ B}{Γ ⊢ A − B}  \frac{Γ_{1} ⊢ A  Γ_{2}, B, Φ ⊢ Δ}{Γ_{2}, Γ_{1}, A − B, Φ ⊢ Δ}
\frac{Γ, A ⊢ B}{Γ ⊢ B − A}  \frac{Γ_{1} ⊢ A  Γ_{2}, Bb, Φ ⊢ Δ}{Γ_{2}, B − A, Γ_{1}, Φ ⊢ Δ}

EXPONENTIAL RULES

\frac{Γ_{1}, Γ_{2} ⊢ Δ}{Γ_{1},!A, Γ_{2} ⊢ Δ}  \frac{Γ_{1},!A,!A, Γ_{2} ⊢ Δ}{Γ_{1},!A, Γ_{2} ⊢ Δ}  \frac{Γ_{1}, A, Γ_{2} ⊢ Δ}{Γ_{1},!A, Γ_{2} ⊢ Δ}  \frac{!Γ ⊢ A}{!Γ ⊢!A}
\frac{Γ ⊢}{Γ ⊢?A}  \frac{Γ ⊢ A}{Γ ⊢?A}  \frac{!Γ_{1}, A,!Γ_{2} ⊢?Δ}{Γ_{1},?A,!Γ_{2} ⊢?Δ}

[A.5] ILL: linear intuitionistic logic [9], language L_{i} minus ⊥, ( )^{⊥} and exponentials.

LOGICAL RULES

A ⊢ A

CUT RULE

\frac{Γ ⊢ A Δ, A ⊢ B}{Γ, Δ ⊢ B}

EXCHANGE RULE

\frac{Γ, A, B, Δ ⊢ C}{Γ, B, A, Δ ⊢ C}

ADDITIVE RULES

Γ ⊢ T  \frac{Γ ⊢ A  Γ ⊢ B}{Γ ⊢ A & B}  \frac{Γ, A ⊢ C}{Γ, A & B ⊢ C}  \frac{Γ, B ⊢ C}{ΓA & B ⊢ C}
Γ, 0 ⊢ A  \frac{Γ ⊢ A}{Γ ⊢ A ⊕ B}  \frac{Γ ⊢ B}{Γ ⊢ A ⊕ B}  \frac{Γ, A ⊢ C  Γ, B ⊢ C}{Γ, A ⊕ B ⊢ C}

56 ALDO URSINI

MULTIPLICATIVE RULES

⊢ 1  \frac{Γ ⊢ A}{Γ, 1 ⊢ A}  \frac{ΓA  ΔB}{Γ, Δ ⊢ A ⊗ B}  \frac{Γ, A, B ⊢ C}{Γ, A ⊗ B ⊢ C}
\frac{Γ, A ⊢ B}{Γ ⊢ A − B}  \frac{Γ ⊢ A  Δ, B ⊢ C}{Γ, Δ, A − B ⊢ C}

[A.6] ncLL: noncommutative classical linear logic [2], language NC − L.

LOGICAL AXIOMS

A ⊢ A

CUT RULES

\frac{Γ_{1} ⊢ Δ_{1}, A  A, Γ_{2} ⊢ Δ_{2}}{Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2}}  \frac{Γ_{1}, A ⊢ Δ_{2}  Γ_{2} ⊢ A, Δ_{2}}{Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2}}
\frac{Γ ⊢ A  Γ_{1}, A, Γ_{2} ⊢ Δ}{Γ_{1}, Γ, Γ_{2} ⊢ Δ}  \frac{Γ ⊢ Δ_{1}, A, Δ_{2}  A ⊢ Δ}{Γ ⊢ Δ_{1}, Δ, Δ_{2}}

NEGATION RULES

\frac{A, Γ ⊢ Δ}{Γ ⊢ A^{⊥}, Δ}  \frac{Γ ⊢ Δ, A}{Γ, A^{⊥} ⊢ Δ}  \frac{Γ, A ⊢ Δ}{Γ ⊢ Δ,^{⊥}A}  \frac{Γ ⊢ A, Δ}{^{⊥}A, Γ ⊢ Δ}

ADDITIVE RULES

Γ ⊢ Δ_{1}, T, Δ_{2} Γ_{1}, 0, Γ_{2} ⊢ Δ
\frac{Γ ⊢ Δ_{1}, A, Δ_{2}  Γ ⊢ Δ_{1}, B, Δ_{2}}{Γ ⊢ Δ_{1}, A & B, Δ_{2}}  \frac{Γ_{1}, A, Γ_{2} ⊢ Δ}{Γ_{1}, & B, Γ_{2} ⊢ Δ}  \frac{Γ_{1}, B, Γ_{2} ⊢ Δ}{Γ_{1}, A & B, Γ_{2} ⊢ Δ}
\frac{Γ ⊢ Δ_{1}, A, Δ_{2}}{Γ ⊢ Δ_{1}, A ⊕ B, Δ_{2}}  \frac{Γ ⊢ Δ_{1}, B, Δ_{2}}{Γ ⊢ Δ_{1}, A ⊕ B, Δ_{2}}  \frac{Γ_{1}, A, Γ_{2} ⊢ Δ  Γ_{1}, B, Γ_{2} ⊢ Δ}{Γ_{1}, A ⊕ B, Γ_{2} ⊢ Δ}

MULTIPLICATIVE RULES

\frac{Γ_{1}, Γ_{2} ⊢ Δ}{Γ_{1}, 1, Γ_{2} ⊢ Δ}  \frac{Γ ⊢ Δ_{1}, Δ_{2}}{Γ ⊢ Δ_{1}, ⊥, Δ_{2}}
\frac{Γ_{1}, A, B, Γ_{2} ⊢ Δ}{Γ_{1}, A ⊗ B, Γ_{2} ⊢ Δ}  \frac{Γ_{1} ⊢ Δ_{1}, A  Γ_{2} ⊢ B, Δ_{2}}{Γ_{1}, Γ_{2} ⊢ Δ_{1}, A ⊗ B, Δ_{2}}

\frac{Γ ⊢ Δ, A, Θ_{1}  ⊢ B, Θ_{2}}{Γ ⊢ Δ, A ⊗ B, Θ_{2}, Θ_{1}}  \frac{⊢ Δ_{1}, A  Γ ⊢ Δ_{2}, Θ}{Γ ⊢ Δ_{2}, Δ_{1}, A ⊗ B, Θ}
\frac{Γ ⊢ Δ_{1}, A, B, Δ_{2}}{Γ ⊢ Δ_{1}, A ⅋ B, Δ_{2}}  \frac{Γ_{1}, A ⊢ Δ_{1}  B, Φ ⊢ Δ_{2}}{Γ_{1}, A ⅋ B, Φ ⊢ Δ_{1}, Δ_{2}}
\frac{Γ, A, Φ_{1} ⊢ Δ  B, Φ_{2} ⊢}{Γ, A ⅋ B, Φ_{1}, Φ_{2} ⊢ Δ}  \frac{Γ_{1}, A ⊢  Γ_{2}, B, Φ ⊢ Δ}{Γ_{2}, Γ_{1}, A ⅋ B, Φ ⊢ Δ}
\frac{A, Γ ⊢ B, Δ}{Γ ⊢ A − B, Δ}  \frac{Γ ⊢ Δ_{1}, A  B, Φ ⊢ Δ_{2}}{Γ, A − B, Φ ⊢ Δ_{1}, Δ_{2}}
\frac{Γ ⊢ Δ, A, Θ  B, Φ ⊢}{Γ, A − B, Φ ⊢ Δ, Θ}  \frac{Γ_{1} ⊢ A  Γ_{2}, B, Φ ⊢ Δ}{Γ_{2}, Γ_{1}, A − B, Φ ⊢ Δ}
\frac{Γ, A ⊢ Δ, B}{Γ ⊢ Δ, B − A}  \frac{Γ_{1} ⊢ A, Δ_{1}  Γ_{2}, B ⊢ Δ_{2}}{Γ_{2}, B − A, Γ_{1} ⊢ Δ_{2}, Δ_{1}}
\frac{Γ_{1} ⊢ Δ_{1}, A, Θ  Γ_{2}  B ⊢}{Γ_{2}, B − A, Γ_{1} ⊢ Δ, Θ}  \frac{Γ_{1} ⊢ A  Γ_{2}, B, Φ ⊢ Δ}{Γ_{2}, B − A, Γ_{1}, Φ ⊢ Δ}

EXPONENTIAL RULES

\frac{Γ_{1}, Γ_{2} ⊢ Δ}{Γ_{1},!A, Γ_{2} ⊢ Δ}  \frac{Γ_{1},!A,!A, Γ_{2} ⊢ Δ}{Γ_{1},!A, Γ_{2} ⊢ Δ}  \frac{Γ_{1}, A, Γ_{2} ⊢ Δ}{Γ_{1},!A, Γ_{2} ⊢ Δ}  \frac{!Γ ⊢?Δ_{1}, A, Δ_{2}}{!Γ ⊢?Δ_{1},!A, Δ_{2}}

\frac{Γ ⊢ Δ_{1}, Δ_{2}}{Γ ⊢ Δ_{1},?A, Δ_{2}}  \frac{Γ ⊢ Δ_{1},?A,?A, Δ_{2}}{Γ ⊢ Δ_{1},?A, Δ_{2}}  \frac{Γ ⊢ Δ_{1}, A, Δ_{2}}{Γ ⊢ Δ_{1},?A, Δ_{2}}  \frac{!Γ_{1}, A,!Γ_{2} ⊢?Δ}{!Γ_{1},?A,!Γ_{2} ⊢?Δ}

Appendix B

[B.1] (i) A linear frame is a structure ⟨M, ·, e, ≤ ⟩ where • ≤ is a quasi-order on M (set a ∼ b for a ≤ b and b ≤ a);

• · is quasi-associative on M (a(bc) ∼ (ab)c);

• · preserves ≤ (x ≤ y implies ax ≤ ay and xa ≤ xb);

• · is continuous: for a, b, p ∈ M, if

∀q(∀z(az ≤ b → z ≤ q) → p ≤ q) → ap ≤ b

and

∀q(∀z(za ≤ b → z ≤ q) → p ≤ q) → pa ≤ b

• e ∈ M. We usually consider only quasi-commutative linear frames satisfying a · b ∼ b · a.

• Cl(X) = {p : ∀q(X ≤ q → p ≤ q)} where X ⊆ M and X ≤ p means x ≤ p for all x ∈ X.

A full linear frame is a linear frame with a base for exponentials (W, N), namely

• W is an ϵ-base : W ⊆ {p : px ≤ x for all x ∈ X}, for every u, v ∈ W there is a w ∈ W such that w ∼ uv and for every u ∈ W uu ∼ u;

1. there is a g ∈ N such that e ∼ g;

2. (connection axiom) whenever u ∈ W and v ∈ N, there is a g ∈ N such that û −^{}v̂ = ĝ, (namely: g ∈ N, ug ≤ v and ux ≤ v implies x ≤ g).

(ii) A web (7.6) is a linear frame M in which

∀x(px ≤ e → qx ≤ e) → q ≤ p

and

∀x(xp ≤ e → xq ≤ e) → q ≤ p.

A full web is a web with a base (W, N) for exponentials.

(iii) A phasoid (8.1) is a structure ⟨M, R, ·, 1⟩ where • R is quasi-symmetric (i.e. {Ra : a ∈ M} = {R^{⌣}a : a ∈ M});

• · is R-associative, i.e. R(a · (b · c)) = R((a · b) · c);

• R(a) = R(1 · a) = R(a · 1);

• a · b R 1 iff a R b. A base for exponentials is a W ⊆ M such that

• R(1) = R(W); for a ∈ W, R(1) = R(aa) and a, b ∈ W, R(ab) ⊆ R(W);

• if a ∈ W there are a′, a′′ ∈ W such that R(a) = R^{⌣}(a′) and R^{⌣}(a) = R(a′′) (relative quasi-symmetry).

A phasoid M, W with a base for exponentials W is a full phasoid. A phasoid is reduced if Ra = Rb implies a = b.

(iv) A quasi-arabesque (10.1) is a structure

⟨M, ·, ≤, e, ∨, ν, 0⟩

such that • ≤ is a quasi-order;

• a ∨ b is a quasi-join of a and b;

• ⟨M, ·, ≤ e⟩ is a (commutative) web;

• ν is unary and obeys the laws

a · νa ≤ e
a ∼ ννa
if a · b ≤ e then a ≤ νb.

An arabesque is a reduced quasi-arabesque (i.e. a ∼ b implies a = b). Thus it is a lattice (a ∧ b = ν(νa ∨ νb)) such that ⟨M, ·1⟩ is a commutative monoid (1 = νe) and

a(b ∨ c) = ab ∨ ac
a · νa ≤ e
a = ννa
ab ≤ e → a ≤ νb.

(v) A girale is an arabesque with a further unary operation ! such that

!x ≤ x ∧ 1
!!x = !x
!x ·!y = !(x ∧ y)

(vi) A flat quiver is a structure ⟨A, ^{}−, −^{}, U⟩ where ^{}− and −^{}are partial mappings from L × L into P(L), U is a subset of L and (write: t ≈ q for “t, q are defined and equal”) ρa = {t : for some u ∈ U, t ≈ a ^{}− u}. Moreover the following axioms hold: L1. For all a, b ∈ L, there is a c ∈ L such that a ∈ b −^{}c; L2. If (a −^{}b) ∩ (a −^{}c) ≠ ∅ then b = c; L3. b ∈ a −^{}c iff a ∈ c ^{}− b; L4. If ((a −^{}t) ^{}− c) ∩ (a −^{}(t′ ^{}− c)) ≠ ∅ then ρ(t) = ρ(t′); L5. {ρa : a ∈ L} = {ρ^{⌣}a : a ∈ L}.

[B.2] (i) A rich source of examples of noncommutative linear frames is obtained by fixing a set U and considering M = P(U × U), with relational product ∘

S ∘ T ≡ {(a, b) : ∃x ∈ U, a S x T b}

and with inclusion as partial order (thus we have a RELF, i.e. a reduced linear frame). In that frame one has a very natural definition of both linear implications

R −^{}S = ⋃{T : R ∘ T ⊆ S}

and analogously for R ^{}− S. The one easily shows that

R ∘ (R −^{}S) ⊆ S.

Thus, since

R̂ −^{}Ŝ = {T : R ∘ T ⊆ S}

one easily shows

Cl(R̂ −^{}Ŝ) = (R −^{}S) .

But R −^{}S ∈ R̂ −^{}Ŝ, therefore R̂ −^{}Ŝ is closed, hence the “continuity axiom” (2.1(5)) holds in M.

(ii) Of course Johannson, Heyting and Boolean algebras are all examples of (commutative) linear frames.

Moreover consider any Boolean algebra A as a Boolean ring. Thus we have a “sum” a + b such that a + a = 0, (a + b) + a = b (a “subtractive algebra” [26]). Define for X, Y ⊆ A:

X −^{}Y = {x : ∀u ∈ X, u + x ∈ Y }.

This is a linear implication on P(A), w.r. to the monoid ⟨A, +⟩.

On the other side, given a girale, if · is a meet semilattice operation, 0 = e is the bottom element and distributivity holds, we get a kind of “generalized” Boolean algebra.

(iii) Other examples can be obtained by the universal algebraic ideal theory [9], [10]. In fact in any subtractive variety, ideals of an algebra form a quantale, but you may forget about the lattice operations. Thus simply the commutator of ideals establishes a structure of a reduced linear frame, with ⊆ as a partial order. Of course it is commutative. Then linear implication I −^{}J of two ideals is their well-known residuation operation: the “quotient J : I” in classical ideal theory (for rings) terminology.

(iv) The following commutative reduced girale G_{4} deserves some consideration (multiplication is defined in the unique possible way):

[figure: 1; ⊥; 0; T]

It also satisfies the rule

\frac{C ⊢ 1}{C ⊢ C ⊗ C}

(tetralinear logic). The conjecture is that tetralinear logic is complete w.r. to the semantic of G_{4} (thus tetralinear logic should come down to tetraboolean algebra ...).

(v) Other examples come easily from ℓ-groups and generally from Riesz groups.

(vi) Finally we may exploit Kripke models on their most friendly side: counterexamples. For instance the model

[figure: a ⊩ A; 1]

where W = {1} and · is defined in the obvious way, shows that it may happen that

1 ⊩!(!(!A −^{}B) −^{}A)

but

1 ⊮ A.

Thus (as it has to be) the Girard translation of Pierce law into LL is falsifiable. Similarly the Kripke model

[figure: 1; ⟳; ⟳; b ⊩ A; ⟲; c ⊩ B]

shows that

1 ⊮!(!A −^{}B) ⊕!(!B −^{}A)).

Finally

[figure: a ⊩ A; 1; ⟳]

shows that

1 ⊮!(!A) −^{}0.

Appendix C

We comment here on the related literature, following the order of the sections in the paper. We do not claim to any exhaustive covering of the literature, nor to any historical precision, nor to any exact ascribing the ideas or results to their ultimate discoverers (thus we electively quote survey papers).

Sec. 1. The notion of (reduced) linear frame is part of what is called iLL-algebra in [24], but we do not have any implication. The notion of base for exponentials allows us to avoid dealing with “topolinear systems” of [6]. This approach is related to “Girard structures” of [4], but we assume no completeness nor lattice operations here.

Sec. 4. There seem to be no evident relation with the result in [18] which shows that Lambek calculus is complete in the semantic of subsets of free semigroups.

Sec. 5. The survey [17] presents (sec. 7) a “Kripke-type” semantic. It is definitely different from the present one. For instance there you have

p ⊩ A ⊕ B iff ∃y∃z : y ∧ z ≤ x and (y ⊩ A ∨ Y ⊩ B) and (z ⊩ A ∨ z ⊩ B).

Also in [11] there is a Kripke-like semantic for a logic with T, &, ^{}− and ⇒. It is completely different from ours.

Sec. 7. The increment seems to be that the canonical model we build uses formulas in place of sequences [2] or multisets [8] of formulas. The remarks above on linear frames apply to webs as well.

Sec. 8. The notion of phasoid is a transformation of the “monoids with a suitable designated subset” of [2]. The relation R in a phasoid is the complement of the relation R hinted at in [4], sec. 3. Full phasoids seem to be new. Also every commutative phasoid has an algebra of Q-closed sets isomorphic to a suitable “pretopology” with interpretations restricted to “facts” (i.e. saturated X such that X = X^{⊥⊥}) of [21], and conversely. The notions themselves seem to be distinct; a “pretopology” is a special kind of closure operator over a monoid. It is not clear whether in a constructive setting there are pretopologies which are not tame (see Sec. 1). (Classically a Fock topological space is an example of a wild (= not tame) closure operation, see [23]).

The notion of base for exponentials is part of a notion of a set F in [4], sec. 4.6, but we do not assume any closure under suprema.

For (commutative) quantales, the basic reference is [19]. No relation seems to appear between bases for exponentials and what you find in [20], to deal with modalities on a quantale. We underline the curious result in 8.7: in a (non commutative) R-quantale, the relation R is to be quasisymmetric.

Sec. 9. No Kripke semantic is known to this author for classical linear logic (commutative, cyclic or non commutative). He was not able to find such in [3]. Some hints for Lambek calculi can be found in [22].

Again the canonical model uses formulas and ⅋ (in place of the usual monoid of sequences or multisets of formulas and usual composition). The invention of the naked tensor is obtained via a transfiguration of an idea in [8] (that we call “put a turbo on your monoid”).

Sec. 10. Quasi algebraic semantics is there to cope with the algebrization of a turbo monoid of Girard. Universal quasi-algebra is a newborn; it is not yet clear if it deserved to be born. Anyway it overlaps in some respects with some ideas in [27].

Arabesques and girales may be traced back, at least in part, to “Girard structures” in [4], but we drop the completeness assumption....

References

[1] V.M. Abrusci, Noncommutative intuitionistic linear propositional logic, Z. Math. Logik Grundlag. Math. 36 (1990), 297–318.

[2] , Phase semantics and sequent calculus for pure noncommutative classical linear logic, J. Symbolic Logic 56 (1991), 1403–1451.

[3] G. Allwein and J.M. Dunn, Kripke models for linear logic, J. Symbolic Logic 58 (1993), 514–545.

[4] A. Avron, The semantics and proof theory of linear logic, Theoret. Comput. Sci. 57 (1988), 161– 184.

[5] G. Debord, La société du spectacle, Buchet/Chastel, Paris, 1967.

[6] K. Došen, A brief survey of frames for Lambek calculus, Z. Math. Logik Grundlag. Math. 38 (1992), 179–187.

[7] J.-Y. Girard, Linear Logic, Theoret. Comput. Sci. 50 (1987), 1–102.

[8] , La Logique Lineaire, Pour la Science, vol. 100, 1990.

[9] , Linear logic: its syntax and semantics, Advances in Linear Logic (J.-Y. Girard et al., ed.), London Math. Soc. L.N., vol. 222, Cambridge, 1995.

[10] J.-Y. Girard and Y. Lafont, Linear logic and lazy computation, TAPSOFT ’87, Vol. 2 (H. Ehrig et al., ed.), Springer Verlag, Berlin, 1987, pp. 52–66.

[11] H.P. Gumm and A. Ursini, Ideals in universal algebras, Algebra Universalis 19 (1994), 45–54.

[12] J.S. Hodas and D. Miller, Logic programming in a fragment of intuitionistic linear logic, Information and Computation 110 (1994), 327–365.

[13] R. Hodel, Cardinal functions, Handbook of Set-Theoretical Topology (K. Kunen and J.E. Vaughan, eds.), North Holland, Amsterdam, 1984, pp. 1–61.

[14] J. Kripke, Semantical analysis of intuitionistic logic, I, Formal Systems and Recursive Functions (J.N. Crossley and M.A.E. Drummond, eds.), North Holland, Amsterdam, 1965, pp. 92–130.

[15] Y. Lafont, Unpublished manuscript on finite phases semantic, 1995.

[16] J. Lambek, From categorical grammar to bilinear logic, Substructural Logics (P. Schroeder-Heister and K. Došen, eds.), Clarendon, Oxford, 1993, pp. 207–237.

[17] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar, Decision problems for propositional linear logics, Ann. Pure Appl. Logic 56 (1992), 239–311.

[18] H. Ono, Semantics for substructural logics, Substructural Logics (P. Schroeder-Heister and K. Došen, eds.), Clarendon, Oxford, 1993, pp. 259–291.

[19] M. Pentus, Lambek calculus is L-complete, manuscript, 1993.

[20] K.I. Rosenthal, Quantales and their applications, Longmans Sc. & Techn., Essex, 1990.

[21] , Modules over a quantale and models for the operator ! in linear logic, Cahiers Topologie Géom. Différentielle Catégoriques 35 (1994), 329–333.

[22] G. Sambin, The semantics of pretopologies, Substructural Logics (P. Schroeder-Heister and K. Došen, eds.), Clarendon, Oxford, 1993, pp. 293–307.

[23] L.A. Steen and Jr. J.A. Seebach, Counterexamples in Topology, Holt & C., New York, 1970.

[24] A. Troelstra, Lectures on Linear Logic, CSLI, Stanford, 1992.

[25] A. Ursini, Undelivered communication at the 1993 Summer Meeting of ASL, abstract in Bull. Symbolic Logic, 1(1995), 114.

[26] , On subtractive varieties, i, Algebra Universalis 31 (1994), 204–222.

[27] N. Weaver, Generalized varieties, Algebra Universalis 30 (1993), 27–52.

[28] D.N. Yetter, Quantales and (noncommutative) linear logic, J. Symbolic Logic 55 (1990), 41–64.

Dipartimento di Matematica, Via del Capitano 15, 53100 Siena ITALY

  E-mail address: ursini@unisi.it