Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents Lu´ıs Pinto1 and Tarmo Uustalu2 1Centro de Matem´atica, UniversidadedoMinho, Campus de Gualtar, P-4710-057 Braga, Portugal [email protected] 2Institute of Cybernetics at Tallinn University of Technology, Akadeemia tee 21, EE-12618 Tallinn, Estonia [email protected] Abstract. Bi-intuitionistic logic is a conservative extension of intu- itionistic logic with a connective dual to implication, called exclusion. We present a sound and complete cut-free labelled sequent calculus for bi-intuitionistic propositional logic, BiInt, following S. Negri’s general methodfordevisingsequentcalculifornormalmodallogics.Althoughit arises as a natural formalization of the Kripke semantics, it is does not directly support proof search. To describe a proof search procedure, we develop a more algorithmic version that also allows for counter-model extraction from a failed proof attempt. 1 Introduction Bi-intuitionisticlogic(alsoknownasHeyting-Brouwerlogic,subtractivelogic)is an extension of intuitionistic logic with a connective dual to implication, called exclusion (coimplication, subtraction), a symmetrization of intuitionistic logic. It first got the attention of C. Rauszer [14,15,16], who studied its algebraic and Kripke semantics, alongside adequate Hilbert-style systems and sequent calculi. More recently, it has been of interest to L(cid:2)ukowski [9], Restall [17], Crolard [2] and Gor´e with colleagues [6,1,7,8]. Part of the motivation is the expected com- putational significance of the logic: one would expect proof systems working as languages for programming with values and continuations in a symmetric way. Aparticularityofbi-intuitionisticlogicisthatitadmitssimplesequentcalculi obtained from the standard ones for intuitionistic logic essentially by dualizing the rule for implication. Although several authors have stated or “proved” that these calculi enjoy cut elimination (most notably Rauszer [15] for her sequent calculus), they arein fact incomplete without cut and thus notdirectly suitable for backward(i.e., root-first)proofsearch.The reasonsof the failure are similar to those for the modal logic S5 (S4 + symmetry) and the future-past tense logic KtT4 (S4 + modalities for the converse of the accessibility relation). A closer analysis suggests that finding remedies that are satisfactory, both from M.GieseandA.Waaler(Eds.):TABLEAUX2009,LNAI5607,pp.295–309,2009. (cid:2)c Springer-VerlagBerlinHeidelberg2009 296 L. Pinto and T. Uustalu the structural proof theory and automated theorem proving points of view, is challenging and provides insights into the subtleties of the logic. In this paper we propose one solution to the problem. We describe a cut-free labelled sequent calculus for bi-intuitionistic propositional logic, BiInt, where thelabelsareinterpretedasworldsinKripkestructures.Exploitingthefactthat BiInt admits a translation to the future-past tense logic KtT4, we obtain it by the general method of S. Negri [12] for devising sequent calculi for normal modal logics. Then, to formulate a search procedure and obtain a termination argumentwefine-tuneitfortheconstructivelogicsituationwithmonotonicityof truth.ThisapproachisinlinewithS.Negri’smethodwhereframeconditionsare uniformlytransformedintoinferencerules,butterminationofproofsearchofthe resultingsequentcalculusmustbeobtainedonacase-by-casebasis.Interestingly, bi-intuitionistic logic turns out to be a rather delicate case. Cut-free sequent calculi for BiInt have also been proposed by Gor´e and col- leagues. Gor´e’s first formulation [6] was in the display logic format, inspired by a general method for devising display systems for normal modal logics. The nextformulationbyPostnieceandGor´e[1,7]achievescut-freedombycombining refutation with proof (passing failure information from premise to premise) to be able to glue counter-models together without the risk of violating the mono- tonicity condition of interpretations. The new nested sequent calculus by Gor´e, Postniece and Tiu [8] is a refinement of the display logic version and basically allows reasoning in a local world of a Kripke structure with references to facts about its neighbouring worlds captured in the nested structure. The paper is organized as follows. In Sect. 2, we introduce BiInt with its Kripke semantics and the translation to KtT4. We also show its Dragalin-style sequentcalculusandwhycuteliminationfails.InSect.3,weintroducealabelled sequent calculus for BiInt designed according to S. Negri’s recipe. In Sect. 4, we refine this declarative system into a more algorithmic version, show that it is sound and its rules also preserve falsifiability. In the next section (Sect. 5) we define a proof search procedure for the calculus and show that it terminates. In Sect. 6 we put the pieces together to conclude completeness. In the final section we sum up and outline some directions for further enquiry. 2 Bi-intuitionistic Propositional Logic, Dragalin-Style Sequent Calculus and Failure of Cut Elimination WestartbydefiningthelogicBiInt.Thelanguageextendsthatofintuitionistic propositionallogic,Int,byoneconnective,exclusion,thustheformulaearegiven by the grammar: A,B :=p|(cid:2)|⊥|A∧B |A∨B |A⊃B |A(cid:2)B where p ranges over a denumerable set of propositional variables which give us atoms; the formula A (cid:2) B is the exclusion of B from A. We do not take negationsasprimitive,butin additiontothe intuitionistic (or strong)negation, Proof Search and Counter-Model Construction 297 we have dual-intuitionistic (or weak) negation, definable by ¬A := A⊃⊥ and (cid:2)A:=(cid:2)(cid:2)A. The Kripke semantics defines truth relative to worlds in Kripke structures thatare the sameas for Int. A Kripke structure is a triple K =(W,≤,I)where W is a non-empty set whose elements we think of as worlds, ≤ is a preorder (reflexive-transitivebinaryrelation)onW (theaccessibility relation)andI—the interpretation—is anassignmentofsets ofpropositionalvariablesto the worlds, which is monotone w.r.t. ≤, i.e., whenever w ≤w(cid:3), we have I(w)⊆I(w(cid:3)). Truth in Kripke structures is defined as for Int, but covers also exclusion, interpreted dually to implication as possibility in the past: – w |=p iff p∈I(w); – w |=(cid:2) always; w|=⊥ never; – w |=A∧B iff w |=A and w |=B; w|=A∨B iff w|=A or w |=B; – w |=B⊃A iff, for any w(cid:3) ≥w, w(cid:3) (cid:11)|=B or w(cid:3) |=A; – w |=A(cid:2)B iff, for some w(cid:3) ≤w, w(cid:3) |=A and w(cid:3) (cid:11)|=B. Aformulaiscalledvalid ifitistrueinallworldsofallstructures.Itiseasytosee that monotonicity extends from atoms to all formulae thanks to the universal and existential semantics of implication and exclusion. It is alsoabasic observationthat the Go¨deltranslationofInt into the modal logic S4 extends to a translationinto the future-past tense logic KtT4 (cf. [9]). As the semantics of KtT4 does not enforce monotonicity of interpretations, atoms must be translated as future necessities or past possibilities (these are always monotone): p# =(cid:3)p (or (cid:4)p); (cid:2)# =(cid:2); ⊥# =⊥; (A∧B)# =A#∧B#; (A∨B)# =A#∨B#; (B⊃A)# =(cid:3)(B#⊃A#); (A(cid:2)B)# =(cid:4)(A#(cid:2)B#). A sequent calculus for BiInt is most easily obtained from Dragalin’s sequent calculus for Int (as has been done by Restall [17] and Crolard [2]; Rauszer’s [15] original sequent calculus was different). In Dragalin’s system sequents are multiple-conclusion,butthe implication-rightrule isconstrained.Theextension imposesadualconstraintontheexclusion-leftrule.Thesequents arepairsΓ (cid:12)Δ where Γ,Δ (the antecedent and succedent) are finite multisets of formulae (we omit braces and denote union by comma as usual). Such a sequent is taken to be valid if, for any Kripke structure K and world w, some formula in Γ is false or some formula in Δ is true. The inference rules are displayed in Fig. 1. NotethatthecontextΔismissinginthepremiseofthe⊃Rruleandduallyin the premise of (cid:2)L we do not have the context Γ. The rules ⊃L and (cid:2)R involve some contraction. This is necessary because we have chosen not to include a general contraction rule. Thiscalculusissoundandcompletew.r.t.theabove-definednotionofvalidity (completeness can be shown going through the algebraic semantics in terms of Heyting-Brouweralgebras[14]). Howeverit is incomplete without cut, as shown byPintoandUustaluin2003(privateemailmessagefromT.UustalutoR.Gor´e, 13 Sept. 2004, quoted in [1]). It suffices to consider the obviously valid sequent 298 L. Pinto and T. Uustalu initialrule andcut: Γ (cid:4)A,Δ Γ,A(cid:4)Δ hyp cut Γ,A(cid:4)A,Δ Γ (cid:4)Δ logicalrules: Γ (cid:4)Δ Γ,A,B(cid:4)Δ Γ (cid:4)A,Δ Γ (cid:4)B,Δ (cid:5)L (cid:5)R ∧L ∧R Γ,(cid:5)(cid:4)Δ Γ (cid:4)(cid:5),Δ Γ,A∧B(cid:4)Δ Γ (cid:4)A∧B,Δ Γ (cid:4)Δ Γ,A(cid:4)Δ Γ,B(cid:4)Δ Γ (cid:4)A,B,Δ ⊥L ⊥R ∨L ∨R Γ,⊥(cid:4)Δ Γ (cid:4)⊥,Δ Γ,A∨B(cid:4)Δ Γ (cid:4)A∨B,Δ Γ,B⊃A(cid:4)B,Δ Γ,A(cid:4)Δ Γ,B(cid:4)A ⊃L ⊃R Γ,B⊃A(cid:4)Δ Γ (cid:4)B⊃A,Δ A(cid:4)B,Δ Γ (cid:4)A,Δ Γ,B(cid:4)A(cid:2)B,Δ (cid:2)L (cid:2)R Γ,A(cid:2)B(cid:4)Δ Γ (cid:4)A(cid:2)B,Δ Fig.1. Dragalin-style sequent calculus for BiInt p(cid:12)q,r⊃((p(cid:2)q)∧r). The only possible last inference in a proof could be ? p,r(cid:2)(p(cid:2)q)∧r ⊃R p(cid:2)q,r⊃((p(cid:2)q)∧r) but the premise is invalid as the succedent formula q has been lost. With cut, the sequent is proved as follows: hyp hyp p,p(cid:2)q,r(cid:2)p(cid:2)q p,p(cid:2)q,r(cid:2)r hyp hyp ∧R p(cid:2)q,p,... p,q(cid:2)q,p(cid:2)q,... p,p(cid:2)q,r(cid:2)(p(cid:2)q)∧r (cid:2)R ⊃R p(cid:2)q,p(cid:2)q,... p,p(cid:2)q(cid:2)q,r⊃((p(cid:2)q)∧r) cut p(cid:2)q,r⊃((p(cid:2)q)∧r) Cut elimination fails as we cannot permute the cut on the exclusion p(cid:2)q up past the ⊃R inference for which the cut formula is a side formula. This is one type of cuts that cannot be eliminated, there are altogether 3 such types [11]. This situation is similar to the naive sequent calculus for S5 where the sequent p (cid:12) (cid:3)♦p cannot be proved without cut, but can be proved by applying cut to the sequents p(cid:12)♦p and ♦p(cid:12)(cid:3)♦p that are provable without cut. 3 L: A Labelled Sequent Calculus We now proceed to a labelled sequent calculus for bi-intuitionistic logic that we callL.Thiscalculusturnsouttobecompletewithoutacutrule.Essentiallyitis aformalizationofthefirst-ordertheoryoftheKripkesemanticsinsuchafashion that the extralogical axioms corresponding to the reflexivity-transitivity condi- tiononframesandmonotonicityconditiononinterpretationsdonotnecessitate cut. Our design follows the method of S. Negri [12]. Weproceedfromadenumerablesetoflabels.Alabelled formulaisapairx:A wherexisalabelandAaformula.Theintendedmeaningistruthoftheformula at a particular world. Proof Search and Counter-Model Construction 299 preorderrules: Γ (cid:2)G∪{(x,x)}Δ xGy yGz Γ(cid:2)G∪{(x,z)}Δ refl trans Γ (cid:2)GΔ Γ (cid:2)GΔ initialruleandmonotonicityrules: hyp xGy Γ,x:A,y:A(cid:2)GΔ monL yGx Γ (cid:2)Gy:A,x:A,Δ monR Γ,x:A(cid:2)Gx:A,Δ Γ,x:A(cid:2)GΔ Γ(cid:2)Gx:A,Δ logicalrules: Γ (cid:2)GΔ Γ,x:A,x:B(cid:2)GΔ Γ (cid:2)Gx:A,Δ Γ (cid:2)Gx:B,Δ (cid:3)L (cid:3)R ∧L ∧R Γ,x:(cid:3)(cid:2)GΔ Γ(cid:2)Gx:(cid:3),Δ Γ,x:A∧B(cid:2)GΔ Γ (cid:2)Gx:A∧B,Δ Γ (cid:2)GΔ Γ,x:A(cid:2)GΔ Γ,x:B(cid:2)GΔ Γ (cid:2)Gx:A,x:B,Δ ⊥L ⊥R ∨L ∨R Γ,x:⊥(cid:2)GΔ Γ(cid:2)Gx:⊥,Δ Γ,x:A∨B(cid:2)GΔ Γ(cid:2)Gx:A∨B,Δ xGy Γ(cid:2)Gy:B,Δ Γ,y:A(cid:2)GΔ y∈/G,Γ,Δ Γ,y:B(cid:2)G∪{(x,y)}y:A,Δ ⊃L ⊃R Γ,x:B⊃A(cid:2)GΔ Γ (cid:2)Gx:B⊃A,Δ y∈/G,Γ,Δ Γ,y:A(cid:2)G∪{(y,x)}y:B,Δ yGx Γ (cid:2)Gy:A,Δ Γ,y:B(cid:2)GΔ (cid:2)L (cid:2)R Γ,x:A(cid:2)B(cid:2)GΔ Γ (cid:2)Gx:A(cid:2)B,Δ Fig.2. Labelled sequent calculus L Sequents are triples Γ (cid:12)G Δ where Γ and Δ are finite multisets of labelled formulae, and G is a finite binary relation on labels called the graph. Graphs area means to keeptrackoflabel dependencies andthus induce anaccessibility relation on worlds. The inference rules are presented in Fig. 2. Some of them have provisos,that we also write as rule premises. We let xGy abbreviate (x,y) ∈ G. Following usual sequent calculus terminology, at a given rule, we call the explicit labelled formulaintheconclusionthelabelled formula introducedbytheruleorthemain labelled formulaoftheruleandtheexplicitlabelledformulaeinthepremisesthe side labelled formulae. The interestinglogicalrulesarethose forimplicationandexclusionwhichare dual. Notice the freshness condition on the label y in the rules ⊃R and (cid:2)L, guaranteeing their soundness. We call label y the eigenlabel of the rule and x the parent of y. Note also the presence of the monotonicity rules accounting for propagation of truth (resp. falsity) to future (resp. past) worlds and preorder rules which account for reflexivity and transitivity of accessibility. Thecounter-exampletocuteliminationfortheDragalin-stylesequentcalculus is proved in L as follows: hyp hyp x:p,y:r(cid:2)(x,y)x:q,x:p x:p,y:r,x:q(cid:2)(x,y)x:q (cid:2)R hyp x:p,y:r(cid:2)(x,y)x:q,y:p(cid:2)q x:p,y:r(cid:2)(x,y)x:q,y:r ∧R x:p,y:r(cid:2)(x,y)x:q,y:(p(cid:2)q)∧r ⊃R x:p(cid:2)∅x:q,x:r⊃((p(cid:2)q)∧r) 300 L. Pinto and T. Uustalu Noticethedownwardinformationpropagationinthe(cid:2)Rinferencetoanalready existing label. In a L-derivationthe names ofthe eigenlabels canbe changed(to new names notoccurringinthederivation)withoutchangingtheendsequent.Thisproperty allowsustoshowbyusualmethodsthatLenjoysadmissibilityoftheweakening rules. A simple combination of the monotonicity, reflexivity and weakening also guarantees admissibility of the contraction rules in L. (This is what enables us to avoid explicit contractions at ⊃L and (cid:2)R rules.) Thecutrule isalsoadmissibleinL.Thiscanbeprovedalongthelinesofcut eliminationresultsofS.Negriforlabelledsequentcalculiformodallogics.Inthis paper,asanimmediate consequenceofsoundnessandcompletenessofsystemL w.r.t. the Kripke semantics (Cor. 1), we get a semantical proof of admissibility of cut. GivenaKripkestructureK,aK-valuationisamappingfromthesetoflabels to the set of worlds of K. Definition 1. A Kripke structure K = (W,≤,I) and a K-valuation v are a counter-model (cm) to an L-sequent Γ (cid:12)G Δ, if: i) for all xGy, v(x)≤v(y); ii) for all x : A ∈ Γ, v(x) |= A; and iii) for all x : A ∈ Δ, v(x) (cid:11)|= A. The sequent is valid, if it has no counter-model. Proposition 1 (Soundness of L). If Γ (cid:12)G Δ is derivable, Γ (cid:12)G Δ is valid. Completenessholdsaswell(Cor.1)andisprovedwiththehelpofthealgorithmic version of L introduced in the next section. In fact our completeness argument allows for construction of counter-models of non-derivable sequents. 4 L∗: An Algorithmic Version of L Although L constitutes a good basis for backward proof search for bi- intuitionistic propositional logic, it still faces the problem that the preorder and monotonicity rules can be applied at any point in backward proof search. To deal with this problem, we introduce now an algorithmic version of L called L∗. System L∗ does not have explicit preorder or monotonicity rules. It uses a marking mechanism on certain kinds of labelled formulae. Such mechanism allowsfortherecoveringoflabelledformulae,sothatmonotonicityrequirements are guaranteed. The marking mechanism is also designed in a way that it can be used in loop-detection, to avoid infinite search along paths corresponding to non-derivable sequents. Sequents in L∗ are triples Γ (cid:12)G Δ as in L, with the difference that, in the contexts Γ and Δ, labelled formulae can now be marked either with ∗ (written as x : A∗), ◦ (written as x : A◦) or with • (written as x : A•). The rules of L∗ are in Fig. 3. Letusbrieflyexplaintheroleof+ and−andofmarks∗,◦and•inbackward proof search. The + (resp. −) is used to propagate a formula to future (resp. past)labels(as determinedby the transitiveclosureofthe graph).The marking Proof Search and Counter-Model Construction 301 initialrule: hyp Γ,x:p◦(cid:2)Gx:p◦,Δ atomrules: Γ,p+,x:p∗,x:p◦(cid:2)GΔ Γ(cid:2)Gx:p◦,x:p∗,p−,Δ atomL atomR Γ,x:p(cid:2)GΔ Γ (cid:2)Gx:p,Δ wherep+={y:p|xGy} wherep−={y:p|yGx} logicalrules: Γ (cid:2)GΔ Γ,x:A,x:B(cid:2)GΔ Γ (cid:2)Gx:A,Δ Γ (cid:2)Gx:B,Δ (cid:3)L (cid:3)R ∧L ∧R Γ,x:(cid:3)(cid:2)GΔ Γ(cid:2)Gx:(cid:3),Δ Γ,x:A∧B(cid:2)GΔ Γ (cid:2)Gx:A∧B,Δ Γ (cid:2)GΔ Γ,x:A(cid:2)GΔ Γ,x:B(cid:2)GΔ Γ (cid:2)Gx:A,x:B,Δ ⊥L ⊥R ∨L ∨R Γ,x:⊥(cid:2)GΔ Γ(cid:2)Gx:⊥,Δ Γ,x:A∨B(cid:2)GΔ Γ(cid:2)Gx:A∨B,Δ Γ,(B⊃A)+,x:(B⊃A)∗(cid:2)Gx:B,Δ Γ,x:A(cid:2)GΔ ⊃L Γ,x:B⊃A(cid:2)GΔ where(B⊃A)+={y:B⊃A|xGy} x:(B⊃A)•∈/Δ y∈/G,Γ,Δ, Γ,Γy/x,y:B(cid:2)G∪{(x,y)}y:A,x:(B⊃A)•,Δ ⊃R Γ (cid:2)Gx:B⊃A,Δ whereΓy/x={y:C|x:C∗∈Γ}∪{y:p◦|x:p◦∈Γ} ∪{y:(C(cid:2)D)•|x:C(cid:2)D∈Γ orx:(C(cid:2)D)•∈Γ} x:(A(cid:2)B)•∈/Γ y∈/G,Γ,Δ Γ,x:(A(cid:2)B)•,y:A(cid:2)G∪{(y,x)}y:B,Δy/x,Δ (cid:2)L Γ,x:A(cid:2)B(cid:2)GΔ whereΔy/x={y:C|x:C∗∈Δ}∪{y:p◦|x:p◦∈Δ} ∪{y:(D⊃C)•|x:D⊃C∈Δorx:(D⊃C)•∈Δ} Γ (cid:2)Gx:A,Δ Γ,x:B(cid:2)Gx:(A(cid:2)B)∗,(A(cid:2)B)−,Δ (cid:2)R Γ (cid:2)Gx:A(cid:2)B,Δ where(A(cid:2)B)−={y:A(cid:2)B|yGx} Fig.3. Algorithmic version L∗ x:A∗ isdoneattheatomrules,⊃Land(cid:2)R(wherex:Aisthemainformula)in ordertobeabletorecoverAateventuallabelsstillunknownwhenx:Aisanal- ysed, but later created with a graph connection to x. The marking of a labelled formula with a ◦ (used only with atoms) or • (used only with implications and exclusions) means essentially that the formula was already analysed (the case with the explicit circles and bullets in the rule premises of the atom rules, ⊃R, (cid:2)L) or has no further useful information and so need not be analysed (the case with circles and bullets implicit in Γy/x and Δy/x in the premises of ⊃R and (cid:2)L respectively) and prevents a new analysis of the formula at the given world (notice that no rule introduces a labelled formula with a circle or a bullet). Notice that an L-sequent is also an L∗-sequent and that if we take an L∗- sequent and erase all ∗, ◦ and • marks we obtain an L-sequent. Given an L∗ 302 L. Pinto and T. Uustalu context Γ, we write Γ− for the L-context resulting from it by replacing all labelled formulae x : A∗, x : A◦ with unmarked labelled formulae x : A and removing all labelled formulae x : A•. Given an L∗-sequent Γ (cid:12)G Δ its erasure is the L-sequent Γ− (cid:12)G Δ−. We say that anL∗-rule is derivable in L if the rule obtained by replacing its premises and conclusion by their erasures is derivable in L. The next proposition shows that all L∗-rules are derivable in L and thus L∗ is sound w.r.t. L. Proposition 2 (SoundnessofL∗ w.r.t.L). 1.AllrulesofL∗ arederivable in L. 2. If Γ (cid:12)G Δ is derivable in L∗ then Γ− (cid:12)G Δ− is derivable in L. Becausethe rulesofL∗ donotthrowawayanyrelevantinformation(readback- ward, i.e., from the conclusion to the premises), they have the strong property thatacounter-modelofapremiseisalsoacounter-modeloftheconclusion.This is used in Sec. 6 for extracting counter-models out of failed proof attempts. Given a Kripke structure K = (W,≤,I), a K-valuation v and a graph G, ≤− denotes the relation ≤ \v(G)∗, i.e., ≤− is the relation obtained from ≤ by G G eliminating all pairs in the reflexive-transitive closure of {(v(x),v(y))|xGy}. Definition 2. A Kripke structure K = (W,≤,I) and a K-valuation v are a counter-model of an L∗-sequent Γ (cid:12)G Δ when: 1. for all xGy, v(x)≤v(y); 2. for all x:A,x:A◦ ∈Γ, v(x)|=A; 3. for all x:A∗ ∈Γ and for all w ∈W such that v(x)≤− w, w |=A; G 4. for all x:A,x:A◦ ∈Δ, v(x)(cid:11)|=A; 5. for all x:A∗ ∈Δ and for all w∈W such that w ≤− v(x), w(cid:11)|=A. G NoticethatforL-sequentsthisnotionofcounter-modelcoincideswiththenotion introduced in the previous section. As usual valid sequents are those for which there are no counter-models. Proposition 3 (Preservation of counter-models). For each L∗-rule, a counter-model of a premise is also a counter-model of the conclusion. 5 A Search Procedure and Its Termination WenowdescribeabackwardsearchprocedureforL∗,whichincorporatesaloop- checking mechanism, and prove it sound and terminating. As a by-product of the explicit presence in sequents of labels/worlds and the graph/accessibility relation,when the searchprocedure terminates with failure,we will be left with a Kripke counter-model of the given sequent. This fact is proved in the next section and accounts for the completeness of the search procedure. In order to describethesearchprocedure,weintroducefirstsometerminology,notationand also the loop-rules. The rules ⊃R and (cid:2)L are the only rules of L∗ where the graph relation variesinabackwardreading.We callthese rulesworld creating rules.Asequent Proof Search and Counter-Model Construction 303 y(cid:12)∈G Γ\Γ(y)(cid:4)GΔ[x/y] loopUp y(cid:12)∈G Γ[x/y](cid:4)GΔ\Δ(y) loopDn Γ (cid:4) Δ Γ (cid:4) Δ G∪{(x,y)} G∪{(y,x)} providedΓ[y]⊆Γ[x]∪Γ•[x],Γ∗[y]⊆Γ∗[x], providedΔ[y]⊆Δ[x]∪Δ•[x],Δ∗[y]⊆Δ∗[x], andΓ◦[y]⊆Γ◦[x] andΔ◦[y]⊆Δ◦[x] Fig.4. Loop rules Γ (cid:12)G Δ is calledsaturatedif it is irreducible w.r.t. the non-worldcreatingrules. A sequent Γ (cid:12)G Δ is called stuck when it is irreducible w.r.t. any rule and moreover it is not an axiom (hyp, ⊥L, (cid:2)R). Given an L∗ context Γ, we use the notations Γ[x], Γ∗[x], Γ◦[x], Γ•[x] and Γ(x)tomean{A|x:A∈Γ},{A|x:A∗ ∈Γ},{A|x:A◦ ∈Γ},{A|x:A• ∈Γ} and Γ[x]∪Γ∗[x]∪Γ◦[x]∪Γ•[x] respectively. The loop rules are presented in Fig. 4. (For a context Γ and labels x and y, the notation Γ[x/y] stands for the context obtained by replacing y with x in Γ.) Their backward reading corresponds to the action taken when a loop is detected and the detection of a loop corresponds to satisfaction of their side- conditions.Theformulationofthe looprulescorrespondstothe situationwhere x is the parentandthusy is adescendantofx, labeling necessarilysubformulae of x-labelled formulae. Wearenowinconditionsofpresentingthesearchprocedure.Itgoesasfollows: 1. Given an L∗-sequent Γ (cid:12)G Δ, we reduce it w.r.t. the non-world creating rules (i.e., we apply as long as possible these rules). We call a saturation both this process and the partial proof of Γ (cid:12)G Δ so constructed. The top sequent of each branch of a saturation is a saturated sequent. Notice also that the order in which rules are applied in saturation is unimportant since they are inter-permutable. 2. Then, for every branch in the saturation of Γ (cid:12)G Δ, we do the following: (a) wecheckifthetopsequentisanaxiomandifsosearchalongthebranch is stopped with success; (b) we checkifthere is aloop,i.e.,we testifthe side conditionofany ofthe loop rules is met, and if so proceed according to the corresponding loop rule. 3. If neither (a) nor (b) is the case, the development of the branch carries on, by applying one of the world creating rules, and we go back to 1.We stop with failure if no world creating rule can be applied. We call proof attempt both the run of the search procedure with a given sequent and the corresponding partial proof (in L∗ augmented with the loop rules).ThroughoutweassumethatproofattemptsalwaysstartwithL-sequents whosegraphsaretrees(i.e.,thegraph,seenasanundirectedgraphbyforgetting the directions of the arcs, is connected and acyclic). Then the graphs of all sequent in the proof attempt are trees. Proposition 4 (Soundness of the search procedure). If the proof attempt for an L-sequent terminates with success, then the sequent is L-derivable. 304 L. Pinto and T. Uustalu Proof: By induction on the height of the proof attempt, we prove that, for any L∗-sequent Γ (cid:12)G Δ in it, Γ− (cid:12)G Δ− is derivable in L. The cases corresponding to L∗-inferences follow by part 1. of Prop. 2. Consider the case correspond- ing to the loopUp rule of Fig. 4. (The case of loopDn is similar.) By IH we have that (Γ \Γ(y))− (cid:12)G Δ[x/y]− is L-derivable. From this, by weakening , Γ− (cid:12)G∪{(x,y)}(Δ\Δ(y))−,Δ(y)[x/y]−,Δ(y)−is alsoderivableinL.Since xGy, byrepeateduseofmonR,wecanderiveΓ− (cid:12)G∪{(x,y)} (Δ\Δ(y))−,Δ(y)−which is Γ− (cid:12)G∪{(x,y)}Δ−. (cid:3) Now we consider terminology, notation and lemmata used in particular for provingterminationofthe searchprocedure.Givena labelx, the world creation treeofxinducedbyabranchofaproofattempthasxasrootandhasassubtrees (if any) the world creation trees of each eigenlabel in the branch whose parent is x. Given a set of formulas S, mhf(S) stands for the maximal height of the formulae in S. Lemma 1. Any saturation in a proof attempt is finite. Proof: Observe that: (i) ∧ and ∨ inferences replace the main formula by strict subformulae; and (ii) even if the main formula of an atomL, atomR, ⊃L or (cid:2)R inference may reappear in the premises or upper sequents, it does so with a distinct label (as the graph is a tree) and thus can only reappear finitely many times (recall L∗-graphs are finite). (cid:3) Lemma 2. Given a label x and a branch B of a proof attempt, x has finitely many children in B. Proof: Notice that all formulae in a sequent of B are subformulae of a formula intheendsequentofB(whichisfinite)andthat,oncex:A⊃B (resp.x:A(cid:2)B) isanalysedasthemainformulaofa⊃R(resp.(cid:2)L)inference,x:(A⊃B)• (resp. x : (A (cid:2)B)•) is added to the succedent (resp. antecedent) of the inference’s premise, preventing that x:A⊃B (resp. x:A(cid:2)B) becomes analysed again.(cid:3) Lemma 3. For (cid:16)∈{∗,◦} and any saturated sequent Γ (cid:12)G∪{(x,y)} Δ in a proof attempt: i) if x:A(cid:16) ∈Γ, y :A(cid:16) ∈Γ; and ii) if y :A(cid:16) ∈Δ, x:A(cid:16) ∈Δ. Proof: Firstly notice that, for any L∗-rule, if z : B(cid:16) is in the antecedent (resp. succedent) of the conclusion, z : B(cid:16) is in the antecedent (resp. succedent) of any premise. Consider the case x : p◦ ∈ Γ (the other cases being similar or simpler).Thenx:p∗ ∈Γ andthus x:p musthavebeenthe mainformulainan atomL inference.LetΓ0 (cid:12)G0 Δ0 be the premise ofthatinference. If(x,y)∈G0, y : p ∈ Γ0 and any top sequent in the saturation of Γ0 (cid:12)G0 Δ0 has both y : p∗ and y : p◦ in the antecedent. If not, above the referred inference, there must be an ⊃R inference with eigenlabel y and parent x and the top sequents of the saturation of its premise have y :p∗ and y :p◦ in their antecedents. (cid:3) Lemma 4. Inaproofattempt,ifΓ0 (cid:12)G Δ0 istheconclusionofan⊃Rinference with eigenlabel x1 and parent x0 and Γ1 (cid:12)G∪{(x0,x1)} Δ1 is a top sequent in the saturation of the inference’s premise, then Γ (x )⊂Γ (x ). 0 0 1 1