So, it follows thatM,f(x)⊩Afor all assignments f. Then, it is immediate to see that Ais valid inM, as required.
□ Then an indirect proof of completeness ofGPALcan be provided as follows:
Corollary 3.3.1. Given any formulaAand labelx∈Var, the following are equivalent.
(i) Ais valid on all models.
(ii) ⊢HPAL A (iii) ⊢GPAL+⇒x:ϵA (iv) ⊢GPAL⇒x:ϵA
Proof. The direction from (i) to (ii) is established by Fact 1 and the direction from (ii) to (iii) is shown by Theorem 3.2.1. Then, the direction from (iii) to (iv) is established by the admissibility of (Cut) (Theorem 3.2.2). Finally, the direction from (iv) to (i) is
shown by Theorem 3.3.1 and Proposition 3.3.4. □
Proposition 3.4.1. ⇒x:⊥pist-valid in the world-deleting semantics.
Proof. We show t-validity of the sequent. Suppose for a contradiction that there is an assignment f : Var → W such that M,f ⊩ x:⊥p. Fix such f. Then we have M,f ⊩x:⊥pwhich is equivalent toM⊥,f(x)⊮pand f(x)∈ D(M⊥). However, since
D(M⊥)=∅, we obtain a contradiction. □
Proposition 3.4.2. ⊬GPAL⇒x:⊥p.
Proof. It suffices to show that sequent⇒(x:p)n,(x:⊥p)mis not derivable inGPALfor alln,m∈Nby induction of the height of the derivation.
Case of height=0. Since⇒(x:p)n,(x:⊥p)mis not an initial sequent, it is not derivable.
Case of height=k. We obtain the following possibilities:
⇒(x:p)n,(x:⊥p)m−1
⇒(x:p)n,(x:⊥p)m (Rw) ,
⇒(x:p)n−1,(x:⊥p)m
⇒(x:p)n,(x:⊥p)m (Rw) ,
⇒(x:p)n,(x:⊥p)m+1
⇒(x:p)n,(x:⊥p)m (Rc) ,
⇒(x:p)n+1,(x:⊥p)m
⇒(x:p)n,(x:⊥p)m (Rc) ,
⇒(x:p)n+1,(x:⊥p)m−1
⇒(x:p)n,(x:⊥p)m (Rat) .
Applying the induction hypothesis to each of the uppersequent (heightk−1) and subsequently applying the same rule, we obtain that the sequent is not derivable inGPAL.
□ As a result of Propositions 3.4.1 and 3.4.2, we conclude the following corollary.
Corollary 3.4.1. The following does not hold: for any sequentΓ ⇒ ∆, ifΓ ⇒ ∆is t-valid in the world-deleting semantics, then⊢GPALΓ⇒∆.
In what follows, we introduce our version of the link-cutting semantics of PAL and provide a direct proof of completeness ofGPALfor link-cutting semantics. 10 The specific definition of the link-cutting version of PAL’s semantics is given as follows, where we keep the symbol⊩for the previous world-deleting semantics of PAL and use the new symbol ‘|=’ for the satisfaction relation for the link-cutting semantics.
Definition 3.4.1(Link-cutting semantics of PAL). Given a modelM,w∈ D(M) and a formulaA,M, w|=Ais defined by
M, w|=p iff w∈V(p), M, w|=¬A iff M, w̸|=A,
M, w|=A→B iff M, w|=AimpliesM, w|=B,
M, w|=□aA iff for allv∈W :wRavimpliesM, v|=A,and M, w|=[A]B iff M, w|=AimpliesMA!, w|=B,
10Thanks to a comment from Makoto Kanazawa in the annual meeting of MLG2014 in Japan, we noticed that the link-cutting semantics may be suitable for our labelled sequent calculus of PAL.
where the restrictionMA!is defined by triple (W,(RA!a )a∈Agt,V) with
RaA!:=Ra∩(⟦A⟧M×⟦A⟧M), where⟦A⟧M:={x∈W|M,x|=A}.
According to this definition, only the accessibility relation is restricted toAinMA!, and the set of worlds and valuation stay as they were. Similar to the world-deleting seman-tics, we can also define the notion of validity in a model. The following soundness of HPALfor the link-cutting semantics is straightforward.
Proposition 3.4.3. IfAis a theorem ofHPAL, Ais valid in every modelMfor the link-cutting semantics.
As before, for any listα=(A1,A2, ...,An) of formulas , we defineMα! inductively as: Mα! :=M(ifα=ϵ), andMα! :=(Mβ!)An! =(W,(Rβa!,An!)a∈Agt,V) (ifα =β,An).
Now we can show that the corresponding notions tos- andt-validity become equivalent under our link-cutting semantics.
Definition 3.4.2. LetMbe a model andf :Var→ D(M) an assignment.
M,f |=x:αA iff Mα!,f(x)|=A M,f |=xRϵay iff (f(x),f(y))∈Ra
M,f |=xRα,aAy iff M,f |=xRαayandMα!,f(x)|=AandMα!,f(y)|=A By this definition, the next proposition immediately follows.
Proposition 3.4.4. For any modelM, assignment f,a∈Agtandx, y∈Var, M,f |=xRαay iff (f(x),f(y))∈Rαa!
The semantics of the negated form of a labelled expressionAis also defined as before.
Definition 3.4.3. LetMbe a model andf :Var→D(M) an assignment. Then, M,f |=x:αA iff Mα!,f(x)̸|=A,
M,f |=xRϵay iff (f(x),f(y))<Ra,
M,f |=xRα,aAy iff M,f ⊩xRαayorM,f ̸|=x:αAorM,f ̸|=y:αA
Now we may confirm that, based on the semantics,t-validity ands-validity are equiv-alent sinceM,f ̸|=Bis equivalent toM,f |=Bin this semantics.
Proposition 3.4.5. Under the link-cutting semantics, a sequentΓ⇒ ∆iss-valid in a modelMiffit ist-valid inM.
Proof. Suppose Γ ⇒ ∆is t-valid inM. In other words, if there is no assignment f : Var → D(M) such thatM,f |= Afor allA ∈ Γ, andM,f |= Bfor all B ∈ ∆. Equivalently, for all assignments f :Var→ D(M),M,f |=Afor allA∈Γ, there exists
B∈∆such thatM,f |=B. □
Because the notion of survival is expelled, the definition of the satisfaction of labelled expressions becomes wholly natural. Thus, we do not need to worry about the notion of survival of worlds in this link-cutting semantics.
Hereafter in this section we consider possibly infinite multi-sets of labelled expres-sions. That is, we callΓ⇒∆an infinite sequent ifΓor∆are infinite multi-sets. We use the notation⊢GPALΓ⇒∆to mean that there are finite multi-setsΓ′and∆′of labelled expressions such that⊢GPAL Γ′ ⇒ ∆′ in the ordinary sense andΓ′ ⊆ Γand∆′ ⊆ ∆. To establish the completeness result ofGPALfor the link-cutting semantics, we first introduce the notion of saturation as follows.
Definition 3.4.4. A possibly infinite sequent Γ ⇒ ∆is saturated if it satisfies the following:
(unprov) Γ⇒∆is not derivable inGPAL, (→l) ifx:αA→B∈Γ, thenx:αA∈∆orx:αB∈Γ, (→r) ifx:αA→B∈∆, thenx:αA∈Γandx:αB∈∆, (¬l) ifx:α¬A∈Γ, thenx:αA∈∆,
(¬r) ifx:α¬A∈∆, thenx:αA∈Γ,
(□al) ifx:α□aA∈Γ, thenxRαay∈∆ory:αA∈Γfor any labely, (□ar) ifx:α□aA∈∆, thenxRαay∈Γandy:αA∈∆for some labely, ([.]l) ifx:α[A]B∈Γ, thenx:αA∈∆orx:α,AB∈Γ,
([.]r) ifx:α[A]B∈∆, thenx:αA∈Γandx:α,AB∈∆, (atl) ifx:α,Ap∈Γ, thenx:αp∈Γ,
(atr) ifx:α,Ap∈∆, thenx:αp∈∆,
(rell) ifxRα,aAy∈Γ, thenx:αA∈Γandy:αA∈Γ, andxRαay∈Γ, and (relr) ifxRα,aAy∈∆, thenx:αA∈∆ory:αA∈∆, orxRαay∈∆.
We show the next lemma which states that any underivable sequent inGPALcan be extended to a (possibility infinite) saturated sequent.
Lemma 3.4.1. LetΓ ⇒ ∆be a finite sequent. If⊬GPAL Γ ⇒ ∆, then there exists a possibility infinite saturated sequentΓ+⇒∆+whereΓ⊆Γ+and∆⊆∆+.
Proof. Suppose that there is a finite sequentΓ ⇒ ∆such that⊬GPAL Γ ⇒ ∆. Let A1,A2, . . . be an enumeration of all labelled expressions such that each labelled ex-pression appears infinitely many times. We inductively construct an infinite sequence (Γi ⇒ ∆i)i∈Nof finite sequents such that⊬GPAL Γi ⇒ ∆iat eachi ∈Nas follows and defineΓ+⇒∆+as the ‘limit’ of such sequence.
LetΓ0⇒∆0beΓ⇒∆as the basis ofΓi⇒∆i, and by the supposition⊬GPALΓ0⇒
∆0. Thei+1-th step consists of the procedures to define an underivableΓi+1 ⇒ ∆i+1
fromΓi⇒∆idepending on the shape of the labelled expressionAi. In thei+1-th step, one of the following operations is executed.
Case whereAiis of the formx:αA→BandAi∈Γi: Because Γi ⇒ ∆i is underiv-able, eitherΓi ⇒ ∆i,x:αAor x:αB,Γi⇒ ∆iis also underivable by (L→). Then we choose one underivable sequent asΓi+1⇒∆i+1.
Case whereAiis of the formx:αA→BandAi∈∆i: We defineΓi+1⇒∆i+1:=x:αA,Γi⇒
∆i,x:αB. By (R→) and⊬GPALΓi⇒∆i, the sequentΓi+1⇒∆i+1is also underiv-able.
Case whereAiis of the formx:α¬AandAi∈Γi: We defineΓi+1 ⇒ ∆i+1 := Γi ⇒
∆i,x:αA. Because of (L¬) and⊬GPAL Γi ⇒ ∆i, the sequentΓi+1 ⇒ ∆i+1 is also underivable.
Case whereAiis of the formx:α¬AandAi∈∆i: We defineΓi+1 ⇒∆i+1:=x:αA,Γi⇒
∆i. Because of (R¬) and⊬GPAL Γi⇒ ∆i, the sequentΓi+1 ⇒∆i+1is also under-ivable.
Case whereAiis of the formx:α[A]BandAi∈Γi: We defineΓi+1⇒∆i+1as either Γi ⇒ ∆i,x:αAor x:α,AB,Γi ⇒ ∆i. Because of (L[.]) and⊬GPAL Γi ⇒ ∆i, the sequentΓi+1⇒∆i+1is also underivable.
Case whereAiis of the formx:α[A]BandAi∈∆i: We defineΓi+1⇒∆i+1:=x:αA,Γi⇒
∆i,x:α,AB. Because of (R[.]) and⊬GPALΓi⇒∆i, the sequentΓi+1⇒∆i+1is also underivable.
Case whereAiis of the formx:α,ApandAi∈Γi: We defineΓi+1⇒∆i+1:=x:αp,Γi⇒
∆i. Because of (Lat′) and⊬GPAL Γi⇒∆i, the sequentΓi+1 ⇒∆i+1is also under-ivable.
Case whereAiis of the formx:α,ApandAi∈∆i: We defineΓi+1 ⇒ ∆i+1 := Γi ⇒
∆i,x:αp. Because of (Rat′) and⊬GPAL Γi ⇒∆i, the sequentΓi+1 ⇒ ∆i+1is also underivable.
Case whereAiis of the formx:α□aAandAi∈Γi: Let{y1, ..., yn}be the set of all la-bels appearing inΓi⇒∆i. Suppose we have constructed (Γ(k)i ⇒∆(k)i )1≤k≤ℓsuch that (Γ(k)i ⇒ ∆(k)i ) is underivable,Γ(k)i ⊆ Γ(ki +1), and∆(k)i ⊆ ∆(ki+1). Because of (L□a) and⊬GPAL Γ(l)i ⇒ ∆(l)i , eitherΓ(l)i ⇒ ∆(l)i ,xRαayℓ+1oryl+1:A,Γ(l)i ⇒ ∆(l)i is underivable, and we choose one underivable sequent asΓ(li+1)⇒∆(li+1). Then we defineΓi+1⇒ ∆i+1 := Γ(n)i ⇒∆(n)i , andΓi+1 ⇒∆i+1is underivable by construc-tion.
Case whereAiis of the formx:α□aAandAi∈∆i: We defineΓi+1⇒∆i+1 :=xRαay,Γi⇒
∆i, y:αA, whereyis a fresh variable that does not appear inΓi⇒∆i. Because of (R□a) and⊬GPALΓi⇒∆i, the sequentΓi+1 ⇒∆i+1is also underivable.
Case whereAiis of the formxRα,aAyandAi∈Γi: We defineΓi+1⇒∆i+1:=x:αA, y:αA,xRαay,Γi⇒
∆i. Because of (Lrel) and⊬GPALΓi⇒∆i, the sequentΓi+1⇒∆i+1is also under-ivable.
Case whereAiis of the formxRα,aAyandAi∈∆i: We defineΓi+1 ⇒ ∆i+1 as either Γi ⇒∆i,x:αAorΓi⇒ ∆i, y:αAorΓi ⇒∆i,xRαay. Because of (Rrel) and⊬GPAL
Γi⇒∆i, the sequentΓi+1⇒∆i+1is also underivable.
Otherwise: We defineΓi+1⇒∆i+1:= Γi⇒∆i. Finally, letΓ+⇒∆+be the union∪
i∈NΓi⇒∪
i∈N∆i. Then, it is routine to check that
Γ+⇒∆+is saturated andΓ⊆Γ+and∆⊆∆+. □
We now prove the completeness ofGPALfor the link-cutting semantics.
Theorem 3.4.1. If a sequentΓ ⇒ ∆is s-valid in every modelMfor the link-cutting semantics, then⊢GPAL Γ⇒∆.
Proof. We show its contraposition, and so suppose⊬GPAL Γ ⇒ ∆. By Lemma 3.4.1, there exists a saturated sequent Γ+ ⇒ ∆+ such that Γ ⊆ Γ+ and ∆ ⊆ ∆+. Using the saturated sequent, we construct the derived modelM =(W,(Ra)a∈Agt,V) from the saturated sequentΓ+⇒∆+.
• Wis a set of all labels appearing inΓ+⇒∆+,
• xRϵayiffxRϵay∈Γ+,
• x∈V(p) iffx:p∈Γ+.
In addition to this, letf :Var→Wbe an arbitrary assignment such that f(x)=x(ifx is inW). Then , we can establish the following two items:
(i) A∈Γ+impliesM,f |=A, (ii) A∈∆+impliesM,f ̸|=A.
The second item implies thatM,f(x)̸|=AhenceAis not valid in the derived model M. The proof for these two items is conducted by simultaneous induction on the length ofA. Here we only look at the cases whereAisx:α,Aporx:α□aA.
Case whereAisx:ϵp: (i) and (ii) are trivial by the definition ofM.
Case whereAisx:α,Ap: (i) Ifx:α,Ap∈Γ+, then by saturatedness, we havex:αp∈Γ+. Then by induction hypothesis,M,f |= x:αp is obtained. This is equivalent to Mα,f(x)|=p, i.e., f(x)∈V(p). HenceM,f |=x:α,Ap.
(ii) If x:α,Ap ∈ ∆+, then by the saturatedness, we have x:αp ∈ ∆+. Then by induction hypothesis,M,f ̸|=x:αpis obtained. This is equivalent to f(x)<V(p), and soM,f ̸|=x:α,Ap.
Case whereAisx:α¬A: (i) If x:α¬A ∈ Γ+. By Definition 3.4.4, x:αA ∈ ∆+. Then by induction hypothesis,M,f ̸|=x:αAis obtained. This is equivalent toM,f |= x:α¬A.
(ii) If x:α¬A ∈ ∆+, then by the saturatedness, we have x:αA ∈ Γ+. Then by induction hypothesis, M,f |= x:αAis obtained. This is equivalent to M,f ̸|= x:α¬A.
Case whereAisx:αA→B: (i) Ifx:αA → B ∈ Γ+. By Definition 3.4.4, x:αA ∈ ∆+ or x:αB ∈ Γ+. Then by induction hypothesis,M,f ̸|= x:αAorM,f |= x:αBis obtained. This is equivalent toM,f |=x:αA→B.
(ii) If x:αA → B ∈ ∆+, then by the saturatedness, we have x:αA ∈ Γ+ and x:αB ∈ ∆+. Then by induction hypothesis,M,f |= x:αAandM,f ̸|= x:αBare obtained. This is equivalent toM,f ̸|=x:αA→B.
Case whereAisx:α□aA: (i) Supposex:α□aA∈Γ+. What we show isM,f |=x:α□aA, i.e., for ally∈ D(M),xRαa!yimpliesMα!, y|=A. So, fix anyy∈ D(M) such that xRαa!y. Now it suffices to showMα!, y|=A. By Proposition 3.4.4, we haveM,f |= xRαay. Suppose for contradiction that xRαay ∈ ∆+. By induction hypothesis, M,f ̸|= xRαay. A contradiction. Therefore, xRαay < ∆+. Since Γ+ ⇒ ∆+ is saturated and x:α□aA ∈ Γ+, we havexRαay ∈ ∆+ory:αA ∈ Γ+. It follows that y:αA∈Γ+, henceMα!, y|=Aby induction hypothesis. (ii) Supposex:α□aA∈∆+. By Definition 3.4.4, xRαay ∈ Γ+ and y:αA ∈ ∆+, for some y. By induction hypothesis,M,f |= xRαayandM,f ̸|=y:αA, for somey. By Proposition 3.4.4, the definition of f and Definition 3.3.1, (x,f(y))∈ Rαa!andMα!,f(y)̸|= A, for somey. Then, we get the goal:M,f ̸|=x:α□aA.
Case whereAisx:α[A]B: (i) If x:α[A]B ∈ Γ+. By Definition 3.4.4, x:αA ∈ ∆+ or x:α,AB ∈ Γ+. Then by induction hypothesis, M,f ̸|= x:αA orM,f |= x:αBis obtained. This is equivalent toM,f |=x:αA→B.
(ii) If x:αA → B ∈ ∆+, then by the saturatedness, we have x:αA ∈ Γ+ and x:αB ∈ ∆+. Then by induction hypothesis,M,f |= x:αAandM,f ̸|= x:αBare obtained. This is equivalent toM,f ̸|=x:αA→B.
Case whereAisxRϵay: (i) and (ii) are trivial by the definition ofM.
Case whereAisxRα,aAy: (i) If xRα,aAy ∈ Γ+. By Definition 3.4.4, x:αA ∈ Γ+ and y:αA ∈ Γ+ andxRαay ∈ Γ+. Then by induction hypothesis, M,f |= x:αA and M,f |=y:αAandM,f |=xRαayare obtained. This is equivalent toM,f |=xRα,aAy. (ii) If xRα,aAy, then by the saturatedness, we have x:αA ∈ ∆+or y:αA ∈ ∆+ or xRαay ∈ ∆+. Then by induction hypothesis, M,f ̸|= x:αA or M,f ̸|= y:αA or M,f ̸|=xRαayis obtained. This is equivalent toM,f ̸|=xRα,aAy.
□ Since in the link-cutting semantics GPAL is complete for any sequent by Theo-rem 3.4.1, there is a counter-model for the underivable sequent⇒ x:⊥p in GPAL (this sequent ist-valid but not derivable as we have seen in Propositions 3.4.1 and 3.4.2 ).
Proposition 3.4.6. There is a model where sequent⇒ x:⊥pdoes not hold in the link-cutting semantics.
Proof. LetAgt =afor simplicity. Consider modelM=({w},∅,V) whereV(p)=∅, and f :Var → {w}such that f(x) =w. We show that inM,f ̸|=⇒ x:⊥p. This is, by Definition 3.4.2, toM⊥!, w̸|=p, and then by Definition 3.4.1, we obtainw<V(p)=∅.
It trivially holds. □
Corollary 3.4.2. Given any formulaAand labelx∈Var, the following are equivalent.
(i) Ais valid on all models for the world-deleting semantics.
(ii) ⊢HPAL A (iii) ⊢GPAL+⇒x:ϵA (iv) ⊢GPAL⇒x:ϵA
(v) Ais valid on all models for the link-cutting semantics.
Proof. The direction from (v) to (iv) is established by Theorem 3.4.1 and the direc-tion from (ii) to (v) is shown by Proposdirec-tion 3.4.3. Then, Corollary 3.3.1 implies the
equivalence between five items. □