Resource models and proof-search in Intuitionistic Linear Logic

D. Larchey-Wendling and D. Galmiche

LORIA UMR 7503 – Université Henri Poincaré Campus Scientifique, BP 239 54506 Vandœuvre-lès-Nancy, France

Abstract

In this paper, we propose to investigate and to revise the semantics of Intuitionistic Linear Logic (ILL), from an unified analysis of known semantics like phase semantics or Petri nets semantics. Thus, we focus on notions like quantale, closure and resource frames and we define a new semantics of ILL that is called resource semantics. The completeness and the finite model property are proved from a based-on proof-search method in which countermodels are obtained from refutation trees. Moreover, we define a new preordered monoid semantics from an adequate choice of pretopology. As Petri nets can be seen as concrete representations of preordered monoids, such a choice also leads to a new Petri nets semantics for ILL with new results like completeness and finite model property. From these semantical considerations, we obtain some results about non-provability in ILL and then we can expect to develop methods for the generation of countermodels.

1 Introduction

Linear logic (denoted LL) [13] is a powerful and expressive logic with connections to a variety of topics in computer science as logic programming, concurrency or functional programming. In this context, Intuitionistic Linear Logic (ILL) and some of its sub-fragments are often used as the basic logic of logical frameworks[3,18]. From the natural deduction and sequent calculus proof systems of ILL one can investigate the problems of type inference and type safety [18] but also apply the programming with proofs paradigm. Moreover there exists an important correspondence between ILL and Petri nets [19] and also between predicate ILL and high-level nets [17]. Such well-known relationships encourage and justify research works on efficient proof-search methods in order to prove or disprove properties of systems expressed for instance in ILL.

Preprint submitted to Elsevier Preprint 10 November 2000

We have previously studied proof-search in ILL from the definition of canonical proofs that are complete w.r.t. provability [12] but also from a based-on proof nets approach [2]. In a complementary way, it is very important to capture provability but also non-provability in ILL, with some new calculi that could be effectively used to build countermodels as it can already be done in Intuitionistic Logic (IL) [11,25]. In this context, we first have to analyze well-known ILL semantics like algebraic and phase semantics but also the relationships between ILL and the Petri nets that are in background of such a study. Petri nets have been early made into models of ILL in such a way that many properties of the nets become expressible in the logic [7]. The completeness for ILL w.r.t. Petri nets as a model has been studied in [8]. We know, for instance, that they form a sound and complete model for the ⊕-free fragment of ILL and in the case of the ⊸-free fragment an extra axiom (of distributivity of & over ⊕) is necessary to have the completeness. Moreover, with the classical interpretation of [8] one cannot establish the non-distributivity of & over ⊕, namely that (A ⊕ B) & C ⊢ (A ⊕ C) & (B ⊕ C) is not provable in ILL. Our initial motivation is to understand why this semantics is not complete and then to propose a complete one, by focusing also on the construction of some countermodels for non-provable formulae of ILL. In section 2, after reminding the notion of quantale, we present the algebraic semantics of ILL and its properties. Then we show that any quantale can be seen as a stable closure. With the particular case of the MacNeille closure, we recover the well-known completeness result of ILL w.r.t. phase semantics. Moreover we illustrate the use of some quantales as countermodels. If we consider another closure, as for example the downward closure, we could obtain another model of ILL but it has some major drawbacks w.r.t. the completeness. In section 3, we present a new semantics of ILL, called resource semantics, from the notion of resource frame and an appropriate closure operator. The completeness and cut-elimination theorems are direct and natural applications of the so-called syntactic models. To complete these contributions, we consider in section 4 the effective construction of counter-models with a method based on a proof-search approach and the appropriate notion of of refutation tree. Thus, we build, from a refutation tree, a particular finite resource frame such that the interpretation of ILL in this frame (that is a countermodel) leads to the finite model property. From this result, we can deduce the completeness (with a clear and elegant proof) and the finite model property for the previous semantics of ILL presented in section 2. In section 5, we come back to the notion of (pre)ordered monoid and propose an algebraic characterization of extensions called ∨-completions. It results from the application of particular closures called pretopologies. Moreover we propose a new semantics of ILL from the greatest pretopology. In section 6, we show that a Petri net can be seen as a preordered monoid and consequently a choice of an appropriate pretopology over this structure leads to a particular quantale and then to a new Petri net semantics of ILL. The initial semantics in [8] corresponds in fact to the choice of the least pretopology and is not complete because of that, even if the completeness can be achieved in particular fragments of ILL. Therefore, we define, from the choice of the greatest pretopology, a new interpretation of ILL on Petri nets with completeness for the full logic and with the finite model property. In this case, we can naturally build from this semantics a countermodel for the non-distributivity of & over ⊕. Moreover, a very similar study on resources and semantics can be developed for the non-commutative ILL, following the same steps and with simple and appropriate adaptations of the main notions for the non-commutative logic.

2 Semantics of Intuitionistic Linear Logic

We focus in this section on the relationships between the notions of quantale and stable closure and then we present the algebraic and phase semantics of ILL from this point of view.

2.1 Basic definitions, notations and conventions

In this paragraph, we remind the basic syntactic notions of ILLthat are formulae, multisets and sequents. On the semantic side, we remind the notions of monoid and (pre)ordered set and explain how to interpret the preceding syntactic objects. Through the rest of the paper, we will suppose that the reader is familiar with all these concepts. The set of formulae Forms of propositional (commutative) exponential-free intuitionistic linear logic (ILL for short) built on a set Vars of variables are inductively defined by

Forms: A::= X | 1 | ⊥ | ⊤ | A □ A for □ ∈ {⊗, &, ⊕, ⊸} and X ∈ Vars

Therefore, Vars ⊆ Forms and if A, B, C ∈ Forms then A ⊸ (B ⊗ C) ∈ Forms. The letters A, B, C will usually be used to denote arbitrary formulae of ILL. A context A_{1}, …, A_{n} is a multiset of formulae, i.e. a list where the order is not taken into account, so A, A, B is equal to A, B, A but not to A, B because because the number of A occurrences is different. An arbitrary context will usually be denoted by the letters Γ, Δ, Σ, …, the empty context by ∅ and Contexts will denote the set of contexts. A sequent is a pair (Γ, A) ∈ Contexts × Forms denoted by Γ ⊢ A. When Γ is the empty context ∅, we also denote by ⊢A the sequent (∅, A). The calligraphic letters K, P, M, Q, … will usually denote sets with some additional structure. Uppercase letters X, Y, … denote subsets of these sets with usually no additional structure. Lowercase letters x, y, … denote elements of sets K or subsets X. The symbol ℙ(K) denotes the powerset of the set K, i.e. the set of all the subsets of K.

A (unital commutative) monoid is a pair (M, •) that consists of a set M and a binary operation • on M which is associative, commutative and has a neutral element denoted by e. A preordered set is a pair (P, ⩽) that consists of a set P and a binary relation ⩽ on P that is reflexive and transitive. When ⩽ is also antisymmetric, we obtain a partially ordered set (poset for short). The so-called downward closure of a subset X ⊆ P is defined by ↓X ≜ {z ∈ P | ∃x ∈ X, z ⩽ x}.

If ⊆ K × P is a binary relation then we denote k p when (k, p) ∈ holds and by extension K p when ∀k ∈ K, k p holds for a subset K of K. For example, when ⩽ is a preorder relation on the set X then X ⩽ x means that x is an upper bound of the subset X of X. If • is a binary operation on the set K, then for X, Y ⊆ K we define X • Y ≜ {x • y | x ∈ X, y ∈ Y }. By an abuse of notation, we denote the subset {x} • Y by x • Y. Given a set K and suitable operations on K, we can define an interpretation of the ILL formulae. This is usually done by induction on the structure of the formula, given an interpretation of the variables in Vars, i.e. a function σ : Vars → K. The interpretation will be denoted by ⟦A⟧ and then for a variable X ∈ Vars, we have the identity ⟦X⟧ = σ(X). Thus, we obtain a function ⟦·⟧ : Forms → K. If • is a monoidal operation on K then we can extend ⟦·⟧ to Contexts by ⟦A_{1}, …, A_{n}⟧ ≜ ⟦A_{1}⟧ • ⋯ • ⟦A_{n}⟧. In case Γ = ∅ we have ⟦∅⟧ = e.

After having reminded these basic definitions, we define the notion of validity for formulae and sequents of ILL from the initial sequent calculus. Then we briefly remind the algebraic and phase semantics and their completeness results. We link both semantics with the well-known representation results of propositions 9 and 10.

2.2 The sequent calculus

There are different equivalent ways to define proof systems for ILL [3]. In figure 1, we present a sequent calculus that is well-suited for our purpose, in particular for the construction of countermodels we will consider in section 3.6.

A sequent Γ ⊢ A is said to be valid if there is a proof of this sequent following the rules of figure 1. Equivalently, the set of valid sequents is the smallest set closed under those rules. We will denote by Γ ⊩ A the fact that the sequent Γ ⊢ A is valid.

Proposition 1 A is a valid formula of ILL if and only if ⊩A.

A ⊢ A [id]  \begin{matrix}Γ ⊢ A & Δ, A ⊢ B \\ Γ, Δ ⊢ B \end{matrix} [cut]
\begin{matrix}Γ, A, B ⊢ C \\ Γ, A ⊗ B ⊢ C \end{matrix} [⊗_{L}]  \begin{matrix}Γ ⊢ A & Δ ⊢ B \\ Γ, Δ ⊢ A ⊗ B \end{matrix} [⊗_{R}]
\begin{matrix}Γ ⊢ A & Δ, B ⊢ C \\ Γ, Δ, A ⊸ B ⊢ C \end{matrix} [⊸_{L}]  \begin{matrix}Γ, A ⊢ B \\ Γ ⊢ A ⊸ B \end{matrix} [⊸_{R}]
\begin{matrix}Γ, A ⊢ C \\ Γ, A & B ⊢ C \end{matrix} [&_{L}^{1}] \begin{matrix}Γ, B ⊢ C \\ Γ, A & B ⊢ C \end{matrix} [&_{L}^{2}] \begin{matrix}Γ ⊢ A & Γ ⊢ B \\ Γ ⊢ A & B \end{matrix} [&_{R}]
\begin{matrix}Γ, A ⊢ C & Γ, B ⊢ C \\ Γ, A ⊕ B ⊢ C \end{matrix} [⊕_{L}] \begin{matrix}Γ ⊢ A \\ Γ ⊢ A ⊕ B \end{matrix} [⊕_{R}^{1}] \begin{matrix}Γ ⊢ B \\ Γ ⊢ A ⊕ B \end{matrix} [⊕_{R}^{2}]
\begin{matrix}Γ ⊢ A \\ Γ, 1 ⊢ A \end{matrix} [1_{L}] _{⊢1 [1_{R}]} _{Γ, ⊥ ⊢ A [⊥_{L}]} _{Γ ⊢ ⊤ [⊤_{R}]}

Fig. 1. The ILL sequent calculus

This result can also be considered as a definition. The reader might consult [30] for more details. From such a calculus, we can study proof-search in ILL in order to efficiently prove or disprove properties of systems expressed in this logic. Proof-search methods based on canonical proofs [12] or on proof nets construction [2] have been studied for ILL. But alternatively we aim at proposing calculi that can effectively build countermodels in case of non-provability in fragments of Linear Logic as it can already be done in Intuitionistic Logic (IL) [11,25]. In this context, we first have to focus on the definition of new semantics from which simple and useful proof-search and countermodels generation methods could be derived. An initial step consists in revisiting known semantics of ILL.

2.3 Algebraic semantics

The algebraic structure of the completed Lindenbaum algebra [26,30] — the algebra of formulae up to the logical equivalence — is characterized by the following definition (see [31]).

Definition 2 (Quantale) A triplet (Q, •, ⩽) is a quantale if (Q, •) is a monoid, (Q, ⩽) is a complete lattice and for all a, (b_{i})_{i} in Q, a•⋁_{i} b_{i} = ⋁_{i}(a•b_{i}) and ⋁_{i} b_{i} • a = ⋁_{i}(b_{i} • a).

A quantale Q is unital if there is a unit of the monoid, i.e., an element e such that, for all a ∈ Q, a • e = e • a = a. Q is commutative if • is commutative. We denote by e the unit of the monoid, by ⊥ (resp. ⊤) the smallest (resp. greatest) element of the lattice. The last condition is equivalent to the existence of a right (resp. left) ad-

\begin{aligned}⊥ • & ⊤ & = & ⊥ \\ m_{i} • & ⊤ & = & ⊤ \\ m_{i} • & ⊥ & = & ⊥ \\ m_{i} • & m_{j} & = & m_{i+j} \end{aligned}

Fig. 2. A quantale

joint x ⊸•_{r} (·) (resp. x ⊸•_{l} (·)) to x • (·) (resp. (·) • x) given by the identity x ⊸•_{r} y = ⋁{z | z • x ⩽ y} (resp. x ⊸•_{l} y = ⋁{z | x • z ⩽ y}).

({⊥}∪ℕ∪{∞}, +, ⩽) and ([0, n], max, ⩽) are examples of quantales. A quantale is said to be finite if the underlying set Q is finite. For the sake of simplicity we will also denote by Q the quantale when the algebraic structure is unambiguous.

Let us illustrate the construction of a quantale from an ordered monoid. A first idea consists in starting from a monoid M with the flat order on M, therefore in identifying the quantales that contain this ordered monoid. For instance, let us consider M = ℤ/kℤ = ({m_{0}, …, m_{k−1}}, •), the integers modulo a natural k and • the addition of classes, hence for example m_{3} • m_{k−2} = m_{1}. This is of course a commutative monoid and even a commutative group. If we consider Q = {m_{0}, …, m_{k−1}} ∪ {⊥, ⊤} with the obvious lattice structure: ⊥ is the least element and ⊤ the greatest, the order on the m_{i} (being flat) is then preserved. The monoidal structure is preserved but it should be extended to ⊥ and ⊤. We can observe that only one extension gives a valid quantale. It is the one given in figure 2.

The simplicity of this construction should not be misleading. Building a quantale from a “flat monoid” is not always so easy as only considering a top and bottom element. Indeed, the preceding construction succeed because the underlying monoid is regular (definition in subsection 5.6). However, we will see how to overcome this difficulty in section 5.

Let us now give the algebraic semantics of ILL. Given a quantale (Q, •, ⩽) and an interpretation σ : Vars → Q of logical variables, we are able to interpret the formulae of ILL by the following definition.

\begin{matrix}⟦X⟧ ≜ & σ(X) & ⟦A ⊸ B⟧ ≜ & ⟦A⟧ ⊸• ⟦B⟧ \\ ⟦1⟧ ≜ & e & ⟦A ⊗ B⟧ ≜ & ⟦A⟧ • ⟦B⟧ \\ ⟦⊥⟧ ≜ & ⊥ & ⟦A ⊕ B⟧ ≜ & ⟦A⟧ ∨ ⟦B⟧ \\ ⟦⊤⟧ ≜ & ⊤ & ⟦A & B⟧ ≜ & ⟦A⟧ ∧ ⟦B⟧ \end{matrix}

Quantale interpretation

For a context Γ = A_{1}, …, A_{n}, we write ⟦Γ⟧ for ⟦A_{1}⟧ • ⋯ • ⟦A_{n}⟧.

Theorem 3 (Soundness) If Γ ⊩ B then ⟦Γ⟧ ⩽ ⟦B⟧.

PROOF. By induction on the proof of the sequent Γ ⊢ B. We only give here the case corresponding to the rule [⊸_{L}]. Let us assume that we have a proof where the last rule is

\begin{matrix}Γ ⊢ A & Δ, B ⊢ C \\ Γ, Δ, A ⊸ B ⊢ C \end{matrix} [⊸_{L}]

Then we have two shorter proofs of Γ ⊢ A and Δ, B ⊢ C. By the induction hypothesis, we obtain ⟦Γ⟧ ⩽ ⟦A⟧ and ⟦Δ⟧ • ⟦B⟧ ⩽ ⟦C⟧. As we have ⟦A⟧ • ⟦A ⊸ B⟧ = ⟦A⟧ • (⟦A⟧ ⊸• ⟦B⟧) ⩽ ⟦B⟧ we can easily deduce that ⟦Γ⟧ • ⟦Δ⟧ • ⟦A ⊸ B⟧ ⩽ ⟦Δ⟧ • ⟦A⟧ • ⟦A ⊸ B⟧ ⩽ ⟦Δ⟧ • ⟦B⟧ ⩽ ⟦C⟧. □

Theorem 4 (Completeness) A is a valid formula if and only if for any interpretation σ in any quantale Q, the property e ⩽ ⟦A⟧ holds.

PROOF. This result is proved by completion of the Lindenbaum algebra in [30]. We will present another proof in the section 3.6. □

When the relation e ⩽ ⟦A⟧ holds, we say that we have a model of A and when e ⩽̸ ⟦A⟧ we call such an interpretation a counter-model.

2.4 Quantales as countermodels

Let us complete this section with some examples of quantales that are effective countermodels of some non-provable formulae of ILL. We consider the lattice and the quantale obtained by completion of the flat monoid ℤ/3ℤ (figure 2 with k = 3). If we interpret the atomic formulae in the following way: ⟦A⟧ ≜ m_{0}, ⟦B⟧ ≜ m_{1} and ⟦B⟧ ≜ m_{2}, we have ⟦A ⊕ (B & C)⟧ = ⟦A⟧ ∨ (⟦B⟧ ∧ ⟦C⟧) = m_{0} ∨ (m_{1} ∧ m_{2}) = m_{0} ∨ ⊥ = 0. Moreover, we have ⟦(A ⊕ B) & (A ⊕ C)⟧ = ⊤ ∧ ⊤ = ⊤ and consequently ⟦(A ⊕ B) & (A ⊕ C)⟧ ⩽̸ ⟦A ⊕ (B & C)⟧. Thus, this quantale is a countermodel of the distributivity of ⊕ over &.

If we consider the same lattice but with the upper bound (∨) as the monoidal operation. With the same interpretation of the atomic formulae, we have now ⟦(A ⊗ B) & (A ⊗ C)⟧ = ⊤ and ⟦A ⊗ (B & C)⟧ = 0 and then deduce that ⟦(A ⊗ B) & (A ⊗ C)⟧ ⩽̸ ⟦A ⊗ (B & C)⟧. Then, this other quantale is a countermodel of the distributivity of ⊗ over &.

These examples illustrate the general problem to build or to generate quantales as countermodels. One of our aims consists in defining appropriate semantics for ILL in order to have some simple and useful methods to generate countermodels in case of non-provability. The next section presents a new based-on resources semantics that can be seen as a first step in this direction. But let us now consider the known phase semantics.

2.5 Phase semantics: quantales as stable closures

A general method to build quantales is based on the use of the completion by a closure method, adapted to the monoidal structure. Let us remark that the phase semantics is in fact the initial semantics of Linear Logic that was presented before the algebraic semantics [14]. We will see that both semantics represent the same notion with two different approaches.

Definition 5 (Closure) Let K be any set, a closure on K is an unary operator (·)^{⋆} : ℙ(K) → ℙ(K) such that for all subsets X, Y, the equivalence X ⊆ Y^{⋆} iff X^{⋆} ⊆ Y^{⋆} holds. A (·)^{⋆}-closed subset is a subset X of the form Y^{⋆} for some Y. The subset X^{⋆} is called the closure of X and K^{⋆} denotes the set of (·)^{⋆}-closed of K.

The notion of closure is important, since it allows us to build a lattice over an order structure. We remark that there is a slight notational ambiguity here, since K is itself a subset of K, and so K^{⋆} may have two different meanings. But since the closure of K (as a subset of K) is just K itself, and hence using K^{⋆} in this sense would be redundant, this ought to cause no confusion. We also introduce an abuse of notation which does not induce ambiguities when denoting by x^{⋆} the closure {x}^{⋆} for an element x of K.

Definition 6 (Stable closure/Quantic nuclei) Let (M, •) be a monoid, a stable closure (or quantic nuclei) (·)^{⋆} is a closure on M that, for any subset X, Y of M, satisfies X^{⋆} • Y^{⋆} ⊆ (X • Y)^{⋆}.

For example, the downward closure ↓(·), defined for a preordered set (P, ⩽) and X ⊆ P by ↓X ≜ {z ∈ P | ∃x ∈ X, z ⩽ x}, is a stable closure for any preorder ⩽ compatible with • (see section 5.) Moreover, if this preordered monoid is residuated (i.e. • has a right adjoint ⊸•) then the MacNeille closure defined for X ⊆ P by X^{†} ≜ {z ∈ P | ∀k ∈ P, X ⩽ k ⇒ z ⩽ k}, is also stable (see [30].) Let us remind that the term “stable closure” comes from [29] whereas the term “quantic nuclei” comes from [28].

Definition 7 (Phase space) A triplet (M, •, (·)^{⋆}) is called an (intuitionistic) phase space if (·)^{⋆} is a stable closure on the monoid (M, •).

Given a stable closure (·)^{⋆}, we define two binary operations on the powerset ℙ(M), one denoted by (· • ·)^{⋆} and defined by the mapping (X, Y) ↦ (X • Y)^{⋆}, another denoted and defined by X ⊸• Y ≜ {x | x • X ⊆ Y }. Then (· • ·)^{⋆} is a monoidal operation on K^{⋆}, the (·)^{⋆}-closed subsets of K with unit e^{⋆} and ⊸• is a right adjoint to it. All these results are proved in Rosentahl’s book [28]. Let us remind the following results:

Proposition 8 For any X, Y the identity X^{⋆} ⊸• Y^{⋆} = X ⊸• Y^{⋆} holds and X ⊸• Y is (·)^{⋆}-closed if Y is (·)^{⋆}-closed.

Proposition 9 For any stable closure (·)^{⋆} on the monoid (M, •), the triplet (M^{⋆}, (· • ·)^{⋆}, ⊆) is a quantale. If M is finite then M^{⋆} is also finite.

We remind that, for the lattice structure, we have the identities ⊥ = ∅^{⋆}, ⊤ = M, ⋀_{i} X_{i} = ⋃_{i} X_{i} and ⋁_{i} X_{i} = (⋃_{i} X_{i})^{⋆}.

Proposition 10 Let (Q, •, ⩽) be any quantale, for a stable closure (·)^{⋆} on Q, the function x ↦ x^{⋆} is an isomorphism from Q to the quantale (Q^{⋆}, (· • ·)^{⋆}, ⊆).

An alternative proof of this proposition is given with proposition 36. The MacNeille closure is a possible choice for such a stable closure [6] and then it leads to a semantics of ILL based on phase spaces and called phase semantics [14]. Given an interpretation σ : Vars → M, we define

Phase interpretation

\begin{matrix}⟦X⟧ ≜ & σ(X)^{⋆} & ⟦A ⊸ B⟧ ≜ & ⟦A⟧ ⊸• ⟦B⟧ \\ ⟦1⟧ ≜ & e^{⋆} & ⟦A ⊗ B⟧ ≜ & (⟦A⟧ • ⟦B⟧)^{⋆} \\ ⟦⊥⟧ ≜ & ∅^{⋆} & ⟦A ⊕ B⟧ ≜ & (⟦A⟧ ∪ ⟦B⟧)^{⋆} \\ ⟦⊤⟧ ≜ & M & ⟦A & B⟧ ≜ & ⟦A⟧ ∩ ⟦B⟧ \end{matrix}

These equations can be seen as a rewriting of the quantale semantics using the particular quantale structure defined by the phase space, as in proposition 9.

Theorem 11 (Completeness) A is a valid formula if and only if for any interpretation σ in any phase space, the relation e ∈ ⟦A⟧ holds.

PROOF. This result is proved by an immediate combination of propositions 4 and 10. □

Thus, the main point here is that any quantale can be seen as a stable closure (cf. proposition 10). Moreover, with the particular choice of the MacNeille closure, we recover the completeness result of the phase semantics of ILL. We could also consider the downward closure ↓(·) and then obtain another model of ILL. But as a semantics of ILL this choice of closure has major drawbacks and the results about closures can explain for example why the Petri nets semantics of [8] is not complete w.r.t. ILL [10]. In the next sections, we analyze these semantical considerations and also propose new semantics of ILL that overcome these problems.

3 Resource semantics

This section and the next one present the main contributions of the paper about the semantics of ILL. Their consequences or relationships with other results are developed in the rest of the paper. We introduce a new semantics based on the notion of resource frame, basically a monoid and a family of its subsets. With a particular choice of closure, in fact the greatest under natural conditions, we can turn a resource frame into a phase space and then provide a soundness result. Moreover, we show that we can naturally turn the syntax (sequents and formulae) of ILL into a resource frame. Such a frame is used to prove the completeness result w.r.t. this new semantics. Moreover, the same proof, slightly modified, can also be used to provide a semantical proof of the cut-elimination theorem. In section 4, we show that this proof sketch also naturally provides the finite model property.

3.1 Resource frames

The notion of resource is an important primitive in computer science and it naturally appears in the context of substructural logics and their applications, for example in linear logic [14]. Moreover, it is used to provide so-called resource models or semantics of logics like BI (Logic of Bunched Implications)

[20] with potential applications for programming and verification. In fact, a resource semantics can elegantly explain how the logical rules deal with the formulae as resources (consumption, combinations) and can be naturally used to define (or derive) new semantic proof-search methods.

Definition 12 (Resource frame) A resource frame (M, P, •, ) is a quadruplet where (M, •) is a monoid (of resources), P is a set (of products) and ⊆ M × P is a binary relation. A frame is finite when M is finite.^{1}

1 The finiteness of M, opposed to the finiteness of P, is important because, as we

Informally, this means that we can compose resources with •, we have a void resource e and also the relation m p the meaning of which is that from the resource m we are able to produce the product p. It is important to notice that products do not have any structure and are distinct from resources in the resource semantics. Moreover they cannot be composed. For any p ∈ P, we define M_{p} ≜ {m | m p} the set of resources producing p. Then the information carried by the relation is the same as the information carried by the family (M_{p})_{p∈P}, i.e. the choice of corresponds to the choice of an arbitrary family of subsets of P. These subsets are called the base facts. Let us define the following closure operator (·)^{}on M by:

x ∈ X^{}iff ∀m, p ∈ M (m • X p ⇒ m • x p)

where m ranges over M and p over P. It means that whenever a resource x is able to produce any product that is produced by all the resources in X in any context, then x must be in the closure of X. It is easy to show that all the base facts M_{p} are (·)^{}-closed subsets as the shifted base facts that are the sets {x | m•x p} = {m}⊸•M_{p}. Then, we propose the following characterization:

Proposition 13 (·)^{}is the greatest stable closure on (M, •) for which all the base facts M_{p} are closed.

PROOF. Let us first prove that (·)^{}is a closure. It is clear that X ⊆ X^{} and that if X ⊆ Y then X^{}⊆ Y^{}. Then it remains to verify X^{}^{}⊆ X^{}. Let be x ∈ X^{}^{}, m ∈ M and p ∈ P such that m • X p. By definition of (·)^{}, m • X^{}p. As x ∈ X^{}^{}, we have m • x p and consequently (·)^{}is a closure. Let us prove now that it is stable, i.e., for any X, Y ∈ M, X • Y^{}⊆ (X • Y)^{}. Let x ∈ X and y ∈ Y^{}, and m and p such that m•(X •Y) p. As x•Y ⊆ X •Y we have m • (x • Y) p and by associativity (m • x) • Y p. As y ∈ Y^{}we deduce (m • x) • y p and finally m • (x • y) p. Thus x • y ∈ (X • Y)^{}and the closure is stable. Moreover, we observe that m • X p ⇔ X ⊆ {m} ⊸• M_{p} and consequently

X^{}= ⋂{{m} ⊸• M_{p} | m ∈ M, p ∈ P and X ⊆ {m} ⊸• M_{p}}

If (·)^{⋆} is another closure for which the M_{p} are closed then we can show that the {m} ⊸• M_{p} are also (·)^{⋆}-closed. We have X^{⋆} = ⋂{Y^{⋆}|X ⊆ Y^{⋆}} ⊆ ⋂{{m} ⊸• M_{p}|X ⊆ {m} ⊸• M_{p}} = X^{}. Thus (·)^{}is the greatest stable closure such that the M_{p} are closed. □

As a consequence we can build a quantale on the top of the set of (·)^{}-closed subsets by application of proposition 9. This quantale is finite if and only if

will see later, it implies the finiteness of the quantale we build from the resource frame (M, P, •, ).

M is finite. Thus we can deduce another new semantics of ILL.

3.2 Examples

We present two examples of quantales we obtained with the preceding construction. Here we only give the lattice structure. Let M be the monoid ℤ/3ℤ = {0, 1, 2} (the cyclic group of order 3). We represent the relation ⊆ M × P by its sections M_{p} which are subsets of M. In this example, the sections are exactly the singletons {0}, {1} and {2}. We obtain the least possible completion lattice (see subsection 5.3).

⟶^{(·)^{}}

In the second example, there are two sections {0, 1} and {1, 2}. In this case, we obtain the greatest possible completion lattice (see subsection 5.3).

⟶^{(·)^{}}

3.3 Interpretation of ILL

If we consider the monoid (M, •) with the stable closure (·)^{}, we obtain a sound semantics for ILL by the soundness result of proposition 11. By making explicit the semantical equations of the phase interpretation, we obtain the following definitions. Let σ : Vars → P be an interpretation of variables, we have

Resource frame interpretation

\begin{matrix}⟦X⟧ ≜ & \{m | m σ(X)\} & ⟦A ⊸ B⟧ ≜ & ⟦A⟧ ⊸• ⟦B⟧ \\ ⟦⊤⟧ ≜ & M & ⟦A & B⟧ ≜ & ⟦A⟧ ∩ ⟦B⟧ \end{matrix} ; \begin{matrix}⟦⊥⟧ ≜ & \{x | ∀m, p m • x p\} \\ ⟦1⟧ ≜ & \{x | ∀m, p (m p ⇒ m • x p)\} \\ ⟦A ⊗ B⟧ ≜ & \{x | ∀m, p (m • ⟦A⟧ • ⟦B⟧ p ⇒ m • x p)\} \\ ⟦A ⊕ B⟧ ≜ & \{x | ∀m, p (m • ⟦A⟧ p and m • ⟦B⟧ p ⇒ m • x p)\} \end{matrix}

Let us give some informal explanations about this semantics. For example, a resource x can produce A ⊗ B (i.e. x ∈ ⟦A ⊗ B⟧) if for any context m of resources it can produce all the products that can be produced in the same context by any binary combination of the resources in ⟦A⟧ and ⟦B⟧. For A⊕B, we do not take into account the combination but the union of resources. The resources for ⊥ are those that produce anything in any context.

Theorem 14 (Soundness) If Γ ⊩ B then ⟦Γ⟧ ⩽ ⟦B⟧.

PROOF. This semantics is in fact a particular case of the phase semantics applied to the phase space (M, •, (·)^{}) which is sound by proposition 11. □

3.4 Closures as frames

Let (M, •) be a monoid and (·)^{⋆} be a stable closure over M. Then the quadruplet (M, M^{⋆}, •, ∈) is a resource frame.^{2} Moreover, it is straightforward to verify that for all X ⊆ M, we have the identity X^{⋆} = X^{∈}. Then the phase interpretation (see section 2.5) and the frame interpretation (see section 3.3) coincide because they are based on the same phase space. Thus, we obtain a completeness result.

Theorem 15 (Completeness) A is a valid formula if and only if for any interpretation σ in any resource frame, the relation e ∈ ⟦A⟧ holds.

PROOF. The proof can be achieved using the preceding frame and the completeness for phase spaces but our claim is that we have a more natural and

2 The symbol ∈ denotes the set ownership between the elements of M and the (·)^{⋆}-closed subsets of M.

direct way to prove the completeness of ILL w.r.t. the resource frame semantics. It is detailed in the following subsections. □

Let us remind that the proof-search method is a natural completeness proof method that has been applied to various logics like classical, intuitionistic or modal logics. It consists of two steps: a) to prove that for any provable formula (or sequent) there exists such a branch (called open branch) in a proof-search tree that does not reach an axiom and that contains enough information to refute the formula and b) to show the construction of a countermodel of the formula from such an open branch. In fact this based-on proof-search method and the standard construction of countermodels are not directly applicable to linear logic but some solutions have been proposed for both intuitionistic and classical linear logics from phase semantics [21]. Here we present another method based on proof-search from the resource semantics we have defined.

3.5 Syntactic resource frame models

Let M be the monoid Contexts, we denote by Γ • Σ the juxtaposition of two contexts that are multisets of formulae. It is usually denoted by Γ, Σ in the sequent calculus but here we choose a less ambiguous notation. As a formula A can be confused with the context with only one formula A, we define the identity map ⌊·⌋ : Contexts → Contexts and we write ⌊A⌋, forcing A to be considered as a context for a type-related reason. Then ⌊A_{1}, …, A_{n}⌋ is the context consisting of n formulae.^{3}

Let ⊆ Contexts×Forms be a binary relation, then we obtain a resource frame (Contexts, Forms, •, ). But we have to consider specific arbitrary relations.

Definition 16 (ILL_{wc}-closed relation) An ILL_{wc}-closed relation is a binary relation ⊆ Contexts × Forms which is closed under the rules of cut-free ILL.

Definition 17 (Syntactic resource frame) A syntactic resource frame is a frame of the form (Contexts, Forms, •, ) where is an ILL_{wc}-closed relation.

An example of ILL_{wc}-closed relation is the cut-free provability of sequents denoted by ⊩_{wc}. We can also mention the validity (i.e. the provability with the [cut]-rule) which is denoted ⊩. We will introduce other ILL_{wc}-closed relations defined by so-called refutation trees in section 4.1.

3 The reader might wonder why we introduce a notation that might appear as redundant. Apart from removing an ambiguity, we point out that we will give another meaning to ⌊·⌋ in the section 4.2.

Let (Contexts, Forms, •, ) be a given syntactic frame, we aim to study the semantic properties of such a model.^{4} In this setting, we have the following identity Contexts_{A} = \{Γ | Γ A\} and moreover we define \underline{A} ≜ Contexts_{A} for a shorter notation. \underline{A} is a (·)^{}-closed subset of Contexts by proposition 13. The following relations just give a based-on semantics rewriting of the logical rules, except for the [cut]-rule.

Proposition 18 For any ILL_{wc}-closed relation and any formulae A and B, the following relations hold:

[id] ⌊A⌋ ∈ \underline{A}
[1_{L}] ⌊1⌋ ∈ \{∅\}^{}[1_{R}] ∅ ∈ \underline{1}
[⊥_{L}] ⌊⊥⌋ ∈ ∅^{}[⊤_{R}] Contexts ⊆ \underline{⊤}
[⊗_{L}] ⌊A ⊗ B⌋ ∈ ⌊A, B⌋^{}[⊗_{R}] \underline{A} • \underline{B} ⊆ \underline{A ⊗ B}
[⊕_{L}] ⌊A ⊕ B⌋ ∈ \{⌊A⌋, ⌊B⌋\}^{}[⊕_{R}^{1,2}] \underline{A} ∪ \underline{B} ⊆ \underline{A ⊕ B}
[&_{L}^{1,2}] ⌊A & B⌋ ∈ ⌊A⌋^{}∩ ⌊B⌋^{}[&_{R}] \underline{A} ∩ \underline{B} ⊆ \underline{A & B}
[⊸_{L}] ⌊A ⊸ B⌋ ∈ \underline{A} ⊸• ⌊B⌋^{}[⊸_{R}] \{⌊A⌋\} ⊸• \underline{B} ⊆ \underline{A ⊸ B}

PROOF. Each relation exactly corresponds to one instance of a rule of the cut-free ILL (which is mentioned on the left of the arrays). For example, for [id], we obtain ⌊A⌋ A which exactly means that is closed for the rule [id]. We can view these relations as an explicit presentation of the definition of the ILL_{wc}-closed relation. Let us consider another case: the property ⌊A ⊗ B⌋ ∈ ⌊A, B⌋^{}expands (by definition of the closure (·)^{}) into ∀ Γ, C (Γ, A, B C ⇒ Γ, A⊗B C) which is exactly the meaning of the logical rule [⊗_{L}]. On the other hand, \underline{A}•\underline{B} ⊆ \underline{A ⊗ B} means that for any Γ, Δ such that Γ A and Δ B hold, the relation Γ, Δ A⊗B holds, and it is in fact the meaning of the rule [⊗_{R}]. □

Now we can give a semantics to the ILL formulae by simply interpreting variables by themselves, which is the same trick used in the Lindenbaum algebra construction. Let σ(X) = X ∈ Forms, we obtain the following result for the semantics in the (Contexts, Forms, •, ) resource frame.

Lemma 19 For any formula A, the relation ⌊A⌋ ∈ ⟦A⟧ ⊆ \underline{A} holds.

PROOF. By induction on A using the relations already proved in proposition

4 This model is just a kind of Lindenbaum algebra [6,26] which has been tuned to fit with the cut-free ILL.

18. The base case is when A is a variable or a constant and the corresponding relations are [id], [1_{L}], [1_{R}], [⊥_{L}] and [⊤_{R}]. Let us consider the case of ⊗. By induction hypothesis, the relations ⌊A⌋ ∈ ⟦A⟧ and ⌊B⌋ ∈ ⟦B⟧ hold. Then we have ⌊A, B⌋ = ⌊A⌋ • ⌊B⌋ ∈ ⟦A⟧ • ⟦B⟧. Then we get ⌊A ⊗ B⌋ ∈ ⌊A, B⌋^{}⊆ (⟦A⟧ • ⟦B⟧)^{}= ⟦A ⊗ B⟧ by the relation [⊗_{L}] in proposition 18. On the other hand, we have the two induction hypothesis ⟦A⟧ ⊆ \underline{A} and ⟦B⟧ ⊆ \underline{B}. Thus, ⟦A⟧ • ⟦B⟧ ⊆ \underline{A} • \underline{B} ⊆ \underline{A ⊗ B} by the relation [⊗_{R}] in proposition 18. Since \underline{A ⊗ B} is (·)^{}-closed by proposition 13, we have ⟦A ⊗ B⟧ = (⟦A⟧ • ⟦B⟧)^{}⊆ (\underline{A ⊗ B})^{}= \underline{A ⊗ B}. □

Let us give some comments about this result. It is very closed to the usual identity for the Lindenbaum algebra that would be ⟦A⟧ = \underline{A} but it is in fact stronger because the proof does not involve the use of the [cut]-rule that is necessary to give the order structure to the Lindenbaum algebra. The technique we use has been introduced in [21] for classical linear logic and extended to the intuitionistic case in [22], but in the specific case of phase semantics.

3.6 Completeness and cut-elimination

As a direct application of the syntactic models, we obtain the very important result of completeness with a simple and short proof.

Theorem 20 (Completeness) If the sequent ⊢A is not provable in ILL, then there exists a resource frame countermodel of the formula A.

PROOF. We choose to be the validity ⊩ in ILL. This is an ILL_{wc}-closed relation. Then the empty context ∅ does not belong to \underline{A} because otherwise ∅ ⊩ A and then ⊢A is provable. By lemma 19, ∅ ∉ ⟦A⟧ and consequently we have a countermodel of A. □

This is the usual result of the Lindenbaum construction. Here we have not stated neither proved the soundness part of the result, because this is already done in proposition 14.

Theorem 21 (Cut elimination) If the sequent ⊢A is provable with the [cut] rule, then it is also provable without this rule.

PROOF. We choose to be ⊩_{wc}, i.e. the validity in the cut-free ILL. This is the least ILL_{wc}-closed relation. If ⊢A is not provable without the [cut] rule, then ∅ ∉ \underline{A} holds, and thus ∅ ∉ ⟦A⟧ holds too and we have a countermodel of A. From the soundness theorem of the resource semantics we can deduce that ⊢A is not provable with the [cut] rule. □

4 Finite countermodels as refutation trees

On the syntactic side, the [cut]-elimination result can be considered as the basic argument for the decidability of a logic, being combined with a proof-search algorithm. On the semantic side, the most important argument for decidability is the finite model property. The results of the following section present a strong link between the two notions putting forward the idea that backward proof-search can be used to build finite counter-models [11,25], even in linear logic.

We introduce the notion of finite refutation tree which can be seen as dual to the notion of proof tree. The idea is to construct, for a given unprovable sequent, a so-called refutation tree which retains enough information to refute this sequent. It arises as the search space of a proof-search algorithm with some unprovable sequent as input. From a finite refutation tree, we can cut down the syntactic resource frame to a finite structure, by identifying the resources outside the refutation tree, but also preserving the semantic properties. Therefore, we obtain a finite counter-model.

4.1 Refutation trees

A proof is a sequent-indexed tree such that each node corresponds to the application of one logical rule and the sons of this node are indexed by the premises of this rule. A refutation tree can be seen as a dual notion: in such a tree there is a son for each applicable logical rule and such a son is indexed by one of the premises of the rule. The sequents indexing the proof trees are provable whereas the sequents indexing the (finite) refutation trees are unprovable.

Definition 22 (Refutation tree) A refutation tree is a sequent-indexed tree such that if f is a node indexed by the sequent C, f has exactly one son s for each instance of a logical rule with conclusion C and this node s is indexed by one of the premise of this rule.

This notion is very general and can be applied to any sequent calculus. Here we only consider the cut-free ILL sequent calculus. As an example, let us suppose that f is a node of a refutation tree indexed by the sequent A ⊕ B, C ⊢ D. Then, as the rule

\begin{matrix}A, C ⊢ D & B, C ⊢ D \\ A ⊕ B, C ⊢ D \end{matrix}

is an instance of the [⊕_{L}] rule, there is a son s of f which is indexed by either A, C ⊢ D or B, C ⊢ D. An axiom is a rule with no premise so the conclusion of an axiom cannot be the index of a node in a refutation tree.

Let R be a given refutation tree, we denote by S ∈ R when S is a sequent indexing at least one node in R and by S ∉ R when the sequent S is not the index of any node in R. We define a unary^{5} relation on the set of sequents by:

S iff S ∉ R

Proposition 23 The relation is closed with respect to the logical rules.

PROOF. This result is better explained with the following diagram:

\begin{aligned}H_{1} & … & H_{n} \\ & S \end{aligned} implies \begin{aligned}H_{1} & … & H_{n} \\ & S \end{aligned}

Then we consider the preceding instance of a logical rule and we suppose that the H_{i} are sequents such that H_{i} for any i. To prove S, we suppose that S is the index of a node f in R. Then, as R is a refutation tree, one of the H_{i}, namely H_{i_{0}} is the index of a son of f. It is not possible because H_{i_{0}}. Therefore S is not in R and then S. □

This result is important because it means that in the case of refutation tree for cut-free ILL, we can use as a particular ILL_{wc}-closed relation. We now prove the existence of finite refutation trees. This is not true for any logical system but it is true for the cut-free ILL.

Proposition 24 If a sequent is not provable in the cut-free ILL, then it is the index of the root of a finite refutation tree.

PROOF. We proceed by induction on unprovable sequents. Let S be a sequent which is not provable. Then, there is only a finite number of instance of logical rules of cut-free ILL with S as conclusion. For any of these rules, at least one of its premises is not provable otherwise the rule could be used as the last in a proof of S. We choose one premise H_{r} for each rule instance r.

5 We intentionally use the same symbol as in section 3.5 where was an ILL_{wc}- closed binary relation. Here we have a unary relation but over sequents, which are pairs in the case of ILL.

Each H_{r} is an unprovable sequent which is simpler ^{6} than S. So we build by induction a H_{r}-rooted finite refutation tree for each unprovable H_{r}. Then we collapse all these trees in a S-rooted refutation tree. □

In the rest of the paper, the refutation tree obtained with this construction from an unprovable Γ ⊢ A will be called the refutation tree of the sequent Γ ⊢ A.

4.2 Finite quotient frame of contexts

In this section, we consider a fixed (finite) refutation tree R for cut-free ILL. We describe how to build a finite resource frame model from such a refutation tree. It corresponds to a countermodel construction for ILL. We first define a quotient monoid identifying all the contexts that do not appear as sub-contexts in the indexes of the tree R. Let us choose a variable X which does not appear in any sequent indexing the nodes of R. Let Π be the context {X} and let us remind that Γ ⊢ A ∈ R means that the sequent Γ ⊢ A is an index in R. We define

Contexts_{R} ≜ {Γ | ∃Σ, A such that Σ, Γ ⊢ A ∈ R}
M ≜ Contexts_{R} ∪ {Π}

As there are only finite numbers of indexes R and subcontexts for a given context, M is finite. The relation Π ∉ Contexts_{R} holds. Thus we can define the following projection ⌊·⌋ : Contexts → M that exactly identifies the contexts that are not in Contexts_{R}:

⌊Γ⌋ ≜ \{ \begin{matrix}Γ if Γ ∈ Contexts_{R} \\ Π otherwise \end{matrix}

Let us remind that the notation ⌊Γ⌋ is used to distinguish multisets from formulae. Now, we have a projection on a finite subset of Contexts and M inherits the monoidal structure of Contexts with the following relation ⌊Γ⌋ • ⌊Σ⌋ = ⌊Γ, Σ⌋.

We define the relation ⊆ Contexts × Forms by Γ A iff Γ ⊢ A ∉ R holds. By proposition 23, we obtain an ILL_{wc}-closed relation. Then, we define the quotient relation (we use the same symbol) ⊆ M×Forms by the equivalence

6 We mean that the linear complexity of the sequent is smaller. It is true for the cut-free ILL without exponentials but false with them.

⌊Γ⌋ A iff Γ A. Therefore we obtain a finite resource frame (M, Forms, •, ) because M is finite.

4.3 Finite model property of resource semantics

There have been a few results on the finite model property of substructural logics [24]. A usual way for other logics is to prove the completeness theorem and to get a frame in which an unprovable formula A is not valid. Then we extract a finite frame from that frame in which A is not valid either. But it is in fact difficult to get such a frame in the case of substructural logics like linear logic fragments even if there exist some results based on phase models and quotient structures [15] or on co-finite powerset models and barriers structures [5]. Here, we consider a based-on proof-search approach with so-called refutation tree and a resource frame construction [21]. We describe how to construct a finite resource frame from a given refutation tree. If we interpret ILL in this frame then we obtain the finite model property. Indeed, it is routine to check that the equations of proposition 18 hold for our quotient frame with our projection ⌊·⌋. Let us remind that the property, if ⌊m⌋ = ⌊m⌋′ then ∀p ∈ Forms m p ⇔ m′ p, is the key property to obtain the appropriate quotient frame. Then the equation ⌊A⌋ ∈ ⟦A⟧ ⊆ \underline{A} of proposition 19 holds too.

Theorem 25 (Finite model property) If ⊢A is not provable in ILL, then there is a finite resource frame which is a countermodel of ⊢A.

PROOF. Let ⊢A be an unprovable sequent in cut-free ILL, we have a finite refutation tree R of the sequent ⊢A by the proposition 24. From this tree, we are able to build a finite frame (M, Forms, •, ) following the previous approach. Then since ⊢A ∈ R and ∅ ∈ Contexts_{R}, the relation ∅ A does not hold and thus ∅ ∉ ⟦A⟧ because ∅ ∉ \underline{A}. □

From this result, we can deduce a new way to construct some counter-models for ILL formulae. We have to build a finite refutation tree for a given sequent and then to generate a quotient syntactic resource frame. Even if it is out of the purpose of the paper, it will be important to study in further work this based-on proof-search procedure for countermodels construction from different points of view: complexity, mechanization, comparison with the structures and proposals of [21] based on phase semantics.

4.4 Finite model property of other semantics

Another important consequence of this result is that we can deduce the completeness and the finite model property for the different semantics of ILL we have considered in previous sections.

Theorem 26 The quantale interpretation and the phase interpretation of ILL satisfy the finite model property.

PROOF. The resource frame interpretation of ILL is just a particular case of a phase interpretation which is itself a particular case of quantale interpretation, and these two embeddings preserve finiteness. Let us remind that if (M, P, •, ) is the resource frame then (M, •, (·)^{}) is the corresponding phase space and (M^{}, (· • ·)^{}, ⊆) is the corresponding quantale. □

This important finite model property has been established for the classical linear logic in [15]. More recently it has been proved for the intuitionistic case using a technique based on proof search with phase semantics and socalled OR-tree structure [22]. Our approach combines the use of the resource semantics and quotient structures with an approach similar to [15] in order to prove the result. The notion of refutation tree (or OR tree in [22]) is central for the intuitionistic case whereas [15] used the restricted notion of proof space branch in the classical case. Such a notion of refutation tree also provides an effective way to generate countermodels. Here we have shown the strong link between the finite model property (a notion of model theory connected to decidability) and refutation trees (a notion of proof theory derived from backward proof-search algorithms).

5 Preordered monoid semantics

We introduce the notion of (pre)ordered monoid as the basis for a new semantics for ILL. The basic idea is to view it as a partially specified quantale, with a possible lack of lattice structure. The next step is to extend preordered monoids to quantale preserving the order structure as much as possible. Therefore, we give an algebraic characterization of a particular type of extension called ∨-completion that can be obtained by application of particular closures, called pretopologies. There is a least ∨-completion that corresponds to the greatest pretopology and this extension preserves enough of the order structure to ensure the completeness result and the finite model property. We can see the preordered monoid semantics as a specific case of the resource semantics where products and resources are of the same kind.

5.1 Preordered monoids and ∨-completions

Definition 27 ((Pre)ordered monoid) A (pre)ordered monoid is a triplet (M, •, ⩽) such that (M, •) is a monoid with unit e,(M, ⩽) is a (pre)ordered set and such that for all x, a, b ∈ M if a ⩽ b then x • a ⩽ x • b and if a ⩽ b then a • x ⩽ b • x.

This property is simply the fact that for any fixed x, the operation x • (·) is monotone w.r.t. the preorder (M, ⩽). Obviously, an ordered monoid is a preordered monoid. We write a ≃ b when both a ⩽ b and b ⩽ a hold. In the case of an ordered set, this relation corresponds to equality (by antisymmetry.) We also write a ≃ ⋁_{i} b_{i} (resp. a ≃ ⋀_{i} b_{i}) when a is a least upper bound (resp. greatest lower bound) of the b_{i}’s. This least upper bound (resp. greatest lower bound) is unique up to the equivalence ≃.

An embedding from the preordered monoid M to M′ is a function i : M → M′ such that for any x, y ∈ M, the equivalence x ⩽ y iff i(x) ⩽ i(y) holds and the relations i(x • y) ≃ i(x) • i(y) and i(e_{M}) ≃ e_{M′} hold too. i is called an equivalence of preordered sets if for any m′ ∈ M′ there exists some m ∈ M such that i(m) ≃ m′. In the case of ordered sets, an embedding is an injective map and an equivalence is an isomorphism.

≃ is an equivalence relation which is a congruence w.r.t. the monoidal operation •. If we denote by [a] the equivalence class of a then we can define a monoidal operation on the set of equivalence classes M/≃ by [x]•[y] ≜ [x•y]. Moreover the classes are ordered by the relation [x] ⩽ [y] iff x ⩽ y.

Proposition 28 Let (M, •, ⩽) be a preordered monoid, the following quotient (M/≃, •, ⩽) is an ordered monoid and x ↦ [x] is an equivalence of preordered monoids.

This trivial result shows that we can either consider preordered monoids (which arise naturally when we consider Petri nets, see section 6) or restrict to ordered monoids.

5.2 Pretopologies

In the next paragraphs, we consider extensions of a given preordered monoid (M, •, ⩽).

Definition 29 (Compatible closure, pretopology) A closure (·)^{⋆} is said compatible when for any element x ∈ M, the identity x^{⋆} = ↓x holds. A pretopology is a closure which is compatible, i.e., ∀x ∈ M, x^{⋆} = ↓x and stable, i.e., ∀X, Y ⊆ M, X^{⋆} • Y^{⋆} ⊆ (X • Y)^{⋆}.

For instance, the closure ↓(·) is a pretopology (see [29]). Pretopologies form a complete lattice under set inclusion ⊆. The extremal elements are presented below. The least one is very well-known whereas the greatest one “looks like” a kind a MacNeille closure. This pretopology seems to be first appeared in [23] but it is not characterized as the greatest pretopology.

Proposition 30 The pretopologies ↓(·) and (·)^{∘} defined below are the least and greatest pretopologies over M.

Least pretopology  ↓X ≜ {z | ∃x ∈ X, z ⩽ x}
Greatest pretopology X^{∘} ≜ {z | ∀m, k ∈ M m • X ⩽ k ⇒ m • z ⩽ k}

PROOF. Indeed, ↓(·) is obviously the least pretopology. For (·)^{∘}, if we consider the resource frame (M, M, •, ⩽) then we obtain the identity (·)^{⩽} = (·)^{∘} and thus (·)^{∘} is a stable closure by proposition 13. Moreover the equality x^{∘} = ↓x is trivial. Consequently (·)^{∘} is a pretopology. Given another pretopology (·)^{⋆}, it stabilizes all the ↓x, i.e. all the ↓x are (·)^{⋆}-closed. It is also a stable closure. Let us consider the frame (M, M, •, ⩽), since M_{x} = ↓x we deduce, by proposition 13, that (·)^{⋆} is smaller than (·)^{⩽} as an M_{x}-preserving stable closure. □

In fact, any closure can be considered as being compatible with a certain preorder relation. Given a closure (·)^{⋆} on P, we can define the following preorder ⩽ on P : X ⩽ Y iff X^{⋆} ⊆ Y^{⋆}. Moreover, we can remark that (·)^{⋆} is compatible with this preorder: X^{⋆} = ↓X. But if the preorder is characterized by the closure (with this relation) then we may notice that, on the contrary, the closure is not characterized by the preorder. In the initial proof of the completeness w.r.t. phase semantics, one has the monoid of contexts (i.e. multisets of formulae) and • is simply the union (or superposition) of contexts. Then, we consider the entailment relation (a preorder) between contexts and we choose the MacNeille closure (relatively to entailment). It is exactly the largest closure compatible with entailment. Therefore, we deal with a hidden (pre)order and the closure is built from it. But if the MacNeille closure works very well for the completeness theorem, it does not work in the general case because the entailment is a particular preorder.

5.3 ∨-completions as pretopologies

Definition 31 (Category of ∨-completions) A ∨-completion of the preordered monoid M is a quadruplet (Q, •, ⩽, i) such that (Q, •, ⩽) is a quantale and i : M → Q is a ∨-dense embedding. A morphism f between two ∨-completions Q and Q′ of M is a ∨-preserving poset morphism f : Q → Q′ such that i′ = f ∘ i.

The density condition for the embedding i means that for any q ∈ Q there exists a family (m_{k})_{k∈M} such that q = ⋁_{k} i(m_{k}), i.e. any element in the ∨- completion is “a least upper bound of some elements” in M. It is trivial to prove that this definition gives rise to a category.

Proposition 32 Let (·)^{⋆} be a pretopology, the structure (M^{⋆}, (· • ·)^{⋆}, ⊆) is a quantale. Each element X^{⋆} of this quantale is a downward closed subset of (M, ⩽). The map i : M → M^{⋆} defined by i(x) = ↓x is a ∨-dense embedding.

PROOF. The density property comes from the identity X^{⋆} = (↓X)^{⋆} = (⋃_{x∈X} ↓x)^{⋆} = ⋁_{x∈X} ↓x. □

Then we build a ∨-completion of M from a pretopology and whichever the ordered monoid M, we always can consider the extremal pretopologies ↓(·) and (·)^{∘}.

For the reader aware of category theory, we point out the following algebraic characterization which expresses the fact that pretopologies and ∨-completions are essentially the same concept.

Proposition 33 The map (·)^{⋆} ↦ (M^{⋆}, (· • ·)^{⋆}, ⊆, x ↦ ↓x) defines an equivalence (of categories) between the complete lattice of pretopologies and the category of ∨-completions of M.

PROOF. A proof of this result is given in [16]. This is a generalization of the correspondence between completions of posets into ∨-lattices and compatible closures [4], the corresponding greatest closure being the MacNeille closure [6]. □

We do not give the detailed proof and do not define the notion of equivalence of categories because it leads to the introduction of a lot of categorical vocabulary in order to state and prove a result which is not central for the rest of the paper. However, we claim that it clarifies the link between the concrete notion of pretopology and the abstract notion of ∨-completion (see [16]).

5.4 Properties of the greatest pretopology

Proposition 34 Let (M, •, ⩽) by a preordered monoid, and (·)^{⋆} be a pretopology on M. The following properties hold

1) If a ≃ ⋀_{i} b_{i} then a^{⋆} = ⋀ b_{i}^{⋆}
2) (b • c)^{⋆} = (b^{⋆} • c^{⋆})^{⋆} and e^{⋆} is the unit in M^{⋆}
3) If a ≃ b ⊸• c then a^{⋆} = b^{⋆} ⊸• c^{⋆}
4) If ⊤ is a greatest element in M then ⊤^{⋆} is the greatest element.

PROOF. The proofs are straightforward. We can see that most of a preexisting partial quantale structure is preserved by (·)^{⋆}-completion and it only remains the cases of least upper bounds and smallest elements. As a first observation, we point out the fact that they cannot always be preserved because infinite distributivity does not always hold in preordered monoids. Thus, preserved least upper bounds should at least verify infinite distributivity. This necessary condition is a sufficient condition for the (·)^{∘}-completion. □

Proposition 35 If a ≃ ⋁_{i} b_{i} in M and this least upper bound is distributive, i.e. for all x in M x • a ≃ ⋁_{i} x • b_{i} then we have a^{∘} = ⋁_{i} b_{i}^{∘}.

PROOF. Let us first prove that for any X ⊆ M, the equivalence a ∈ X^{∘} ⇔ ∀i b_{i} ∈ X^{∘} holds. The direct side is trivial but the reverse is more tricky. We assume that m • X ⩽ k holds. Then, as b_{i} ∈ X^{∘}, we have m • b_{i} ⩽ k for any b_{i} and thus m • a ⩽ k since m • a ≃ ⋁_{i} m • b_{i} holds by hypothesis, for any m, k and a ∈ X^{∘}. We finally obtain the equivalence a^{∘} ⊆ X^{∘} ⇔ a ∈ X^{∘} ⇔ ∀i b_{i} ∈ X^{∘} ⇔ ⋃_{i} b_{i}^{∘} ⊆ X^{∘} ⇔ ⋁_{i} b_{i}^{∘} ⊆ X^{∘} and consequently a^{∘} = ⋁_{i} b_{i}^{∘}. □

As a remark, we observe that ⊥ may not be preserved if it exists.^{7} We obtain the condition x • ⊥ ⩽ ⊥ which is not always verified for ordered monoids, but is verified in quantales. The greatest pretopology defines a surjection that is a projection of preordered monoids onto quantales.

7 We remind that ⊥ is a particular case of a least upper bound with an empty family.

Proposition 36 If (Q, •, ⩽) is a preordered monoid which is a quantale then x ↦ ↓x is a quantale isomorphism from Q to (Q^{∘}, (· • ·)^{∘}, ⊆).

PROOF. Indeed by propositions 34 and 35 and the equality ↓x = x^{∘}, it is clear that the embedding x ↦ ↓x is also an embedding of quantales, i.e. all the algebraic structure is preserved. We only have to prove that x ↦ ↓x is a surjection. But the property X^{∘} = ↓(⋁ X) holds because X ⩽ ⋁ X and ⋁ X ∈ X^{∘}. Thus, any (·)^{∘}-closed subset is an image by x ↦ ↓x. □

5.5 Interpretation of ILL

Given a preordered monoid (M, •, ⩽), we build the quantale (M^{∘}, (· • ·)^{∘}, ⊆) obtained by completion with the greatest pretopology (·)^{∘}. This provides a sound interpretation of ILL, i.e. a semantics based on preordered monoids with the following equations. Let σ : Vars → M be an interpretation of the logical variables.

Preordered monoid interpretation

\begin{matrix}⟦X⟧ ≜ & ↓σ(X) & ⟦A ⊸ B⟧ ≜ & ⟦A⟧ ⊸• ⟦B⟧ \\ ⟦⊤⟧ ≜ & M & ⟦A & B⟧ ≜ & ⟦A⟧ ∩ ⟦B⟧ \\ ⟦1⟧ ≜ & ↓e & ⟦⊥⟧ ≜ & \{x | ∀m, p m • x ⩽ p\} \end{matrix} ; \begin{matrix}⟦A ⊗ B⟧ ≜ & \{x | ∀m, p (m • ⟦A⟧ • ⟦B⟧ ⩽ p ⇒ m • x ⩽ p)\} \\ ⟦A ⊕ B⟧ ≜ & \{x | ∀m, p (m • ⟦A⟧ ⩽ p and m • ⟦B⟧ ⩽ p ⇒ m • x ⩽ p)\} \end{matrix}

Again we can see these equations as a rewriting of the interpretation of ILL based on phase spaces, from an adequate adaptation to the particular case of the greatest pretopology (·)^{∘}.

Theorem 37 (Completeness and finite model property) The interpretation of ILL based on (pre)ordered monoids is complete and has the finite model property, i.e. if ⊮A holds then there exists a finite (pre)ordered monoid M and a valuation σ : Vars → M such that e ∉ ⟦A⟧.

PROOF. By proposition 26, there exists a finite quantale (Q, •, ⩽) and a valuation σ : Vars → M such that e ⩽̸ ⟦A⟧. By proposition 36, we consider the quantale (Q^{∘}, (· • ·)^{∘}, ⊆) and we define σ′ ≜ σ. We denote ⟦·⟧′ the (pre)ordered monoid semantics defined over Q (considered here as a (pre)ordered monoid) by σ′. The property ⟦F ⟧′ = ↓⟦F ⟧ is trivially proved and therefore e ∉ ⟦A⟧′ holds because e ⩽̸ ⟦A⟧ holds. □

Definition 38 (Equivalence between interpretations) A function i : M_{1} → M_{2} is called an equivalence between the interpretations σ_{1} : Vars → M_{1} and σ_{2} : Vars → M_{2} if i is a preordered monoid equivalence and if for any variable X, the property σ_{2}(X) ≃ i(σ_{1}(X)) holds.

Proposition 39 Let i : M_{1} → M_{2} be an equivalence between σ_{1} and σ_{2} and (·)^{⋆} be either ↓(·) or (·)^{∘}. If we denote by ⟦·⟧_{1} and ⟦·⟧_{2} the respective interpretations in M_{1} and M_{2} corresponding to (·)^{⋆}, then for any formula F, ⟦F ⟧_{2} = ↓(⟦F ⟧_{1}) holds.

PROOF. By a structural induction on F and the fact that equivalent elements cannot be distinguished by the formulae defining the interpretation. □

This last result tells indicates that equivalent interpretations define the same semantics. Combined with proposition 28, we deduce that, from the point of view of ILL semantics, the notions of preordered monoids and of ordered monoids can be interchanged.

5.6 Some examples

In this section we apply our greatest pretopology construction to build examples of quantales. Proofs are left to the reader.

\begin{matrix}(ℕ, +, ⩽) & ⟶^{(·)^{∘}} & (\{[0, n[ | n ∈ ℕ\}, +, ⊆) \\ (ℚ, +, ⩽) & ⟶^{(·)^{∘}} & (ℝ ∪ \{−∞, +∞\}, +, ⩽) \end{matrix}

The case of ℕ is interesting because the least element 0 is not preserved as an example of what we said in section 5.4. A trivial method to build ordered monoids is to consider the flat order structure on any monoid. Even though the order is the same in all cases, the obtained lattice is not always the same. The situation is different with ↓(·) because the lattice structure is in this case independent of the monoidal structure, and with a flat monoid, we obtain a powerset for the lattice structure.

Proposition 40 If the flat monoid M is regular then M^{∘} = M ∪ {⊥, ⊤} with ⊥ • x = ⊥ and for x ≠ ⊥, ⊤ • x = ⊤.

A monoid is regular if • can be cancelled, i.e. a • x = b • x implies a = b. This is the case for free monoids (multisets) like ℕ or for groups like ℤ/kℤ but there are monoids that are not regular. The structure obtained by completion is described by the following figure.

\begin{aligned}⊥ • & ⊤ & = & ⊥ \\ m • & ⊤ & = & ⊤ \\ m • & ⊥ & = & ⊥ \end{aligned}

Thus we obtain a non-distributive lattice and the quantale can be seen as a countermodel of the distributivity of ⊕ over & in ILL, i.e. of the linear sequent (X ⊕ Y) & Z ⊢ (X ⊕ Z) & (Y ⊕ Z) .

As an example of non-regular flat monoid, we can consider for a fixed natural n the monoid ([0, n], max). It is not regular because max(0, n) = max(1, n). The structure obtained is described in the next figure for n = 3. We can show that ∅^{∘} = ∅, x^{∘} = {x} and if X has more than two elements then X^{∘} = [0, max X].

([0, 3], max, flat)^{∘}

Proposition 41 There are ordered monoids for which the MacNeille closure is not stable.

PROOF. We show that the MacNeille closure (·)^{∘} is not stable on the previous ordered monoid ([0, 3], max, flat). It means that it does not satisfy the property X • Y^{†} ⊆ (X • Y)^{†} . Indeed, {0, 1}^{∘} = [0, 3] because 0 and 1 have no common upper bound in the flat order. But {2}max{0, 1} = {2}. Then {2}max{0, 1}^{∘} = {2, 3} ⊈ {2} = ({2}max{0, 1})^{∘}. □

6 Petri nets semantics

Petri nets can naturally be made into models of ILL in such a way that many properties of nets we aim to state be expressible in linear logic [7,8]. But the question of the completeness for the logic w.r.t. Petri nets arose and has been addressed in [8]. In fact, Petri nets form a sound and complete model for the ⊕-free fragment of ILL (without the exponential !). For the ⊸-free logic an extra axiom of distributivity of & over ⊕ is necessary in order to obtain a completeness result. In fact, the strongest completeness result for the full logic involves the addition of axioms to the Petri nets semantics [8]. One of our aims is to understand this problem related to the Petri nets semantics and precisely why a completeness result cannot be naturally obtained. This point is in fact in background of the semantical developments of this paper. We present in this section a new based-on Petri nets semantics for ILL where Petri nets appear as concrete representations of preordered monoids, at least up to an equivalence. Therefore, the important result here is that the incompleteness of full ILL arises as the result of the choice of the “wrong” pretopology (the least one) whereas the choice of the greatest pretopology, as it is done for (pre)ordered monoids naturally provides the completeness and even the finite model property.

6.1 Petri nets as preordered monoids

Let us remind the basics of the theory of Petri nets. They form a model of processes in terms of resources, represented by places which can hold to arbitrary nonnegative multiplicity, and of production or consumption of resources by actions, represented by transitions — see [27] for more details.

Let P be a set the elements of which are called places.

Fig. 3. A Petri net.

We denote by M_{f}(P) the set of finite multisets of elements of P that are called markings.^{8} The set of markings is the free commutative monoid over P. We denote by + the monoidal operation and by 0 the neutral element. We generally write M instead of M_{f}(P) for the set of markings. A transition t is an elementary transformation of markings described by a pair (^{•}t, t^{•}) of markings. The associated transformation is defined by the contextual closure of the relation ^{•}t ↦ t^{•}:

m [t⟩ m′ iff ∃c ∈ M, m = c +^{•}t and m′ = c + t^{•}

Intuitively, it means that when one reaches the marking m′ from the marking m with a transition t, one has to remove ^{•}t tokens from m getting e and put t^{•} tokens in e getting m′.

Definition 42 (Petri net) A Petri net is a quadruplet R = (P, T ,^{•}(·), (·)^{•})

8 A marking is a distribution of tokens over the places of P.

where P is a set of places, T is a set of transitions, and ^{•}(·), (·)^{•} are two functions T → M_{f}(P).

To distinguish places from markings, we use the notation \underline{a} to denote the marking that consists of only one token over the place a. We now introduce the reachability relation ⇝ which is the preorder induced by [·⟩, i.e. the reflexive and transitive closure ⇝ ≜ (⋃_{t∈T} [t⟩)^{⋆}. In other words, m ⇝ m′ means that one can reach m′ from m by a finite number of transitions m [t_{1}⟩ m_{1} … m_{n−1} [t_{n}⟩ m′. As an example, in the Petri net of figure 3, the property \underline{a} ⇝ 3\underline{a} is obtained by the following transitions \underline{a} [t_{1}⟩ \underline{a}+\underline{b} [t_{3}⟩ 3\underline{a}. We have the following property that expresses that the monoidal operation + is increasing with respect to the ⇝ preorder, or equivalently that ⇝ is contextually closed [8].

Proposition 43 For any marking m_{0}, m, m′ such that m ⇝ m′, the relation m_{0} + m ⇝ m_{0} + m′ holds.

PROOF. ⇝ is the preorder induced by the union of the contextually closed relations [t⟩ for transitions t, thus it is contextually closed. □

Proposition 44 If R = (P, T ,^{•}(·), (·)^{•}) is a Petri net, then (M_{f}(P), +, ⇝) is a preordered monoid.

We will denote by M_{R} the preordered monoid (M_{f}(P), +, ⇝). The mapping R ↦ M_{R} gives rise to a Petri net based semantic for ILL as a direct application of the preordered monoid semantic defined in section 5.5.

6.2 Interpretation of ILL

We consider a Petri net R = (P, T ,^{•}(·), (·)^{•}). As M_{R} = (M_{f}(P), +, ⇝) is a preordered monoid, it is sufficient to choose a pretopology (·)^{⋆} over this structure to obtain a quantale M_{R}^{⋆}, and thus a semantics for ILL.

In figure 4, we propose two quantales obtained for the pretopologies ↓(·) and (·)^{∘} from a given Petri net. The numbers 0, 1 and 2 respectively represent the sets 3ℕ.\underline{a}, (1 + 3ℕ).\underline{a} and (2 + 3ℕ).\underline{a}, and ⊥ and ⊤ represent ∅.\underline{a} and ℕ.\underline{a}.

In the following sections, we compare the two extremal pretopologies from the point of view of the interpretation of ILL.

⟵^{↓(·)}  ⟶^{(·)^{∘}}

Fig. 4. Quantales from a Petri net

6.2.1 The initial semantics

If we analyze the results of [8] w.r.t. our investigations on semantics, we observe that ↓(·) has been chosen as the underlying pretopology. Let us remind the corresponding interpretation of ILL. Let σ : Vars → M_{f}(P) be an interpretation of variables,

Initial Petri nets interpretation

\begin{matrix}⟦1⟧ ≜ \{x | x ⇝ 0\}  ⟦⊤⟧ ≜ M_{f}(P)  ⟦⊥⟧ ≜ ∅ \\ ⟦X⟧ ≜ & \{x | x ⇝ σ(X)\} & ⟦A ⊸ B⟧ ≜ & ⟦A⟧ ⊸• ⟦B⟧ \\ ⟦A ⊕ B⟧ ≜ & ⟦A⟧ ∪ ⟦B⟧ & ⟦A & B⟧ ≜ & ⟦A⟧ ∩ ⟦B⟧ \\ ⟦A ⊗ B⟧ ≜ \{x | ∃a ∈ ⟦A⟧, ∃b ∈ ⟦B⟧, x ⇝ a + b\} \end{matrix}

Unfortunately this semantics is not complete because we have the following result, that is due to the choice of the least pretopology.

Proposition 45 In the above interpretation (defined by the choice of the ↓(·) pretopology), we have ⟦A & (B ⊕ C)⟧ = ⟦(A & B) ⊕ (A & C)⟧.

PROOF. & is interpreted by subset intersection and ⊕ by subset union. □

For this semantics, the completeness can only be achieved at the price of removing one of the operators & or ⊕, i.e. by weakening the logic. In a certain sense, the partial completeness results of [8] are misleading because they could suggest that the structure of Petri nets is the main reason for incompleteness. In the following section, we show that such the incompleteness result comes from the choice of the least pretopology (instead of the greatest one).

6.2.2 The new Petri nets semantics

If we consider the greatest pretopology (·)^{∘} then we obtain the following interpretation of ILL:

New Petri nets interpretation

\begin{matrix}⟦X⟧ ≜ & \{x | x ⇝ σ(X)\} & ⟦A ⊸ B⟧ ≜ & ⟦A⟧ ⊸• ⟦B⟧ \\ ⟦⊤⟧ ≜ & M_{f}(P) & ⟦A & B⟧ ≜ & ⟦A⟧ ∩ ⟦B⟧ \\ ⟦1⟧ ≜ & \{x | x ⇝ 0\} & ⟦⊥⟧ ≜ & \{x | ∀m, p m + x ⇝ p\} \end{matrix} ; \begin{matrix}⟦A ⊗ B⟧ ≜ & \{x | ∀m, p (m + ⟦A⟧ + ⟦B⟧ ⇝ p ⇒ m + x ⇝ p)\} \\ ⟦A ⊕ B⟧ ≜ & \{x | ∀m, p (m + ⟦A⟧ ⇝ p and m + ⟦B⟧ ⇝ p ⇒ m + x ⇝ p)\} \end{matrix}

Therefore, the interpretations of ⊥ and ⊗ and ⊕ only differ in this semantics, compared to the initial semantics. But, it does not mean that a formula of type A & B has the same interpretation in both models. In fact, the interpretations ⟦A⟧ and ⟦B⟧ might already be different in case we have an internal ⊕ for example.

In figure 4, the given Petri net is such that the two semantics are different. Indeed, let us define X to be the smallest closed set containing the marking \underline{a}, i.e. ⟦X⟧ = (1 + 3ℕ).\underline{a} and Y be the smallest containing 2\underline{a}, ⟦Y ⟧ = (2 + 3ℕ).\underline{a}. The interpretations of X and Y are the same in both semantics, but the interpretation of X ⊕ Y is not the same anymore. Indeed, in the initial semantics, we get ⟦X ⊕ Y ⟧ = (\{1, 2\}) + 3ℕ).\underline{a} whereas in our new semantics, we get ⟦X ⊕ Y ⟧ = ℕ.\underline{a}. For that, we observe that the number of occurrences of \underline{a} in the markings is preserved modulo 3 by any transition t_{1} or t_{2}. Then, for any natural k, there is no natural n such that (k + \{1, 2\} + 3ℕ).\underline{a} ⇝ \underline{a}. Thus the role of the ⊕ connective, which is a kind of disjunction in the initial case, now can no longer be seen that way. This point will be developed in further work. Of course, we obtain a soundness theorem for this new semantics as a particular case of a preordered monoid semantics. We now prove the completeness and the finite model property that were questions studied and not solved in [8].

6.3 Universality of Petri nets

In this section, we prove that the mapping R ↦ M_{R} is a surjection, up to an equivalence of preordered monoids. The consequence is the completeness result of theorem 50.

We consider a preordered monoid (K, •, ⩽). We have to define a Petri net R such that M_{R} is equivalent to K. We define the Petri net R ≜ (K, T ,^{•}(·), (·)^{•}), the places of which are the elements of K. The set of transitions T is defined by T ≜ T_{1} ∪ ⋯ ∪ T_{5} where

t_{1} ∈ T_{1} \underline{a} [t_{1}⟩ \underline{b}  for a ⩽ b
t_{2} ∈ T_{2} \underline{a} [t_{2}⟩ \underline{b} + \underline{c} for a = b • c
t_{3} ∈ T_{3} \underline{b} + \underline{c} [t_{3}⟩ \underline{a} for a = b • c

\{t_{4}\} = T_{4} 0 [t_{4}⟩ \underline{e}_{\{t_{5}\} = T_{5} \underline{e} [t_{5}⟩ 0}

Thus, for example, there is exactly one transition of type T_{1} for each pair (a, b) such that a ⩽ b. Thus we have defined a Petri net with a set of transitions of five different types. Let us notice that R is finite if and only if K is finite.

Proposition 46 For any choice a_{1}, …, a_{n} of elements of K, the relation defined by \underline{a_{1}} + ⋯ + \underline{a_{n}} ≃ \underline{a_{1} • ⋯ • a_{n}} holds.

PROOF. The proof is by induction on n. For n = 0, by transitions of type T_{4} (resp. T_{5}) we obtain 0 ⇝ \underline{e} (resp. \underline{e} ⇝ 0). The case n + 1 is done by using transitions of type T_{2} and T_{3}. □

Proposition 47 The relation \underline{a_{1}} + ⋯ + \underline{a_{n}} ⇝ \underline{b_{1}} + ⋯ + \underline{b_{m}} holds in R if and only if a_{1} • ⋯ • a_{n} ⩽ b_{1} • ⋯ • b_{m} holds in K.

PROOF. For the only if case, we observe that all the transitions in T_{1} ∪ ⋯ ∪ T_{5} are increasing with respect to ⩽ and it is the contextual, reflexive and transitive closure ⇝ of their union. The if case is a trivial combination of proposition 46 and one transition of T_{1}. □

Proposition 48 The function i : K → M_{f}(K) defined by i(a) ≜ \underline{a} is an equivalence between (K, •, ⩽) and (M_{f}(K), +, ⇝).

PROOF. By proposition 47 (with n = m = 1), i is an embedding of preordered sets. The equivalence i(a_{1}•⋯•a_{n}) ≃ \underline{a_{1}}+⋯+\underline{a_{n}} holds by proposition 46. For n = 0, we obtain i(e) = 0 and for n = 2, we obtain i(x•y) = i(x)+i(y). Finally, as any element in M_{f}(K) is of the form \underline{a_{1}} + ⋯ + \underline{a_{n}}, i is also full, and hence is an equivalence. □

Theorem 49 Let (K, •, ⩽) be a preordered monoid and R be the Petri net (K, T ,^{•}(·), (·)^{•}) previously defined with transitions in T = T_{1} ∪ ⋯ ∪ T_{5}, then M_{R} and K are two equivalent preordered monoids. Moreover R is a finite Petri net whenever K is a finite preordered monoid.

We point out that another construction is presented in [8] but it does not preserve the finiteness because in this work the Petri net obtained by this construction always has an infinite number of transitions.

6.4 Completeness and finite model property

Theorem 50 (Completeness and finite model property) The new basedon Petri nets interpretation of ILL (corresponding to the choice of the greatest pretopology as in 6.2.2) is complete and has the finite model property.

PROOF. Soundness has been trivially proved earlier. Let us now suppose that F is a formula which is not valid, i.e. ⊮F holds. By proposition 37, there exists a finite preordered monoid (K, •, ⩽) and an interpretation σ : Vars → K such that for the corresponding interpretation, the property e ∉ ⟦F ⟧ holds. By proposition 49 we consider the finite Petri net for which M_{R} and K are equivalent under i(x) = \underline{x}. Then we take the interpretation of F in R with σ′(X) ≜ i(σ(X)). We denote by ⟦·⟧′ this interpretation. As i is an equivalence, we obtain the property ⟦F ⟧′ = ↓(⟦F ⟧) by proposition 39. And so, as 0 ≃ i(e), if 0 ∈ ⟦F ⟧′ holds then i(e) ∈ i(⟦F ⟧) holds because ⟦F ⟧′ is downward closed for ⇝ by proposition 32. Finally, e ∈ ⟦F ⟧ holds because i is an injection of K into M_{f}(K) which is contradictory. Therefore 0 ∉ ⟦F ⟧′ holds and R is a finite counter-model of F. □

These two results complete and reinforce the initial study of [8] about the relationships between ILL and Petri nets. In fact, Petri nets, with our semantics, are a helpful and convincing model for the full ILL. But we also have to study the consequences of such results when ILL is thought as a logic for specifying and reasoning about Petri nets, that is one of the concerns of the initial papers about Linear Logic and Petri nets. The logical fragments of ILL used in [8] enable to prove some basic positive assertions on nets and also to capture good negative properties. Further work will be devoted to such a study in the context of our new interpretation of ILL connectives.

6.5 Countermodels

At first we reconsider the result of section 5.6 about non-provability but with the Petri nets semantics point of view. Then we have

Proposition 51 (A ⊕ C) & (B ⊕ C) ⊢ (A & B) ⊕ C is not provable in ILL.

PROOF. Let us come back to the Petri net of figure 4. We also define Z to be the smallest closed set containing 0, ⟦Z⟧ = ⟦1⟧ = 3ℕ \underline{a}. Then we have ⟦A & B⟧ = ⟦A⟧ ∩ ⟦B⟧ = ∅ and ⟦A & B⟧ ⊕ C = ⟦C⟧ = 3ℕ \underline{a}. On the contrary, ⟦A ⊕ C⟧ = ⟦B ⊕ C⟧ = ℕ \underline{a} as we have already noticed. Thus, ⟦(A ⊕ C) & (B ⊕ C)⟧ is not included in ⟦(A & B) ⊕ C⟧. □

We can also reconsider the result of proposition 41 from the Petri net point of view. We can prove it by giving a Petri net on which the MacNeille closure is not stable. Let us consider the following Petri net

We define X = \{\underline{a}\} and Y = \{\underline{b}_{1}, \underline{b}_{2}\}. Then after a computation, we obtain: X^{†} = ↓\underline{a} = \{\underline{a}\} and Y^{†} = \{\underline{k}, \underline{b}_{1}, \underline{b}_{2}\}. Moreover, X +Y^{†} = \{\underline{a}+\underline{k}, \underline{a}+\underline{b}_{1}, \underline{a}+\underline{b}_{2}\}. Now, let us evaluate (X + Y)^{†} = \{\underline{a} + \underline{b}_{1}, \underline{a} + \underline{b}_{2}\}^{†}. It is clear that \{\underline{a} + \underline{b}_{1}, \underline{a} + \underline{b}_{2}\} ⇝ \underline{c}. It is also true that \underline{a} + \underline{k} ⇝̸ \underline{c} even if it is less clear how to prove it. Then \underline{a} + \underline{k} ∉ \{\underline{a} + \underline{b}_{1}, \underline{a} + \underline{b}_{2}\}^{†} and we have X + Y^{†} ⊈ (X + Y)^{†}.

6.6 Non-commutative linear logic

In this paragraph, we analyze what happens in the case of non-commutative linear logic, for which we do not require the monoidal operations/ors to be commutative. We will not give the detailed proofs of the results because they can be guessed more or less directly from the commutative case. The non-commutative linear logic has been proposed by Abrusci [1] as an interesting view of linear logic excluding the commutativity of hypotheses or conclusions in the linear sequent calculus [13]. Because of its relationships with Lambek calculus and its ”order-sensitive” characteristics, this logic appears important for computational linguistics applications but also for specifications and proofs development about properties of concurrent systems. Using non-commutative quantales, we can follow steps similar to the commutative case in order to define a new closure operator that is in this case X^{∘} ≜ {z | ∀m, k, n ∈ M m • X • n ⩽ k ⇒ m • z • n ⩽ k}. From this definition, we can get completeness results for the non-commutative case. Petri nets are represented by transitions between states, where states are multisets of tokens: this is the free commutative monoid generated by tokens. In the non-commutative case, we get the free (non-commutative) monoid, i.e. the set of words.^{9} If you have words a, b, and a transition t, then the transition rule will be If m = ^{•}t and m′ = t^{•} then a.m.b [t⟩ a.m′.b. With such a definition we can show how to obtain a non-commutative monoid and thus to provide a completeness result for so-called non-commutative Petri nets as well as a finite model property.

7 Concluding remarks

We have previously studied proof-search in ILL from the definition of canonical proofs being complete w.r.t. provability [12] but also from a based-on proof nets approach [2,9]. In this paper we aim at analyzing provability but also non-provability in ILL from a strong and fine revision of the semantics. One motivation is in fact to understand the semantic foundations that could explain for example the problems about completeness results in the context of Petri nets as models of ILL [8]. Another one is to provide appropriate semantics in order to design proof-search methods that can generate countermodels in case of non-provability. From an unified analysis of the completeness results of ILL with respect to algebraic and phase semantics, we have emphasized the importance of some particular choices of closures related to the completeness. A main contribution is the definition of a new semantics of ILL based on the notion of resource and for which we have proved the completeness and cut-elimination theorems using so-called syntactic models. To complete these results we have studied the effective construction of countermodels with a method based on a proofsearch approach using an appropriate notion of refutation tree. Then we have proved the finite model property and then deduced this important property for other semantics of ILL. Coming back to the notion of (pre)ordered monoid we have analyzed some particular closures called pretopologies and derive a new semantics of ILL from the choice of the greatest pretopology. As a Petri net can be seen as a preordered monoid, the choice of an appropriate pretopology over this structure leads to a particular quantale and then to a new Petri nets semantics of ILL. We have observed that the initial Petri nets semantics in [8] corresponds to the choice of the least pretopology. Therefore, it is clear that the problem of completeness is not directly connected to the Petri net structure but to semantic foundations (the choice of a particular closure). Thus, from our natural choice of the greatest pretopology, we have defined a new interpretation of ILL on Petri nets and then obtained the completeness and the finite model property for the full logic as main results. These results reinforce the fact that Petri nets, moreover with our semantics, are a helpful and convincing model for the full ILL. Further work will be devoted to the

9 Orelse, multisets of tokens where the order matters.

study of the consequences of such results when ILL is thought as a logic for specifying and reasoning about Petri nets. We will study the possibilities to prove assertions about nets and to capture different kinds of properties, regarding our new interpretation of ILL connectives. In these different new semantics, based on different kinds of semantic structures, we also have focused on the construction of countermodels. Further work will be devoted to the design of semantic proof-search methods based on these new based-on resources semantics with a particular interest for the generation of countermodels in case of non-provability. The relationships with proof-search methods based on proof nets that can also be efficient to detect non-provability [2] will be also explored. A very similar study on resources and semantics could be easily developed for the non-commutative ILL, following the same steps and with appropriate adaptations of the main notions to the non-commutative case, for instance non-commutative Petri nets. The interest of such a specialization of the previous results is to have new resource models for non-commutative ILL and also connected proof-search methods with the capability to generate countermodels. Such results will have an important impact in connected applications in computational linguistics or also in development of specifications and proofs about properties of concurrent systems.

References

[1] S. Abramsky. Computational Interpretations of Linear Logic. Theoretical Computer Science, 111(1-2):3–58, 1993.

[2] V. Balat and D. Galmiche. Labelled Deduction, volume 17 of Applied Logic Series, chapter Labelled Proof Systems for Intuitionistic Provability. Kluwer Academic Publishers, 2000.

[3] N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for Intuitionistic Linear Logic. In Int. Conference on Typed Lambda Calculi and Applications, LNCS 664, pages 75–90, Utrecht, The Netherlands, March 1993.

[4] G. Birkhoff. Lattice Theory. American Mathematical Society, 1967.

[5] W. Buszkowski. The Finite Model Property for BCI and Related Systems. Studia Logica, 57:303–323, 1996.

[6] B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press, 1990.

[7] U. Engberg and G. Winskel. Petri Nets as Models of Linear Logic. In CAAP 90, Coll. on Trees in Algebra and Programming, LNCS 431, pages 144–161, Copenhagen, Denmark, May 1990.

[8] U. Engberg and G. Winskel. Completeness results for linear logic on Petri nets. Annals of Pure and Applied Logic, 86:101–135, 1997.

[9] D. Galmiche. Connection Methods in Linear Logic and Proof nets Construction. Theoretical Computer Science, 232(1-2):231–272, 2000.

[10] D. Galmiche and D. Larchey-Wendling. Provability in Intuitionistic Linear Logic from a new interpretation on Petri nets - extended abstract. Electronic Notes in Theoretical Computer Science, 17, 1998.

[11] D. Galmiche and D. Larchey-Wendling. Structural sharing and efficient proof-search in propositional intuitionistic logic. In Asian Computing Science Conference, ASIAN’99, LNCS 1742, pages 101–112, Phuket, Thailand, December 1999.

[12] D. Galmiche and G. Perrier. Foundations of proof search strategies design in linear logic. In Logic at St Petersburg ’94, Symposium on Logical Foundations of Computer Science, LNCS 813, pages 101–113, St Petersburg, Russia, July 1994.

[13] J-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.

[14] J-Y. Girard. Linear logic: its syntax and semantics. In J.Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 1–42. Cambridge University Press, 1995.

[15] Y. Lafont. The finite model property for various fragments of linear logic. Journal of Symbolic Logic, 62(4):1202–1208, 1997.

[16] D. Larchey-Wendling and D. Galmiche. Quantales as completions of ordered monoids: revised semantics for intuitionistic linear logic. Electronic Notes in Theoretical Computer Science, 35, 2000.

[17] J. Lilius. High-level nets and linear logic. In 13th Int. Conference on Applications and Theory of Petri Nets, LNCS 616, pages 310–327, Sheffield, UK, 1992.

[18] P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In 7th IEEE Symposium on Logic in Computer Science, pages 235–246, Santa-Cruz, California, 1992.

[19] J. Meseguer and N. Marti-Oliet. From Petri nets to Linear Logic. Math. Struct. in Comp. Science, 1:69–101, 1991.

[20] P.W. O’Hearn and D. Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999.

[21] M. Okada. Phase semantic cut-elimination and normalization proofs of firstand higher-order linear logic. Theoretical Computer Science, 227:333–396, 1999.

[22] M. Okada and K. Terui. The finite model property for various fragments of intuitionnistic linear logic. Journal of Symbolic Logic, 2000. to appear.

[23] H. Ono. Substructural Logics, volume 2 of Studies in Logic and Computation, chapter Semantics for Substructural Logics, pages 259–291. Oxford University Press, 1993.

[24] H. Ono. Decidability and Finite Model Property of Substructural Logics. In The Tbilisi Symposium on Logic, Language and Computation, pages 262–274. CSLI Publications, 1997.

[25] L. Pinto and R. Dyckhoff. Loop-free construction of counter-models for intuitionistic propositional logic. In Behara and al., editors, Symposia Gaussiana, pages 225–232, 1995.

[26] H. Rasiowa and R. Sikorski. The Mathematics of Metamathematics, volume 41 of Monografie Matematyczne. Polska Akademia Nauk, Warszawa, 1963.

[27] W. Reisig. Petri Nets, An Introduction, volume 4 of EATCS Monographs on Theorical Computer Science. Springer-Verlag, 1985.

[28] K. I. Rosenthal. Quantales and their Applications. Research Notes in Mathematics, 1990.

[29] G. Sambin. Substructural Logics, volume 2 of Studies in Logic and Computation, chapter Semantics of Pretopologies. Oxford Science Publications, 1993.

[30] A. S. Troelstra. Lectures on Linear Logic, volume 29 of Center for the Study of Language and Information. CSLI, 1992.

[31] D. N. Yetter. Quantales and (noncommutative) Linear Logic. Journal of Symbolic Logic, 55:41–64, 1990.