Fei Liang Zhiguang Zhao

Abstract. Lehtinen (2008) introduced a new concept of validity of modal formulas,where quantification over binary relations is allowed for the so called “helper modalities”,and the “boss modalities” are similar to ordinary modalities in modal logic in the sense that they are interpreted as a fixed binary relation in a Kripke frame.In the present paper,we study the correspondence theory for this validity notion.We define the class of Sahlqvist formulas for this validity notion,each formula of which has a first-order frame correspondent,and define the algorithm ALBARQ to compute the first-order correspondents of this class.

1 Introduction

Lehtinen ([6]) introduced a new concept of validity of modal formulas,which allows,from the perspective of second-order logic,quantification over binary relations.In this definition of validity,if the modal similarity type isτ={◇1,...,◇n},then we say that the modal formulaφisτ-valid in a setW(notationW?τ φ) iff it is valid in each frame F=(W,R1,...,Rn).With the help of the standard translation,assume that onlyp1,...,pkoccur inφ,then theτ-validity in a setWcan be equivalently written as:

As is shown in[6,Example 5.1.2,5.1.3],this notion of validity can be used to define the size of the domain.Indeed,takeτ={◇},

In this definition,set validity allows us to talk about the size of a domain,but we lose the possibility to talk about relations.Therefore,Lehtinen proposes a more general perspective by allowing some relations to behelpersand others to bebosses,such that we only quantify over the helpers and keep the bosses similar to the standard Kripke frame validity.

In the new definition,the similarity typeτis defined to be the disjoint union ofτHandτB,where modalities inare calledhelpers,and modalities inare calledbosses.

We say that a formula isτH-validin a frame(W,R1,...,Rn),if

for all helper relationsH1,...,Hm.With the help of the standard translation,theτH-validityin F=(W,R1,...,Rn)can be reformulated as

With the notion ofτH-validity,we can use modal formulas to define first-order properties of Kripke frames that cannot be defined using standard validity notion.

Example 1(Example 5.1.7 in[6]).LetτB={◇},τH={◇H},and F=(W,R).Then we have

In the present paper,we study the Sahlqvist correspondence theory of this validity notion,namely,we define a class of Sahlqvist formulas in the modal language of helpers and bosses,and define an Ackermann Lemma Based Algorithm ALBARQ1Here RQ stands for “relation quantifier”.to compute the first-order correspondents of Sahlqvist formulas.

The structure of the paper is organized as follows: Section 2 presents preliminaries on modal logic of helpers and bosses.Section 3 defines Sahlqvist formulas and inequalities.Section 4 defines the expanded modal language,the first-order correspondence language and the standard translation,which will be used in the algorithm.Section 5 defines the Ackermann Lemma Based Algorithm ALBARQ.Section 6 proves the soundness of the algorithm.Section 7 shows that ALBARQsucceeds on Sahlqvist formulas.Section 8 gives some examples.Section 9 gives conclusions.

2 Preliminaries

In the present section,we collect the preliminaries on modal logic with helpers and bosses.For more details,see[6,Section 5].

2.1 Language and Syntax

Definition 1.Given a set Prop of propositional variables,a finite setτH={,...,},a finite setsuch thatτH ∩τB=?,the modal language with helpers and bosses is defined recursively as follows:

wherep ∈Prop,◇∈τH ∪τB. □and?are defined in the standard way.We call a formulapureif it contains no propositional variables.We useτ:=(τH,τB) to denote thesimilarity typeof the language.Throughout the article,we will also make substantial use of the following expressions:

(1) Aninequalityis of the formφ ≤ψ,whereφandψare formulas.

(2) Aquasi-inequalityis of the formφ1≤ψ1& ...&φn ≤ψn ?φ ≤ψ.

We will find it easy to work with inequalitiesφ ≤ψin place of implicative formulasφψin Section 3.

2.2 Semantics

Definition 2.Given a similarity typeτ=(τH,τB),aτ-Kripke frameis a tuple F=(W,R1,...,Rn,H1,...,Hm)whereW≠ ?is thedomainof F,R1,...,Rn,H1,...,Hmareaccessibility relationswhich are binary relations onW,and eachRicorresponds to,eachHicorresponds to.The underlyingτB-Kripke frameof aτ-Kripke frame is a tuple F=(W,R1,...,Rn)where eachRicorresponds torespectively and no relations forare there.τB-Kripke frames are used to define validity.Aτ-Kripke modelis a pair M=(F,V)where F is aτ-Kripke frame andV: Prop(W) is avaluationon F.Now the satisfaction relation is defined as follows2The basic case and the Boolean cases are defined as usual,and here we only give the clauses for the modalities.: given anyτ-Kripke model M=(W,R1,...,Rn,H1,...,Hm,V),anyw ∈W,

For any formulaφ,we let?φ?M={w ∈W|M,w?φ}denote thetruth setofφin M.The formulaφisglobally trueon M(notation:M ?φ)if?φ?M=W.The crucial difference between modal logic with helpers and bosses and ordinary modal logic is the definition of validity.Validity in the former is only defined onτB-Kripke frames:Aτ-formulaφisvalidon aτB-Kripke frame F=(W,R1,...,Rn)(notation:F ?φ)ifφis globally true on(F,H1,...,Hm,V)for all helper relationsH1,...,Hmand all valuationsV.The semantics of inequalities and quasi-inequalities are given as follows:

The definitions of validity are similar to formulas.It is easy to see thatt M ?φ ≤ψiff M ?φψ.

3 Sahlqvist Formulas and Inequalities

In this section,we define Sahlqvist formulas and inequalities in the similarity typeτ,in the style of unified correspondence[2].We collect preliminaries here.

Definition 3(Order-type).(cf.[4,p.346])For ann-tuple(p1,...,pn)of propositional variables,an order-typeεis an element in{1,?}n.We say thatpihas ordertype 1(resp.?)with respect toεifεi=1(resp.εi=?),and denoteε(pi)=1(resp.ε(pi)=?).We useε?to denote the order-type whereε?(pi)=1(resp.ε?(pi)=?)iffε(pi)=?(resp.ε(pi)=1).

Definition 4(Signed generation tree).(cf.[5,Definition 4])Thepositive(resp.negative)generation treeof anyτ-formulaφis defined by first labelling the root of the generation tree ofφwith+(resp.-)and then labelling the children nodes as follows:

· Assign the same sign to the children nodes of any node labelled with ∨,∧,,

· Assign the opposite sign to the child node of any node labelled with ?;

· Assign the opposite sign to the first child node and the same sign to the second child node of any node labelled with;

Nodes in signed generation trees are calledpositive(resp.negative)if they are signed+(resp.-).

We give an example of signed generation tree in Figure 1.

Figure 1: Positive generation tree for (p ∨?□q)◇q

For anyτ-formulaφ(p1,...pn),any order-typeεovern,and anyi=1,...,n,anε-critical nodein a signed generation tree ofφis a leaf node +piwhenεi=1 or -piwhenεi=?.Anε-critical branchin a signed generation tree is a branch from anε-critical node.Theε-critical occurrences are intended to be those which the algorithm ALBARQwill solve for.

We use+p?+φ(resp.-p?+φ)to indicate that an occurrence of a propositional variablepinherits the positive(resp.negative)sign from the positive generation tree+φ,and say thatpispositive(resp.negative)inφif+p?+φ(resp.-p?+φ)for all occurrences ofpinφ.

Definition 5.(cf.[5,Definition 5])Nodes in signed generation trees are calledouternodesandinner nodes,according to Table 1.Here □stands for,◇stands for

Table 1: Outer and Inner nodes.

A branch in a signed generation tree isexcellentif it is the concatenation of two pathsP1andP2,one of which might be of length 0,such thatP1is a path from the leaf consisting(apart from variable nodes)of inner nodes only,andP2consists(apart from variable nodes)of outer nodes only.

Definition 6(Sahlqvist inequalities).(cf.[5,Definition 6]) For any order-typeε,the signed generation tree?φ(where?∈{+,-}) of a formulaφ(p1,...pn) isε-Sahlqvistif

· for all 1≤i ≤n,everyε-critical branch with leafpiis excellent;

· for every branch(notice that here it might not beε-critical)with occurrences of+◇Hor-□H,every node from the root to this occurrence of+◇Hor-□Hin the signed generation tree is an outer node.

An inequalityφ ≤ψisε-Sahlqvistif the signed generation trees+φand-ψareε-Sahlqvist.An inequalityφ ≤ψisSahlqvistif it isε-Sahlqvist for someε.A formulaφψis Sahlqvist if the inequalityφ ≤ψis a Sahlqvist inequality.

Example 2.An example of Sahlqvist formula in our language is ◇H□Bp □B◇Hp,which is similar to the Geach formula in ordinary modal logic.Notice that here we have position restrictions on the first occurrence of ◇H.

The classification of outer nodes and inner nodes is based on how different connectives behave in the algorithm.When the input inequality is a Sahlqvist inequality,the algorithm first decompose the outer part of the formula,and then decompose the inner part of the formula,which will be shown in the success proof of the algorithm in Section 7.

The difference between the present setting and ordinary modal logic is that we have additional requirement of the positions of helper modalities,which will be clear from the execution of the algorithm.

4 The Expanded Modal Language,First-Order Correspondence Language and Standard Translation

4.1 The Expanded Modal Language

In the present subsection,we define the expanded modal language,which will be used in the execution of the algorithm:

where i∈Nom arenominalsas in hybrid logic which are interpreted as singleton sets,∈τH,∈τB,S={(i1,j1),...,(ik,jk)}for some pairs(i1,j1),...,(ik,jk).

The reason for introducing the nominals and S-modalities is to compute the minimal valuations for propositional variables and for the H-modalities(which are essentially quantified by second-order quantifiers in the validity definition),therefore we can eliminate them to get a quasi-inequality which is essentially quantified by firstorder quantifiers.

□Sand ◇Sare interpreted on the relationS:={(V(i1),V(j1)),...,(V(ik),V(jk))}.For ■and ◆,they are interpreted as the box and diamond modality on the inverse relation,S-1,according to the superscipt and subscript,respectively.TheS-modalities are interpreted as the computation result of the minimal relations for the helper modalities,which is similar to the minimal valuations of propositional variables in the algorithm ALBARQ.

For the semantics of the expanded modal language,the valuation is defined asV: Prop ∪NomP(W)whereV(i)is defined as a singleton as in hybrid logic,and the additional semantic clauses can be given as follows:

4.2 The first-order correspondence language and the standard translation

In the first-order correspondence language,we have a binary predicate symbolHicorresponding to the binary relationHi,a binary predicate symbolRjcorresponding to the binary relationRj,a set of constant symbolsicorresponding to each nominal i,a set of unary predicate symbolsPcorresponding to each propositional variablep.Notice that we do not have binary predicate symbols for theSrelations.

Definition 7.For the standard translation of the expanded modal language,the basic propositional cases and the Boolean cases as well as the modal cases for boss modalities are defined as usual and hence omitted,the other cases are defined as follows:

It is easy to see that this translation is correct:

Proposition 1(Folklore.).For any Kripke modelM,any w ∈W and any expanded modal formula φ,

For inequalities,quasi-inequalities,the standard translation is given in a global way:

Definition 8.·ST(φ ≤ψ):=?x(STx(φ)STx(ψ));

·ST(φ1≤ψ1&...&φn ≤ψn ?φ ≤ψ):=ST(φ1≤ψ1)∧...∧ST(φn ≤ψn)ST(φ ≤ψ).

Proposition 2(Folklore.).For any Kripke modelM,any inequalityIneq,any quasiinequalityQuasi,

5 The Algorithm ALBARQ

In this section,we define the algorithm ALBARQwhich computes the firstorder correspondents of input Sahlqvist formulas,in the style of[3,4].The algorithm receives an input formulaφψand transforms it into an inequalityφ ≤ψ.Then the algorithm goes in three steps.

1.Preprocessing and first approximation:

In the generation tree of+φand-ψ3The discussion below relies on the definition of signed generation tree in Section 3.In what follows,we identify a formula with its signed generation tree.,

(a) Apply the distribution rules:

(b) Apply the splitting rules: rewriteα ≤β ∧γasα ≤βandα ≤γ;rewriteα ∨β ≤γasα ≤γandβ ≤γ;

(c) Apply the monotone and antitone variable-elimination rules:

forβ(p)positive inpandα(p)negative inp.

We denote by Preprocess(φψ)the finite set{φi ≤ψi}i∈Iof inequalities obtained after the exhaustive application of the previous rules.Then we apply the following first approximation rule to every inequality in Preprocess(φψ):

Here,i0and i1are special fresh nominals.Now we get a set of inequalities{i0≤φi,ψi ≤?i1}i∈I.

2.The reduction stage:

In this stage,for each{i0≤φi,ψi ≤?i1},we apply the following rules to prepare for eliminating all the propositional variables and helper modalities:

(a) Splitting rules(similar to the splitting rules in Stage 1);

(b) Approximation rules:

The nominals introduced by the approximation rules must not occur in the system before applying the rule,and ◇stands for,or ◇S,□stands for,or □S.

(c) Residuation rules:

(d) Ackermann rules:

By the Ackermann rules,we compute the minimal/maximal valuation for propositional variables and minimal valuation for helper modalities and use the Ackermann rules to eliminate all the propositional variables and helper modalities.These three rules are the core of ALBARQ,since their application eliminates propositional variables and helper modalities.In fact,all the preceding steps are aimed at reaching a shape in which the Ackermann rules can be applied.Notice that an important feature of these rules is that they are executed on the whole set of inequalities,and not on a single inequality.

The right-handed Ackermann rule for propositional variables:

where:

i.Eachβiis positive inp,and eachγinegative inp,for 1≤i ≤m;

ii.Eachαiis pure.

The left-handed Ackermann rule for propositional variables:

where:

i.Eachβiis negative inp,and eachγipositive inp,for 1≤i ≤m;

ii.Eachαiis pure.

The right-handed Ackermann rule for helper modalities:

where:

3.Output:If in the previous stage,for some{i0≤φi,ψi ≤?i1},the algorithm gets stuck,i.e.some propositional variables or helper modalities cannot be eliminated by the application of the reduction rules,then the algorithm halts and output “failure”.Otherwise,each initial tuple{i0≤φi,ψi ≤?i1}of inequalities after the first approximation has been reduced to a set of pure inequalities Reduce(φi ≤ψi)without helper modalities,and then the output is a set of quasi-inequalities{&Reduce(φi ≤ψi)?i0≤?i1:φi ≤ψi ∈Preprocess(φψ)}without helper modalities,where &is the big metaconjunction in quasi-inequalities.Then the algorithm use the standard translation to transform the quasi-inequalities into first-order formulas.

6 Soundness of ALBARQ

In the present section,we will prove the soundness of the algorithm ALBARQwith respect to Kripke frames.The basic proof structure is similar to[7].

Theorem 3(Soundness).IfALBARQruns successfully on φψ and outputsFO(φψ),then for any τB-Kripke frameF=(W,R1,...,Rn),

Proof.The proof goes similarly to [4,Theorem 8.1].Letφi ≤ψi,1≤i ≤ndenote the inequalities produced by preprocessingφψafter Stage 1,and{i0≤φi,ψi ≤?i1}denote the inequalities after the first-approximation rule,Reduce(φi ≤ψi) denote the set of pure inequalities after Stage 2,and FO(φ ■ψ) denote the standard translation of the quasi-inequalities into first-order formulas,then we have the following chain of equivalences:

· The equivalence between(1)and(2)follows from Proposition 4;

· the equivalence between(2)and(3)follows from Proposition 5;

· the equivalence between(3)and(4)follows from Propositions 6,7 and 8;

· the equivalence between(4)and(5)follows from Proposition 2.□

In the remainder of this section,we prove the soundness of the rules in Stage 1,2 and 3.

Proposition 4(Soundness of the rules in Stage 1).For the distribution rules,the splitting rules and the monotone and antitone variable-elimination rules,they are sound in both directions inF,i.e.the inequality before the rule is valid inFiff the inequality(-ies)after the rule is(are)valid inF.

Proof.The proof is the same as[7,Proposition 6.2].□

Proposition 5.(2)and(3)are equivalent,i.e.the first-approximation rule is sound inF.

Proof.The proof is the same as[7,Proposition 6.3].□

The next step is to show the soundness of each rule of Stage 2.For each rule,before the application of this rule we have a set of inequalitiesS(which we call thesystem),after applying the rule we get a set of inequalitiesS′,the soundness of Stage 2 is then the equivalence of the following two conditions:

· F ?&S ?i0≤?i1;

· F ?&S′?i0≤?i1;

where&Sdenote the meta-conjunction of inequalities ofS.It suffices to show the following property:

· For anyτB-Kripke frame F=(W,R1,...,Rn),any binary relationsH1,...,Hm,any valuationVon it,if(F,H1,...,Hm,V)?S,then there is a valuationV′and binary relations,...,such thatV′(i0)=V(i0),V′(i1)=V(i1)and(F,,...,,V′)?S′;

· For anyτB-Kripke frame F=(W,R1,...,Rn),any binary relations,...,,any valuationV′on it,if(F,,...,H′m,V′) ?S′,then there is a valuationVand binary relationsH1,...,Hmsuch thatV(i0)=V′(i0),V(i1)=V′(i1)and(F,H1,...,Hm,V)?S.

Proposition 6.The splitting rules,the approximation rules for ◇,□,■,the residuation rules for?,◇,□are sound inF.

Proof.The proof is similar to[7,Proposition 6.4 and 6.11].□

Proposition 7.The Ackermann rules for propositional variables are sound inF.

Proof.The proof is similar to[7,Proposition 6.17].□

Proposition 8.The right-handed Ackermann rule for helper modalities is sound inF.

This rule is the key rule of the algorithm ALBARQsince it eliminates helper modalities.The proof method is similar to the soundness proof of the right-handed Ackermann rule for propositional variables.Without loss of generality,we assume thatk1=k2=m=1.To prove Proposition 8,it suffices to prove the following right-handed Ackermann lemma for helpers:

Lemma 1.Assume that β1is positive inand negative inandγ1is negative inand positive inthen for any τB-Kripke frameF=(W,R1,...,Rn),any binary relations H1,...,Hm,any valuation V on it,thefollowing are equivalent

(1) M:=(F,H1,...,Hm,V)?β1(S/Hi)≤γ1(S/Hi)?

(2)there is a binary relationsuch thatM′:=(F,H1,...,Hi-1,,Hi+1,...,Hm,V)

Since helper modalities with subscriptido not occur inβ1(S/Hi)andγ1(S/Hi),we have M ?β1(S/Hi)≤γ1(S/Hi).□

7 Success

In this section,we prove that ALBARQsucceeds on all Sahlqvist formulas.The proof structure is similar to[7].

Theorem 9.ALBARQsucceeds on all Sahlqvist formulas.

Definition 9(Definiteε-Sahlqvist inequality,similar to Definition 7.2 in[7]).Given any order-typeε,?∈{-,+},the signed generation tree?φof the termφ(p1,...,pn)isdefinite ε-Sahlqvistif there is no+∨,-∧occurring in the outer part on anε-critical branch.An inequalityφ ≤ψis definiteε-Sahlqvist if the trees+φand-ψare both definiteε-Sahlqvist.

Lemma 2.Let {φi ≤ψi}i∈I=Preprocess(φψ)obtained by exhaustive application of the rules in Stage 1 on an input ε-Sahlqvist formula φψ.Then each φi ≤ψi is a definite ε-Sahlqvist inequality.

Proof.Same as[7,Lemma 7.3].□

Definition 10(Innerε-Sahlqvist signed generation tree,similar to Definition 7.4 in[7]).Given an order typeε,?∈{-,+},the signed generation tree?φof the termφ(p1,...,pn)isinner ε-Sahlqvistif its outer partP2on anε-critical branch is always empty,i.e.itsε-critical branches have inner nodes only.

Lemma 3.Given inequalitiesi0≤φi and ψi ≤?i1obtained from Stage 1 where+φi and-ψi are definite ε-Sahlqvist,by applying the rules in Substage 1 of Stage 2 exhaustively,the inequalities that we get are in one of the following forms:

1.pure inequalities which does not have occurrences of propositional variables?

2.inequalities of the formi≤α where+α is inner ε-Sahlqvist?

3.inequalities of the form β ≤?iwhere-β is inner ε-Sahlqvist.

Proof.Similar to [7,Lemma 7.5].For the sake of the proof of the next lemma we repeat the proof here.Indeed,the rules in the Substage 1 of Stage 2 deal with outer nodes in the signed generation trees +φiand -ψiexcept +∨,-∧.For each rule,without loss of generality assume we start with an inequality of the form i≤α,then by applying the approximation rules,splitting rules and the residuation rules for negation in Stage 2,the inequalities we get are either a pure inequality without propositional variables,or an inequality where the left-hand side (resp.right-hand side) is i (resp.?i),and the other side is a formulaα′which is a subformula ofα,such thatα′has one root connective less thanα.Indeed,ifα′is on the left-hand side(resp.right-hand side)then-α′(+α′)is definiteε-Sahlqvist.

By applying the rules in the Substage 1 of Stage 2 exhaustively,we can eliminate all the outer connectives in the critical branches,so for non-pure inequalities,they become of form 2 or form 3.□

The next two lemmas are crucial to the success of the whole algorithm,which also justify the definition of Sahlqvist formulas and inequalities:

Lemma 4.In Lemma 3,all the occurrences of+◇H’s and-□H’s are in the form ofi≤◇Hjand □H?j≤?i,and in form 2 and 3,+α and-β only contain positive occurrences of □H’s and negative occurrences of ◇H’s.

Proof.As we can see from the proof of Lemma 3 and the second item of Definition 6 for Sahlqvist inequalities,during the decomposition of the outer part of the Sahlqvist signed generation trees,all occurrences of+◇H’s and-□H’s are in the outer part of the signed generation tree,hence are treated by the approximation rules.Before the application of the approximation rules,the inequalities are of the form i≤◇Hαor of the form □Hα ≤?i.By applying the approximation rules,they are in the form of i≤◇Hj and □H?j≤?i.For the rest of occurrences of ◇H’s and □H’s,they could only be in form 2 and 3,and ◇H’s occur only negatively and □H’s occur only positively.□

Lemma 5.Assume we have inequalities of the form as described in Lemma 3 and 4,the right-handed Ackermann rule for helper modalities is applicable and therefore all helper modalities can be eliminated.

Proof.It is easy to check that the shape of the system exactly satisfies the requirement of the application of the right-handed Ackermann rule for helper modalities.In addition,since in the result of the rule,some inequalities are deleted and the other inequalities have helper modalities replaced by the same kind of modalities(e.g.diamond by diamond,box by box,white connectives by white connectives,black connectives by black connectives),we still have pure inequalities and inequalities of the form 2 and 3 as described in Lemma 3,but now without helper modalities.□

Lemma 6.Assume we have an inequalityi≤α or β ≤?iwhere+α and-β are inner ε-Sahlqvist,by applying the splitting rules and the residuation rules in Stage 2,we have inequalities of the following form:

1.α ≤p,where ε(p)=1,α is pure?

2.p ≤β,where ε(p)=?,β is pure?

3.α ≤γ,where α is pure and+γ is ε?-uniform?

4.γ ≤β,where β is pure and-γ is ε?-uniform.

Proof.The proof is similar to[7,Lemma 7.6].Notice that for each input inequality,it is of the form i≤αorβ ≤?i,where+αand-βare innerε-Sahlqvist.By applying the splitting rules and the residuation rules,it is easy to check that the inequality will have one side pure,and the other side still innerε-Sahlqvist.By applying these rules exhaustively,one will either havepas the non-pure side (with thispon a critical branch),or have an innerε-Sahlqvist signed generation tree with no critical branch,i.e.,ε?-uniform.□

Lemma 7.Assume we have inequalities of the form as described in Lemma 6,the Ackermann rules for propositional variables are applicable and therefore all propositional variables can be eliminated.

Proof.Immediate observation from the requirements of the Ackermann rules.□

Proof of Theorem 9Assume we have an Sahlqvist formulaas input.By Lemma 2,we get a set of definiteε-Sahlqvist inequalities.Then by Lemma 3,we get inequalities as described in Lemma 3 and 4.By Lemma 5,all helper modalities are eliminated.By Lemma 6,we get the inequalities as described.Finally by Lemma 7,the inequalities are in the right shape to apply the Ackermann rules for propositional variables,and thus we can eliminate all the propositional variables and the algorithm succeeds on the input.□

8 Examples

In this section we show how to run the algorithm ALBARQon some examples that we give in the introduction.By the Goldblatt-Thomason theorem [1,Theorem 3.19],a first-order definable class of Kripke frames is modally definable iff it is closed under taking bounded morphic images,generated subframes,disjoint unions and reflects ultrafilter extensions.Since|W|≤1 andR=W×Ware not closed under taking disjoint unions,they are not definable by ordinary modal formulas,so our results go beyond Sahlqvist theorem in ordinary modal logic.

Example 3.We have input formula ◇Hp□Hp.To make the validity quantification pattern clear,we add quantifiers for the propositional variables,nominals and helper modalities:

First we transform the input formula into inequality:

Stage 1:By first approximation,we have:

Stage 2:By the approximation rule for ◇H,we have:

By the approximation rule for □H,we have:

By the right-handed Ackermann rule for ◇Hand □H,we have(notice that there is no receiving inequalities,so we just eliminate the inequalities i≤◇Hk and □H?k′≤?j):

By the right-handed Ackermann rule forp,we have:

Stage 3:

By standard translation,we have:

By first-order logic,we have:

By first-order logic,we have:

which is:

which is:

Example 4.We have input formula □Bp□Hp.To make the validity quantification pattern clear,we add quantifiers for the propositional variables,nominals and helper modalities:

First we transform the input formula into inequality:

Stage 1:

By first approximation,we have:

Stage 2:

By the approximation rule for □H,we have:

By the right-handed Ackermann rule for □H,we have(notice that there is no receiving inequalities,so we just eliminate the inequality □H?k≤?j):

By the left-handed Ackermann rule forp,we have:

The following are not really obtained by rules in ALBARQ,but they are soundly obtained:

Stage 3:

By standard translation we have:

which is:

9 Conclusion

In the present paper,we develop the correspondence theory for modal logic with helpers and bosses,define the Sahlqvist formulas in this setting,give an algorithm ALBARQwhich transforms input Sahlqvist formulas into their first-order correspondents.

There is one issue remains to be dealt with.In the algorithm ALBARQ,we have the right-handed Ackermann rule for the helper modalities.It seems plausible to also have the left-handed Ackermann rule for the helper modalities,which is more difficult since+□H’s and-◇H’s do not occur in the outer part of the signed generation tree,they cannot be in the form of i ≤◇Hj or □H?j≤?i,which makes it more difficult to compute the corresponding minimal/maximal relation.Therefore we leave it to future work.