Completeness Proofs for Linear Logic Based on the Proof Search Method
(Preliminary Report)
Mitsuhiro Okada Kazushige Terui Department of Philosophy, Keio University
Abstract
The proof search method is a traditionally established way to prove the completeness theorem for various logics. The purpose of this paper is to show that this method can be adapted to linear logic.
First we prove the completeness theorem for a certain fragment of intuitionistic linear logic, callednaive linear logic, with respect tonaive phase semantics, i.e., phase semantics without any closure condition, using the proof search method in a certain labelled sequent system. Then the completeness of the (rudimentary) classical linear logic can be obtained as a direct corollary by a Kolmogorov-G¨odel style double negation interpretation.
To apply the proof search method for the full system of linear logic, we generalize the notion ofbranchin the standard proof search method to that ofOR-tree, and give a proof of the completeness theorem for intuitionistic (classical, resp.) linear logic with respect to intuitionistic (classical, resp.) phase semantics, based on a generalized form of the proof search method.
1 Introduction
The proof search method is considered to be one of the most natural completeness proof methods and successfully applied to prove the completeness theorems for various logics, typi- cally for classical logic, intuitionistic logic and some of modal logics (cf. Kleene[?], Sch¨utte[?], Takeuti[?]).
This method consists of the following two steps; (i) to prove that for any unprovable formula there exists such a branch in a proof search tree that does not reach an axiom and that contains enough information to refute the formula (called an open branch), and (ii) to show the construction of a countermodel of the formula from the open branch obtained by (i). This method could be viewed as a specific way of the Henkin model construction in the classical logic case since the proof search procedure gives a process of construction of a maximal consistent set of formulas.
The usual proof search method uses the structural rules (weakening and contraction) very essentially. Hence it has not been known if or not this method is adaptable to linear logic in which the lack of the structural rules is one of the main features. The purpose of this paper is to give an affirmative answer to this question.
To see how structural rules are essential in the case of the proof search method for tra- ditional logics, let us suppose that we would like to refute (i.e., to find a countermodel of)
Γ A∨B in classical logic. Our task is to find an open branch in a proof search tree that contains enough information to make every formula in Γ true and both A and B false. A proof search tree of a given sequent is constructed by successively applying the inference rules of classical logic in a bottom-up manner. However, if we use the usual inference rules for
∨-right, that is, ΓA
ΓA∨B and
ΓB ΓA∨B,
we lose one of A andB (when read bottom-up), hence branches in the resulting proof search tree retain too little information to refute ΓA∨B. The essential trick here is to consider the following derived rule in classical logic which is equivalent to the above two rules, due to weakening and contraction;
ΓA, B ΓA∨B.
Thanks to using this equivalent rule we can preserve the information on bothA andB. This trick is a part of the reason why an open branch in classical logic suffices to construct a countermodel. One could consider the same trick for intuitionistic logic, which leads to the completeness with respect to the Kripke models (cf. eg. Takeuti[?], CH 1,§8).
In linear logic, however, we cannot use any trick like above because of the lack of structural rules;
• We cannot replace two ⊕-right rules by a single rule, contrary to the ∨-right case of classical logic.
• We must take all possible context partitions into account when we apply ⊗-right and
−◦-left rules. For example,α, βα⊗γ has only one non-atomic formula, but we must consider four possibilities when we apply ⊗-right rule;
α α, βγ α, βα⊗γ
αα βγ α, βα⊗γ
βα αγ α, βα⊗γ
α, β α γ α, βα⊗γ .
As a consequence, the standard construction of a countermodel from one open branch is not possible for linear logic. In this paper, we propose two solutions to overcome this difficulty.
1. To introduce labels; we consider a sort of labelled system for the proof search method in which resource information is expressed not in terms of number of formula occurrences in a se- quent, but in terms oflabels attached to formulas. In the system, structural rules can be used freely, hence we can accommodate the standard proof search method to this system. In this way, we prove that a certain fragment of intuitionistic linear logic, which we callnaive linear logic(NLL), is complete with respect tonaive phase semantics, i.e., phase semantics without any closure condition. Then we show that the multiplicative additive fragment of classical linear logic (MALL), sometimes called rudimentary linear logic, is encoded into NLL via the Kolmogorov-G¨odel style double negation translation. Hence, as a direct corollary, we also have a completeness proof of MALL based on the proof search method, since the classical phase semantics (in the sense of Girard[?]) is also obtained by the double-negation closure property from our naive phase semantics. The labelling method has been investigated under Gabbay’s general framework ofLabelled Deductive Systems (LDS) [?]. Our method could be
viewed as an application of LDS (see Kurtonina[?], Venema[?] for other applications of LDS to substructural logics).
2. To generalize the notion of open branch; We generalize the notion of branch in a proof search tree to the notion ofOR-branching treeor simplyOR-tree, and show that given an un- provable sequent ΓC, one can construct anopenOR-tree which retains enough information to refute the sequent. Then we describe how to construct an intuitionistic phase model from an open OR-tree of full intuitionistic linear logic (ILL), and a classical phase model from that of full classical linear logic (LL). In both cases, the closure condition of phase semantics plays an essential role. This gives a completeness proof based on a generalized form of the proof search method both forILLand forLL. We also obtain the cut-elimination theorem as a corollary, since we do not use the cut rule during the construction of the required OR-tree and the corresponding countermodel.
In section 2, first we give the definitions of intuitionistic and classical phase semantics.
Then naive phase semantics is obtained by dropping the closure condition from intuitionistic phase semantics. In section 3, we define naive linear logic (NLL), which consists of connec- tives (⊗, ⊕, −◦) where −◦ is restricted to the form A−◦α (for any atomic formula α). In order to incorporate with the standard proof search method, we also introduce an alterna- tive formulation of NLL using labels, called labelled naive linear logic (LNLL), and prove the completeness of NLL with respect to naive phase semantics. Section 4 is devoted to a completeness proof of both ILLand LLbased on the open OR-branching tree construction.
We give the definitions of intuitionistic linear logic and classical (left one-sided) linear logic in Appendix A and B, respectively.
2 Intuitionistic, Classical and Naive Phase Semantics
In this section, we define intuitionistic phase semantics (cf. Abrusci[?], Troelstra[?], Okada[?]), classical phase semantics (cf. Girard[?][?] and Lafont[?]), and naive phase semantics.
Definition 1 An intuitionistic phase space (M, Cl) consists of a commutative monoid M and a function Cl:P(M) −→ P(M), called a closure operator, satisfying the following;
(C1) X ⊆Cl(X);
(C2) X ⊆Y impliesCl(X)⊆Cl(Y);
(C3) Cl(X) =Cl(Cl(X));
(C4) Cl(X)Cl(Y)⊆Cl(XY);
where XY is defined by{xy|x∈X, y∈Y}. A setX⊆M that satisfiesX =Cl(X) is called a fact.
Then, we can define1=Cl({1}) (1 stands for the unit element ofM), =M,0=Cl(∅), and for any facts X, Y,
• X−◦Y ={y|∀x∈Xxy ∈Y}
• X⊗Y =Cl(XY);
• X&Y =X∩Y;
• X⊕Y =Cl(X∪Y).
As easily seen, each constant above is a fact and each operation above produces a fact when- ever facts X and Y are given.
IfM is an intuitionistic phase space, then J(M) ={x∈1|x∈Cl({xx})} is a submonoid ofM. Anenriched intuitionistic phase spaceis an intuitionistic phase spaceM endowed with a submonoid K of J(M) (not necessary to be a fact).
For any factX of intuitionistic phase space, define
• !X=Cl(X∩K).
An intuitionistic phase modelM = (M, Cl, K, v) is given by an intuitionistic phase space M = (M, Cl, K) and aninterpretation v which maps each atomic formulaα to a factv(α) of M, which is also denoted by α∗. Then each formulaA is interpreted by a factA∗ along the above definitions, and Γ ≡A1, . . . , An is interpreted by Γ∗ =A∗1⊗ · · · ⊗A∗n. We say that A issatisfied inM if 1∈A∗, and that ΓC is satisfied inM if Γ∗ ⊆C∗.
A classical phase space (M,⊥, K) is an intuitionistic phase space (M, Cl, K) with a subset
⊥ofM in which the closure operatorClis defined by double negation, i.e., Cl(X) =X⊥⊥= (X−◦ ⊥)−◦ ⊥. In classical phase spaces, we have two additional operations;
• X Y = (X⊥Y⊥)⊥;
• ?X = (X⊥∩K)⊥.
A naive phase space M is an intuitionistic phase space (M, Cl) where Cl is the identity function. In a naive phase spaceM, any subset ofM is a fact,X⊗Y =XY andX⊕Y =X∪Y. Since J(M) is degenerate (= {1}), we do not consider enriched naive phase spaces at all.
The following examples indicate that naive phase semantics is a natural generalization of traditional semantics such as classical 2-valued semantics and Kripke semantics.
1. Consider a naive phase model whose underlying monoid is the singleton {1}. Write F, T to denote φ,{1}, respectively. Then A∗⊗B∗=T iff A∗&B∗=T iff A∗ =T and B∗ = T; A∗ ⊕B∗ = T iff A∗ = T or B∗ = T; and A∗−◦B∗ = T iff A∗ = T implies B∗=T. Hence, this model is a usual 2-valued model for classical logic.
2. Consider (M, v) whereM is idempotent, i.e., xx =x for any x ∈ M and v maps each atom to an ideal of M, i.e. a subset satisfying XM ⊆ X. M can be seen as the set of possible worlds with accessibility relation ≤ defined by x ≤ y ⇔ y = xz for some z ∈M. Write x|=A ifx∈A∗. Thenx |=A⊗B iffx|=A&B iff x|=A and x|=B; x |=A⊕B iff x |= A or x |= B; andx |=A−◦B iff for every y ≥ x, y |=A implies y|=B. Hence, (M, v) is a usual Kripke model for intuitionistic logic.
3 Naive Linear Logic and its Completeness with respect to Naive Phase Semantics
Naive linear logic(NLL) is a fragment of intuitionistic linear logic with connectives (⊗,−◦,⊕) such that −◦ is restricted to the formX−◦α. More precisely, given a set V of propositional variables, the set Lof NLL formulas is defined as follows;
L::=V|L⊗L|L⊕L|L−◦V.
NLLdoes not have any constant. However, we will see in the end of this section that the multiplicative additive fragment of classical linear logic (MALL) including constants 1 and
⊥ can be encoded into this simple fragment.
Now we introduce labelled naive linear logic (LNLL). We presuppose that a countable alphabet Σ is given. The free commutative monoid generated by Σ is denoted by Com(Σ).
a, b, c, . . . ∈Com(Σ) are called labels and in particularx, y, z, . . .∈Σ are calledsimple labels.
A label ais said to belinear if it contains no repetition; for example,xyx is not linear while xyz is linear wherex, y, z ∈Σ. The set of linear labels is denoted by Lin(Σ). In particular, the unit 1 ofCom(Σ) is inLin(Σ). We writea≤bifb=acfor somec∈Com(Σ). Alabelled formula is of the form a:A wherea is a linear label and A is a formula ofNLL. Alabelled sequent is of the form Γ∆, where Γ and ∆ are finite multisets of labelled formulas. Let Γ be {a1:A1, . . . , an:An}. Then we also write a1· · ·an: Γ∆ to indicate the total amount of labels occuring in Γ (in particular, we write 1 : Γ ∆ if Γ=φ). We say that boccurs inΓ if b≤ai for somei, and also say thatb is unique in Γ if boccurs in {ai:Ai} for exactly one i. The similar conventions also apply to ∆.
A labelled sequent a1:A1, . . . , an:An c:C is said to be strict ifc=a1· · ·an and ai= 1 for any i. In particular, a sequent of the form c:C is strict iff c= 1.
The formulas and the sequents of LNLL are labelled formulas and labelled sequents, respectively. The inference rules of LNLLare those in Figure 1.
It is assumed that each inference rule should preserve the linearity of the labels; for example, the following inference is not allowed in LNLL;
Γ1a:A Γ2a:B Γ1,Γ2 aa:A⊗B .
Lemma 1 Given a proof π of LNLL sequent Γ ∆, one can construct a proof π of strict LNLL sequent c: Γ0 c:C0, where c: Γ0 ⊆Γ and c:C0∈∆, such that each sequent occuring in π is strict.
Proof. By induction on the length ofπ.
Proposition 1 If a strict LNLL sequent c: Γ c:C is provable in LNLL, then Γ C is provable in NLL.
Proof. Given a proof π of strict LNLL sequent c: Γ c:C, we can obtain another proof π of the same sequent in which each sequent is strict by Lemma 1. Such a proof is easily transformed into a proof of ΓC inNLL by dropping all the labels occurring in it.
Next, we enrich the labelled sequents with tags which express additional information needed to define a suitable proof search procedure. A tagged sequent is of the form < (Γ
∆),Σ1,Σ2,Σ3 >where Γ∆ is a labelled sequent, Σ1 is a finite multiset of atomic labelled formulas such that Σ1 ⊆Γ, and Σ2 and Σ3 are finite multisets of labelled formulas. <(Γ
∆),Σ1,Σ2,Σ3 > is often denoted by <(Γ∆),Σ>. If Π is a multiset of labelled formulas such that Σ1⊆Π, the difference of Π and Σ1 is denoted by Π−.
<(Γ∆),Σ1,Σ2,Σ3 >is regular if
Identity and Cut:
a:Aa:A Identity Γ1 ∆1, a:A a:A,Γ2 ∆2 Γ1,Γ2 ∆1,∆2 Cut Structural Rules:
Γ∆
a:A,Γ∆ W l Γ∆
Γ∆, a:A W r a:A, a:A,Γ∆
a:A,Γ∆ Cl Γ∆, a:A, a:A Γ∆, a:A Cr Loose Rules:
Γ1∆1, a:A Γ2∆2, b:B
Γ1,Γ2 ∆1,∆2, ab:A⊗B ⊗r Γ1∆1, a:A ab:α,Γ2 ∆2 b:A−◦α,Γ1,Γ2∆1,∆2 −◦l Γ∆, a:A
Γ∆, a:A⊕B ⊕r1 Γ∆, a:B
Γ∆, a:A⊕B ⊕r2 Strict Rules:
a:A,Γ∆, ab:α Γ∆, b:A−◦α −◦r
whereadoes not occur in Γ and ∆.
a:A, b:B,Γ∆[x:=ab] x:A⊗B,Γ∆ ⊗l
wherea and b do not occur in Γ and ∆, simple labelx does not occur in Γ and is unique in
∆. [x:=ab] means the usual substitution operation.
a:A,Γ∆ a:B,Γ∆ a:A⊕B,Γ∆ ⊕l
whereadoes not occur in Γ and is unique in ∆. Moreover, each formula in Γ is labelled with a simple label distinct from each other.
Figure 1: Inference Rules of Labelled Naive Linear Logic
(θ1) For each a:α∈Σ1, there area1:A∈Σ2 anda2:A−◦α∈Γ− such thata=a1a2. (θ2) Each formula in Γ− is labelled with a simple label distinct from each other.
(θ3) If Γ contains a formula of the forma:A⊗B ora:A⊕B, thenais unique in Γ and also unique in ∆.
(θ4) Γ−∆, c:C is provable for any c:C ∈Σ2.
Lemma 2 Let<(Γ∆),Σ1,Σ2,Σ3 >be a regular tagged sequent. ThenΓ−∆is derivable from Γ∆.
Proof. Γ ∆ is of the form Σ1,Γ− ∆ and Σ1 ={a1:α1, . . . , an:αn}. By (θ1), there are a11:A1 ∈ Σ2 and a12:A1−◦α1 ∈ Γ− such that a1 = a11a12. By (θ4), Γ− ∆, a11:A1 is provable. Hence,
Γ−∆, a11:A1 a1:α1, . . . , an:αn,Γ−∆ a12:A1−◦α1, a2:α2, . . . , an:αn,Γ−,Γ−∆,∆
a2:α2, . . . , an:αn,Γ− ∆
By repeating this process ntimes, we can eliminate all ai:αi’s.
Definition 2 We assume a fixed well-ordering ≺L on the labels and also assume a fixed well-ordering ≺F on the labelled formulas. A labelled formula of the forma:A−◦α is called a −◦-formula. ⊗-formulas and⊕-formulas are defined similarly.
Letσ be a function which maps a tagged sequent to either a finite set of tagged sequents or symbol∗, defined as follows;
(i) If < S,Σ>is irregular, then σ(< S,Σ>) =∗;
(ii) else if S ≡a:A,Γ∆, a:A, thenσ(< S,Σ>) =∗;
(iii) else ifS ≡Γ∆, d:A−◦α and no−◦-formula≺F-smaller thand:A−◦α is in ∆, then σ(< S,Σ>) = {<(x:A,Γ ∆, xd:α),Σ>}, where x is the≺L-smallest simple label not occuring in Γ and ∆;
(iv) else if S ≡d:A⊗B,Γ ∆ and no ⊗-formula ≺F-smaller than d:A⊗B is in Γ, then d is simple (otherwise < S,Σ>would be irregular by (θ3)), so let σ(< S,Σ1,Σ2,Σ3 >
) = {<(x:A, y:B,Γ∆[d:=xy]),Σ1,Σ2,Σ3[d:=xy]>}, where x and y are the two
≺L-smallest simple labels not occurring in Γ and ∆;
(v) else ifS ≡a:A⊕B,Γ ∆ and no ⊕-formula ≺F-smaller than a:A⊕B is in Γ, then σ(< S,Σ>) ={<(a:A,Γ∆),Σ>, <(a:B,Γ∆),Σ>};
(vi) else if (1) S ≡ d:A−◦α,Γ ∆, (2) ad occurs in ∆, (3) ad:α ∈ Γ and a:A ∈ Σ3, and (d:A−◦α, a) is the smallest pair (according to ≺F and ≺L) satisfying conditions (1)–(3), then
σ(< S,Σ1,Σ2,Σ3 >) = {<(d:A−◦α,Γ∆, a:A),Σ1,Σ2,Σ3∪ {a:A}>,
<(ad:α, d:A−◦α,Γ∆),Σ1∪ {ad:α},Σ2∪ {a:A},Σ3 >};
(vii) else if (1)S ≡Γ∆, d:A⊗B, (2) d=ab, (3)a:A∈Σ3 and b:B ∈Σ3, and (d:A⊗B, a) is the smallest pair (according to≺F and ≺L) satisfying conditions (1)–(3), then
σ(< S,Σ1,Σ2,Σ3 >) = {<(Γ∆, ab:A⊗B, a:A),Σ1,Σ2,Σ3∪ {a:A}>,
<(Γ∆, ab:A⊗B, b:B),Σ1,Σ2,Σ3∪ {b:B}>}; (viii) else if S ≡Γ ∆, a:A⊕B and no ⊕-formula ≺L-smaller than a:A⊕B is in ∆, then
σ(< S,Σ>) ={<(Γ∆, a:A, a:B),Σ>};
(ix) elseσ(< S,Σ>) =φ.
For any < S0,Σ0 >, σ induces a rooted tree Tσ(< S0,Σ0>) (called a proof search tree) each node of which is labelled with a tagged sequent, constructed as follows;
1. The root of Tσ(< S0,Σ0 >) is labelled with< S0,Σ0 >;
2. If a node x is labelled with < S,Σ > and σ(< S,Σ >) = ∗, then x has a child node which is labelled with∗ and is a leaf ofTσ(< S0,Σ0 >);
3. If a node x is labelled with < S,Σ>and σ(< S,Σ>) ={< S1,Σ1 >, . . . , < Sk,Σk>}
(where k is 0 or 1 or 2), then xhas k children nodesx1, . . . , xk and each xi is labelled with < Si,Σi >(in particular,x is a leaf ofTσ(< S0,Σ0>) if k= 0).
A branch of a proof search tree is either a path from the root to a leaf or an infinite sequence of nodes in the tree such that every initial segment of it is a path from the root.
A branch of a proof search tree is said to be closed if it is a finite path x0, . . . , xn and xn is labelled with ∗; otherwise a branch is said to be open.
Lemma 3 Tσ(< S0,Σ0 >) is finite for any < S0,Σ0 >.
Lemma 4 Let < S0,Σ0 > be regular. If S0 is unprovable, then Tσ(< S0,Σ0 >) has an open branch.
Proof. Let S be unprovable and < S,Σ > be regular. Then σ(< S,Σ >) = ∗. Hence it suffices to show that if σ(< S,Σ >) = {< S1,Σ1 >, . . . , < Sk,Σk >}, then < Si,Σi > is regular and Si is unprovable for somei.
It is easily shown that (θ1)–(θ3) hold for every< Si,Σi >. Hence it suffices to show that
< Si,Σi > satisfies (θ4) and Si is unprovable for some i. We only prove the two essential cases;
(v) S ≡a:A⊕B,Γ∆ andσ(< S,Σ>) ={< S1,Σ>, < S2,Σ>}, whereS1≡a:A,Γ∆ and S2 ≡a:B,Γ∆. First we prove that both< S1,Σ>and< S2,Σ>satisfies (θ4).
Let c:C∈Σ2. Then by the assumption a:A⊕B,Γ−∆, c:C is provable. Hence, a:Aa:A
a:Aa:A⊕B a:A⊕B,Γ−∆, c:C a:A,Γ−∆, c:C .
The same holds for a:B,Γ− ∆, c:C. Hence both < S1,Σ > and < S2,Σ > are regular.
Now we prove that either S1 or S2 is unprovable. Suppose that both S1 and S2 are provable. Then by the regularity of < S1,Σ>and < S2,Σ> and by Lemma 2,
a:A,Γ∆ a:A,Γ−∆
a:B,Γ∆ a:B,Γ−∆ a:A⊕B,Γ−∆
a:A⊕B,Γ∆ , which contradicts the assumption.
(vi) S ≡d:A−◦α,Γ∆ and
σ(< S,Σ1,Σ2,Σ3 >) = {< S1,Σ1,Σ2,Σ3∪ {a:A}>,
< S2,Σ1∪ {ad:α},Σ2 ∪ {a:A},Σ3 >}, where S1≡d:A−◦α,Γ∆, a:A and S2≡ad:α, d:A−◦α,Γ∆.
< S1,Σ1,Σ2,Σ3 ∪ {a: A} > satisfies (θ4) by W r rule. Hence if S1 is unprovable, our claim holds. Suppose that S1 is provable. Then S2 should be unprovable by the assumption, −◦l rule and Cl rule. Moreover, < S2,Σ1 ∪ {ad:α},Σ2 ∪ {a:A},Σ3 >
satisfies (θ4); d:A−◦α,Γ−∆, c:C is provable by the assumption for c:C ∈Σ2, and d:A−◦α,Γ−∆, a:Ais also provable becauseS1is provable and< S1,Σ1,Σ2,Σ3∪ {a: A}> is regular, hence
d:A−◦α,Γ∆, a:A d:A−◦α,Γ−∆, a:A by Lemma 2.
Let R be a open branch. By Lemma 3, R is a finite path, say, of length n. R can be represented as;
R ≡< S0,Σ10,Σ20,Σ30 >, < S1,Σ11,Σ21,Σ31 >, . . . , < Sn,Σ1n,Σ2n,Σ3n> .
From now on, we will not use the second and the third component (Σ1i and Σ2i) of each tagged sequent (the fourth component Σ3i will be used to prove the next lemma). Hence we consider the following sequence
R =<(Γ0∆0),Σ0 >, <(Γ1∆1),Σ1 >, . . . , <(Γn ∆n),Σn >, where Γi ∆i≡Si and Σi ≡Σ3i.
R may contain the following subsequence;
. . . , <(z:A⊗B,Γ∆),Σ>, <(x:A, y:B,Γ∆[z:=xy]),Σ[z:=xy]>, . . ..
To correlate the resource information in the first tagged sequent above with that in the second one, we would like to make a relabelling operation on the labels occurring inR to obtain the following sequence;
. . . , <(xy:A⊗B,Γ∆[z:= xy]),Σ[z:=xy]>, <(x:A, y:B,Γ∆[z:=xy]),Σ[z:=xy]>
, . . ..
The process of relabelling is described below.
For each 0≤j ≤n, we define a finite sequence Rj of the form<(Γj0 ∆j0),Σj0 >, . . . , <
(Γjj ∆jj),Σjj >of lengthj+ 1, as follows;
• R0 ≡<(Γ0∆0),Σ0 >;
• If Sj ≡z:A⊗B,Γ∆ andSj+1≡a:A, b:B ∆[z:=xy], then
Rj+1 ≡<(Γj0∆j0[z:=xy]),Σj0[z:=xy]>, . . . , <(Γjj ∆jj[z:=xy]),Σjj[z:=xy]>, <
(Γj+1∆j+1),Σj+1>;
• otherwise Rj+1≡<(Γj0 ∆j0),Σj0 >, . . . , <(Γjj ∆jj),Σjj >, <(Γj+1 ∆j+1),Σj+1>. Now we have sequenceRnof length n. Let ΓRbe0≤j≤nΓnj and ∆Rbe0≤j≤n∆nj. The following lemma is checked by induction on the construction of Rj;
Lemma 5
(1) ΓR and ∆R are disjoint;
(2) If a:A⊗B ∈ ΓR, then there are some b, c such that b:A ∈ ΓR and c:B ∈ ΓR and a=bc;
(3) If a:A⊗B∈∆R, then for any b, c such that a=bc, either b:A∈∆R or c:B ∈∆R; (4) If a:A−◦α ∈ ΓR, then for any b such that ab occurs in ∆R, either b:A ∈ ∆R or
ab:α∈ΓR;
(5) If a:A−◦α∈∆R, then there isb such that b:A∈ΓR and ab:α∈∆R; (6) If a:A⊕B∈ΓR, then either a:A∈ΓR or a:B ∈ΓR;
(7) If a:A⊕B∈∆R, then a:A∈∆R anda:B ∈∆R. We define naive phase modelMR= (M, v) by
• M =Com(Σ);
• v(α) ={a|a:α∈∆R}.
Proposition 2 For any NLL formula A, the following hold;
(a) If a:A∈ΓR, then a∈A∗ in MR; (b) If a:A∈∆R, then a∈A∗ in MR.
Proof. By induction on the complexity of A.
(Case 1)Ais an atomic formulaα. (b) is by definition. As for (a), suppose thata:α∈ΓR anda∈α∗. The latter means thata:α∈∆R, which is impossible by Lemma 5(1).
(Case 2) A is of the form B⊗C. To show (a), suppose that a:B ⊗C ∈ ΓR. Then for someb andc, b:B ∈ΓR and c:C ∈ΓR and a=bc by Lemma 5(2), hence by IH,b∈B∗ and c∈C∗, thus a=bc∈B∗⊗C∗.
As for (b), note that a∈B∗⊗C∗ iff for any b and c such that bc =a, eitherb ∈B∗ or c ∈C∗. Suppose that a:B⊗C ∈∆R and a= bc. Then either b:B ∈∆R or c:C ∈∆R by Lemma 5(3). Hence by IH, either b∈B∗ orc∈C∗, so the claim holds.
(Case 3) Ais of the formB−◦α. To show (a), suppose thata:B−◦α∈ΓR and b∈B∗. If ab does not occur in ∆R, then ab∈α∗ by definition. Otherwise, ab occurs in ∆R and by Lemma 5(4), either b:B ∈ ∆R orab:α ∈ ΓR. However, the former is impossible by IH(b), hence ab∈α∗, so the claim holds.
As for (b), ifa:B−◦α ∈∆R thenb:B ∈ΓR and ab:α ∈∆R for somebby Lemma 5(5).
By IH, b∈B∗ and ab∈α∗. Therefore, a∈B∗−◦α∗.
(Case 4)A is of the form B⊕C. Similarly shown using Lemma 5(6) and (7).
Theorem 1 For any NLL sequent ΓC, the following are equivalent;
1. ΓC is provable in NLL;
2. ΓC is satisfied in all naive phase models;
3. a: Γa:C is provable in LNLLfor some linear label a.
Proof. 1 implies 2 by the usual soundness argument. 3 implies 1 by Proposition 1. To show that 2 implies 3, suppose that a1:A1, . . . , al:Al a1· · ·al:C is unprovable for any a1, . . . , al where Γ ≡ A1, . . . , Al. Let x1, . . . , xl be distinct simple labels. Then S0 ≡ x1 : A1, . . . , xl:An x1· · ·xl:C is unprovable and < S0, φ, φ, φ >is regular. Hence by Lemma 4, Tσ(< S0, φ, φ, φ >) has an open branch R. By the construction described before, we get sequence
Rn≡<(b1:A1, . . . , bl:Alb1· · ·bl:C),Σn0 >, . . .,
from which naive phase model MR is constructed. By Proposition 2, bi ∈A∗i for 1≤i ≤l and b1· · ·bl∈C∗, i.e., ΓC is not satisfied in MR, that contradicts 2.
The multiplicative additive fragment of classical linear logic (MALL) can be encoded into NLL by the following Kolmogorov-G¨odel style double negation interpretation.
Definition 3
1. Let us fix an atomic formulaα0and assume that noMALLformula containsα0. Then, given an MALLformulaA, an NLL formulaA◦ is defined as follows;
1◦ = α0
⊥◦ = α0−◦α0
β◦ = β−◦α0 (β⊥)◦ = β
(B⊗C)◦ = ((B◦−◦α0)⊗(C◦−◦α0))−◦α0
(B C)◦ = B◦⊗C◦
(B⊕C)◦ = ((B◦−◦α0)⊕(C◦−◦α0))−◦α0
(B&C)◦ = B◦⊕C◦ 2. A• is defined to beA◦−◦α0.
Proposition 3 A is provable inMALL iff A• is provable inNLL.
Proof. The Only-if-part is shown by induction on the length of proof. The If-part is by induction on the complexity ofA.
Classical phase models are obtained from naive phase models by the double negation clo- sure condition, which precisely corresponds to the above syntactic double negation translation.
Hence the following proposition is almost immediate.
Proposition 4 Ais satisfied in all classical phase models iffA• is satisfied in all naive phase models.
As a direct corollary of Theorem 1, Proposition 3 and Proposition 4, we have Corollary 1 MALL is complete with respect to classical phase models.
4 A Completeness Proof for Full Intuitionistic and Classical Linear Logics Based on the Proof Search Method
Now we move on to the problem if or not the proof search method can be extended to the full systems of intuitionistic linear logic (ILL) and classical linear logic (LL). As discussed in section 1, the standard countermodel construction from one open branch does not work for ILLand LL. Hence, in this section, we generalize the notion of branch in a proof search tree to the notion of OR-branching tree or simply OR-tree, and show that given an unprovable sequent Γ C, one can always find an open OR-tree, which is considered to retain enough information to refute the sequent (in§4.1). Then we describe how to construct an intuitionistic phase model from an open OR-tree of ILL (in §4.2) and a classical phase model from that of LL (in§4.3). These countermodel constructions give the completeness theorem (and the cut-elimination theorem as a corollary) both for ILLand for LL. In both cases, the closure condition of phase semantics plays an essential role.
4.1 OR-branching trees
Let L be an arbitrary sequent-based inference system of a logic, and S0 be an L-sequent.
An OR-branching tree (or, simply OR-tree) of S0 in Lis a rooted tree each node of which is labelled with an L-sequent, satisfying the following;
(1) The root is labelled with S0; (2) If a node x is labelled withS, and
(i) if no rule can be applied (bottom-up) toS, then x is a leaf ofR; (ii) otherwise, let
S11, . . . , Sm11
S ,
S12, . . . , Sm22 S , . . . ,
S1i, . . . , Smi i S , . . ..
be the enumeration of all instances of inference rules of L that can be applied (bottom-up) to S. Then, x has children nodes x1, x2, . . . and each xi is labelled with Sji for some 1≤j≤mi.
An OR-tree isopen if no node in it is labelled with an axiom.
Proposition 5 S0 is provable inL if and only if there is no open OR-tree of S0.
Proof. Assume that S0 has a proofπ inL. We show that if Ris an OR-tree ofS0, thenR contains at least one axiom by induction on length of π. If S0 is an axiom, then the claim is trivial. Suppose that the last part of π is of the form
S1, . . . , Sn
S0 (n≥1) .
Since Ris an OR-tree, Rshould contain someSi (1≤i≤n) as a child ofS0. But by IH the sub-OR-tree R’ of which the root is Si contains an axiom, hence so does R.
To show the reverse, observe that if S is not provable in Land S1, . . . , Sn
S (n≥1)
is an instance of an inference rule of L, then at least one of Si (1 ≤ i ≤ n) is unprovable.
Therefore, by choosing such an unprovable sequent at each stage of OR-tree construction (2ii), we can obtain an OR-tree in which each node is labelled with an unprovable sequent.
In particular, such an OR-tree contains no axiom.
If R is an OR-tree, let |R| be the set {S|S is a label of a node in R}, and R∗l be {∆|∆,ΠC ∈ |R|for some Π and C}.
4.2 Countermodel Construction for Intuitionistic Linear Logic
In this subsection, we consider the case ofILLand describe how to construct a intuitionistic phase model from a given open OR-tree.
LetRbe an open OR-tree incut-free ILL. Based onR, we define an intuitionistic phase modelMR = (M, Cl, K, v) as follows.
• M =R∗l ∪ {√
}, where √
is a distinguished formula not occurring in R. Note that the empty sequence ∅ is always in M.
• For each Γ∈M and ∆∈M, Γ·∆ =
Γ√,∆ if Γ,∆∈ R∗l otherwise.
In particular, √
·Γ = √
for any Γ ∈ M. It is immediate that < M,·,∅ > forms a commutative monoid.
• Let [[ΓC]] be{Σ∈M |Σ,ΓC∈ |R|}. We write [[C]] to denote [[C]].
• For X ⊆ M, Cl(X) = {[[Γ C]] |X ⊆ [[Γ C]], ΓC is a sequent of ILL}. Then clearly Cl([[ΓC]]) = [[ΓC]]. These facts are called base factsof MR.
• K ={!∆ |!∆∈M} ∪ {∅,√ }.
• v(α) = [[α]] for each atomic formulaα.
Lemma 6 The operator Cl defined above is actually a closure operator.
Lemma 7 Each factX =Cl(X) satisfies the follwing properties;
(i) √∈X;
(ii) ifA, B,Γ∈X and A⊗B,Γ∈M, then A⊗B,Γ∈X;
(iii) ifA,Γ∈X, B,Γ∈X, and A⊕B,Γ∈M, then A⊕B,Γ∈X; (iii)’ ifA,Γ∈X, B,Γ∈M, and A⊕B,Γ∈M, then A⊕B,Γ∈X; (iii)” if A,Γ∈M, B,Γ∈X, and A⊕B,Γ∈M, then A⊕B,Γ∈X;
(iv) if either A,Γ∈X or B,Γ∈X, and A&B,Γ∈M, then A&B,Γ∈X; (v) if B,Γ∈X, ∆A∈ |R|, and∆, A−◦B,Γ∈M, then ∆, A−◦B,Γ∈X; (vi) if A,Γ∈X and !A,Γ∈M, then !A,Γ∈X;
(vii) if !A,!A,Γ∈X, then !A,Γ∈X;
(viii) if Γ∈X and !A,Γ∈M, then !A,Γ∈X.
Proof. It suffices to show that the properties hold for each base fact [[∆ C]], since the above properties are preserved by arbitrary intersection.
As for (ii), for example, suppose A, B,Γ ∈ [[∆ C]], that means A, B,Γ,∆ C ∈ |R|. Since
A, B,Γ,∆C A⊗B,Γ,∆C
is an instance of an inference rule of cut-free ILL, A⊗B,Γ,∆ C is not in |R| by the definition of OR-trees, henceA⊗B,Γ∈[[∆C]]. The other properties are shown similarly.
Proposition 6 InMR, the following hold;
(a) if A is in R∗l, then A∈A∗;
(b) if ΓA∈ |R|, then Γ∈A∗.
Proof. We prove the following equivalent form (b’) instead of (b);
(b’) for any A, A∗ ⊆[[A]].
The proof is carried out by induction on the complexity of A.
(Case 1)A is an atomic formula. A ∈[[A]] =A∗ since |R| contains no axiom. (b’) is by definition.
(Case 2) A is of the form B ⊗C. As for (a), B ∈ B∗ and C ∈ C∗ by IH (induction hypotheses). Hence B, C ∈B∗C∗. Therefore, by Lemma 7(ii), B⊗C∈B∗⊗C∗.
As for (b’), B∗ ⊆[[B]] andC∗ ⊆ [[C]] by IH, hence B∗C∗ ⊆ [[B]][[C]]. To show [[B]][[C]] ⊆ [[B⊗C]], suppose that Γ1 ∈ [[B]] and Γ2 ∈[[C]], that mean Γ1 B ∈ |R| and Γ2 C ∈ |R|. Since
Γ1B Γ2C Γ1,Γ2 B⊗C
is an instance of ⊗r rule of cut-free ILL, Γ1,Γ2 B⊗C ∈ |R| by the definition of the OR- trees. Consequently, B∗C∗ ⊆[[B⊗C]] and we conclude thatB∗⊗C∗=Cl(B∗C∗)⊆[[B⊗C]].
(Case 3) A is of the form B −◦C. As for (a), it suffices to show that for any ∆ ∈ B∗,
∆·B−◦C ∈C∗. If ∆·B−◦C = √
, then√
∈C∗ by Lemma 7(i). Hence we may assume that ∆, B−◦C is inR∗l, i.e., ∆, B−◦C,ΠE ∈ |R| for some Π and E. Since
∆B C,ΠE
∆, B−◦C,ΠE
is an instance of −◦l rule of cut-freeILL, either ∆ B ∈ |R| or C,Π E ∈ |R|. However, the former is impossible by IH(b’). Hence the latter holds, and by IH(a), C∈C∗. Therefore by Lemma 7(v), ∆, B−◦C∈C∗.
As for (b’), assume that Γ ∈ B∗ −◦C∗. It suffices to show that Γ B −◦C ∈ |R|. If ΓB−◦C ∈ |R|, then Γ, BC would be also in|R|, thus Γ, B ∈[[C]]. But it is impossible because B ∈ B∗ by IH(a), Γ ∈ B∗−◦C∗ by assumption, and C∗ ⊆ [[C]] by IH(b’). Hence ΓB−◦C∈ |R|.
(Case 4) Ais of the form B&C. As for (a), since bothB and C are inR∗l,B ∈B∗ and C ∈C∗ by IH. Hence B&C ∈B∗ and B&C ∈C∗ by Lemma 7(iv). ThusB&C∈B∗&C∗. As for (b’), assume that Γ∈A∗&B∗. Then Γ∈[[B]] and Γ∈[[C]] by IH. It is immediate from the definition of the OR-trees that Γ B&C ∈ |R|.
(Case 5)A is of the formB⊕C. This is essentially the reverse of (Case 4). (a) is shown by using (iii), (iii)’ and (iii)” of Lemma 7. As for (b’), show that A∗∪B∗ ⊆[[A⊕B]].
(Case 6)A is of the form !B. As for (a),B ∈B∗ by IH (sinceB ∈ R∗l), hence !B ∈B∗ by Lemma 7(vi). On the other hand, !B ∈K by definition. Therefore !B ∈Cl(B∗∩K) =!B∗.
As for (b’), we show that B∗∩K ⊆[[!B]]. Assume that Γ ∈B∗∩K. If Γ ≡√
, then by Lemma 7(i). Otherwise Γ is of the form !∆ (the case that Γ is the empty sequece is shown
in the same way). If !∆!B ∈ |R|, then !∆ B would be also in |R|. But it is impossible because !∆∈[[B]] by IH. Therefore !∆!B ∈ |R|, and !∆∈[[!B]].
(Case 7)A is a logical constant. Immediate.
Theorem 2 (Completeness and Cut-Elimination) Let S0 be a sequent of ILL. Then the following are equivalent;
1. S0 is satisfied in every intuitionistic phase model;
2. S0 is cut-free provable in ILL; 3. S0 is provable in ILL.
Proof. 2 implies 3 trivially. 3 implies 1 by the usual soundness argument. Here we prove that 1 implies 2.
Suppose that S0 ≡A1, . . . , AnB is not provable in cut-free ILL. Then by Proposition 5, there is an open OR-tree R of S0, from which we can construct an intuitionistic phase model MR. By Proposition 6, Ai ∈A∗i for each 1 ≤ i ≤ n and A1, . . . , An ∈ B∗ in MR. Hence A∗1⊗ · · · ⊗A∗n ⊆B∗. ThusMR is a countermodel of S0, but it is impossible by the assumption.
4.3 Countermodel Construction for Classical Linear Logic
In this subsection, we sketch the countermodel construction in the case of classical logic.
For technical reasons, we employ the left one-sided formulation of classical linear logic (see Appendix B). Γ issatisfied in a classical phase model (M,⊥, K, v) if Γ∗ ⊆ ⊥. Note that
• Γis provable in left one-sided linear logic iffΓ⊥is provable in right one-sided linear logic, where Γ⊥ denotesA⊥1, . . . , A⊥n when Γ≡A1, . . . , An;
• Γ∗⊆ ⊥ iff 1∈Γ∗⊥.
Let R be an open OR-tree in cut-free LL. Based on R, we define an enriched classical phase model MR = (M,⊥, K, v) as follows;
• M is defined byR∗l ∪ {√} as before.
• ⊥={Σ∈M |Σ∈ |R|}.
• K ={!∆ |!∆∈M} ∪ {∅,√ }.
• v(α) ={α⊥}⊥ ={Σ∈M |Σ, α∈ |R|}.
Proposition 7 InMR, if A is in R∗l, then A∈A∗. Proof. By induction on the complexity of A.
Theorem 3 (Completeness and Cut-Elimination) LetS0 be a sequent ofLL. Then the following are equivalent;
1. S0 is satisfied in every classical phase model;
2. S0 is cut-free provable in LL; 3. S0 is provable in LL.
Proof. Similar to Theorem 2, using Proposition 7.
A Syntax of Intuitionistic Linear Logic
Roman capitalsA, B, . . . stand for formulas. The constants and the connectives of intuition- istic linear logic are classified into three groups;
• Multiplicatives: 1,A⊗B,A−◦B;
• Additives: ,0,A&B,A⊕B;
• Modality (Exponential): !A.
Greek capitals Γ1,Γ2,∆, . . . stand for finite multisets of formulas. A sequent ofILL is of the form ΓC. The inference rules ofILL are as follows;
Identity and Cut:
AA Identity ΓA A,∆C Γ,∆C Cut Multiplicatives:
A, B,ΓC
A⊗B,ΓC ⊗l ΓA ∆B
Γ,∆A⊗B ⊗r ΓC
1,ΓC 1l 1 1r ΓA B,∆C
Γ, A−◦B,∆C −◦l A,ΓB ΓA−◦B −◦r Additives:
A,ΓC B,ΓC
A⊕B,ΓC ⊕l ΓA
ΓA⊕B ⊕r1 ΓB
ΓA⊕B ⊕r2
0,ΓC 0l A,ΓC
A&B,ΓC &l1 B,ΓC
A&B,ΓC &l2 ΓA ΓB
ΓA&B &r Γ r Modality (Exponential):
A,ΓC
!A,ΓC !D !A,!A,ΓC
!A,ΓC !C ΓC
!A,ΓC !W !ΓA
!Γ!A !r Here !Γ stands for a multiset of the form !A1, . . . ,!An.
