• <tr id="yyy80"></tr>
  • <sup id="yyy80"></sup>
  • <tfoot id="yyy80"><noscript id="yyy80"></noscript></tfoot>
  • 99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

    Sahlqvist Correspondence for Instantial Neighbourhood Logic*

    2021-09-29 06:54:24ZhiguangZhao
    邏輯學(xué)研究 2021年3期

    Zhiguang Zhao

    Abstract. In the present paper,we investigate the Sahlqvist-type correspondence theory for instantial neighbourhood logic (INL),which can talk about existential information about the neighbourhoods of a given world and is a mixture between relational semantics and neighbourhood semantics.The increased expressivity and its ability to talk about certain relational patterns of the neighbourhood function makes it possible to ask what kind of properties can this language define on the frame level,whether the“Sahlqvist”fragment of instantial neighbourhood logic could be larger than the rather small KW-fragment.(H.Hansen,2003)We have two proofs of the correspondence results,the first proof is obtained by using standard translation and minimal valuation techniques directly,the second proof follows M.Gehrke et al.(2005)and H.Hansen(2003),where we use bimodal translation method to reduce the correspondence problem in instantial neighbourhood logic to normal bimodal logics in classical Kripke semantics.We give some remarks and future directions at the end of the paper.

    1 Introduction

    Recently,a variant of neighbourhood semantics for modal logics was given,under the name of instantial neighbourhood logic(INL),where existential information about the neighbourhoods of a given world can be added.([5,13,2,3,4,14,15])This semantics is a mixture between relational semantics and neighbourhood semantics,and its expressive power is strictly stronger than neighbourhood semantics.

    In this semantics,the(n+1)-ary modality□(ψ1,...,ψn;φ)is true at a worldwif and only if there exists a neighbourhoodS ∈N(w)such thatφis true everywhere inS,and eachψiis true atwi ∈Sfor somewi.This language has a natural interpretation as a logic of computation in open systems:□(ψ1,...,ψn;φ)can be interpreted as“in the system,the agent has an action to enforce the conditionφwhile simultaneously allowing possible outcomes satisfying each of the conditionsψ1,...,ψn”;this language can describe not only what properties can be guaranteed by an agent’s action,but also exactly what possible outcomes may be achieved from this action(see[3]).

    Instantial neighbourhood logic is first introduced in [4],where the authors defines the notion of bisimulation for instantial neighbourhood logic,gives a complete axiomatic system,and determines its precise SAT complexity;in [13],the canonical rules are defined for instantial neighbourhood logic;in [2],the game-theoretic aspects of instantial neighbourhood logic is studied;in[3],a propositional dynamic logic IPDL is obtained by combining instantial neighbourhood logic with propositional dynamic logic (PDL),its sound and complete axiomatic system is given as well as its finite model property and decidability;in [5],the duality theory for instantial neighbourhood logic is developed via coalgebraic method;in[14],a tableau system for instantial neighbourhood logic is given which can be used for mechanical proof and countermodel search;in[15],a cut-free sequent calculus and a constructive proof of its Lyndon interpolation theorem is given.However,the Sahlqvist-type correspondence theory is still unexplored,which is the theme of this paper;in addition,the increased expressivity makes it possible to ask what kind of properties can this language define on the frame level,whether the“Sahlqvist”fragment of instantial neighbourhood logic could be larger than the rather small KW-fragment in [10] in monotone modal logic.

    In this paper,we define the Sahlqvist formulas in the instantial neighbourhood modal language,and give two different proofs of correspondence results.The first proof is given by standard translation and minimal valuation techniques as in[6,Section 3.6],while the second proof uses bimodal translation method in monotone modal logic and neighbourhood semantics([10,11,12,1])to show that every Sahlqvist formula in the instantial neighbourhood modal language can be translated into a bimodal Sahlqvist formula in Kripke semantics,and hence has a first-order correspondent.The first proof is standard and it reveals how the instantial neighbourhood semantics have the relational pattern,and the second proof is simpler and easier to understand.

    The structure of the paper is as follows:in Section 2,we give a brief sketch on the preliminaries of instantial neighbourhood logic,including its syntax and neighbourhood semantics.In Section 3,we define the standard translation of instantial neighbourhood logic into a two-sorted first-order language.In Section 4,we define Sahlqvist formulas in instantial neighbourhood logic,and prove the Sahlqvist correspondence theorem via standard translation and minimal valuation.In Section 5,we discuss the translation of instantial neighbourhood logic into normal bimodal logic,and prove Sahlqvist correspondence theorem via this bimodal translation.In Section 6,we give some examples.We give some remarks and further directions in Section 7.

    2 Preliminaries on Instantial Neighbourhood Logic

    In this section,we collect some preliminaries on instantial neighbourhood logic,which can be found in[4].

    Syntax.The formulas of instantial neighbourhood logic are defined as follows:

    wherep ∈Prop is a propositional variable,□nis an (n+1)-ary modality for eachn ∈N.→,?can be defined in the standard way.An occurence ofpis said to bepositive(resp.negative)inφifpis under the scope of an even(resp.odd)number of negations.A formulaφis positive(resp.negative)if all occurences of propositional variables inφare positive(resp.negative).

    Semantics.For the semantics of instantial neighbourhood logic,we use neighbourhood frames to interpret the instantial neighbourhood modality,one and the same neighbourhood function for all the(n+1)-ary modalities for alln ∈N.

    Definition 1(Neighbourhood frames and models) Aneighbourhood frameis a pair F(W,N) where?is the set of worlds,N:W →P(P(W)) is a map called aneighbourhood function(notice that there is no restriction on what additional propertiesNshould satisfy,e.g.w ∈Xfor allX ∈N(w),or upward-closedness:X ∈N(w) andX ?YimpliesY ∈N(w)),whereP(W) is the powerset ofW.AvaluationonWis a mapV:Prop→P(W).A triple M(W,N,V)is called aneighbourhood modelor a neighbourhood model based on(W,N)if(W,N)is a neighbourhood frame andVis a valuation on it.

    The semantic clauses for the Boolean part is standard.For the instantial neighbourhood modality□,the satisfaction relation is defined as follows:

    M,w?□n(φ1,...,φn;φ)iff there isS ∈N(w)such that for alls ∈Swe have

    Semantic properties of instantial neighbourhood modalities.It is easy to see the following lemma,which states that the(n+1)-ary instantial neighbourhood modality□nis monotone in every coordinate,and is completely additive(and hence monotone)in the firstncoordinates(even if the neighbourhood function is not upward-closed).This observation is useful in the algebraic correspondence analysis in instantial neighbourhood logic.

    Lemma 1

    Algebraically,if we view the (n+1)-ary modality□nas an (n+1)-ary function:An+1→A,then(a1,...,an;a) is completely additive (i.e.preserve arbitrary joins) in the firstncoordinate,and monotone in the last coordinate.This observation is useful in the algebraic correspondence analysis(see Section 7).

    Getting standard neighbourhood semantics and Kripke semantics from INL.

    As we have already seen in[4],instantial neighbourhood logic can express standard monotone neighbourhood modalities by just takingn0,i.e.,

    Indeed,from the definition ofNwe can define some induced(n+1)-ary relations,and instantial neighbourhood logic can reason about these relational structures.Here we take binary relation and the binary modality□1as an example:

    We can define the following binary relationR1,?based on the neighbourhood functionN:

    Then it is easy to see that

    Therefore,instantial neighbourhood logic can talk about certain relational structures behind the neighbourhood function.Indeed,we will expand on this phenomenon later on(see Section 4.2)when we analyze when instantial neighbourhood logic become“normal”.

    3 Standard Translation of Instantial Neighbourhood Logic

    3.1 Two-sorted first-order language L1 and standard translation

    Given the INL language,we consider the corresponding two sorted first-order languageL1,which is going to be interpreted in a two-sorted domainWw×Ws.For a more detailed treatment,see[10,7].This language is used in the treatment of the standard translation for neighbourhood semantics.The major pattern of this language is that we treat worlds and subsets of worlds as two different sorts,which makes it different from standard first-order language.In addition,allowing quantification over subsets of worlds makes the language have some flavor of second-order logic,but here we treat those subsets of worlds as first-order objects in the second domainWs.

    This language has the following ingredients:

    1.world variablesx,y,z,...,to be interpreted as possible worlds in the world domainWw;

    2.subset variablesX,Y,Z,...,to be interpreted as objects in the subset domainWs{X |X ?Ww};1Notice that here the subset variables are treated as first-order variables in the subset domain Ws,rather than second-order variables in the world domain Ww.Indeed,when talking about standard translation in neighbourhood semantics,it is not possible to avoid talking about subsets of the domain,since the elements in N(w)are subsets of W.Therefore,we follow the tradition in monotone modal logic[10,p.34]to call this two-sorted language first-order.

    3.a binary relation symbolR?,to be interpreted as the reverse membership relationR??Ws×Wwsuch thatR?Xxiffx ∈X;

    4.a binary relation symbolRN,to be interpreted as the neighbourhood relationRN ?Ww×Wssuch thatRNxXiffX ∈N(x);

    5.unary predicate symbolsP1,P2,…,to be interpreted as subsets of the world domainWw.

    We also consider the following second-order languageL2which is obtained by adding second-order quantifiers?P1,?P2,…over the world domainWw.Existential second-order quantifiers?P1,?P2,...are interpreted in the standard way.Notice that here the second-order variablesP1,…are different from the subset variablesX,Y,Z,...,since the former are interpreted as subsets ofWw,and the latter are interpreted as objects inWs.

    Now we define the standard translationSTw(φ)as follows:

    Definition 2(Standard translation) For any INL formulaφand any world symbolx,the standard translationSTx(φ)ofφatxis defined as follows:

    ?STx(p):Px;

    ?STx(⊥):xx;

    ?STx(?):xx;

    ?STx(?φ):?STx(φ);

    ?STx(φ ∧ψ):STx(φ)∧STx(ψ);

    ?STx(φ ∨ψ):STx(φ)∨STx(ψ);

    ?STx(□n(φ1,...,φn;φ))?X(RNxX ∧?y(R?Xy →STy(φ))∧

    ?y1(R?Xy1∧STy1(φ1))∧...∧?yn(R?Xyn ∧STyn(φn))).

    For any neighbourhood frame F(W,N),it is natural to define the following corresponding two-sorted Kripke frame F2(W,P(W),R?,RN),where

    1.R??P(W)×Wsuch that for anyx ∈WandX ∈P(W),R?Xxiffx ∈X;

    2.RN ?W × P(W) such that for anyx ∈WandX ∈P(W),RNxXiffX ∈N(x).

    Given a two-sorted Kripke frame F2(W,P(W),R?,RN),a valuationVis defined as a mapV:Prop→P(W).Notice that here theP(W)in the definition ofVis understood as the powerset of the first domain,rather than the second domain itself.

    For this standard translation,it is easy to see the following correctness result:

    Theorem 3.For any neighbourhood frameF(W,N),any valuation V onF,any w ∈W,any INL formula φ,

    4 Sahlqvist Correspondence Theorem in Instantial Neighbourhood Logic via Standard Translation

    In this section,we will define the Sahlqvist formulas in instantial neighbourhood logic and prove the correspondence theorem via standard translation and minimal valuation method.First we recall the definition of Sahlqvist formulas in normal modal logic.Then we identify the special situations where the instantial neighourhood modalities“behave well”,i.e.have good quantifier patterns in the standard translation.Finally,we define INL-Sahlqvist formulas step by step in the style of[6,Section 3.6],and prove the correspondence theorem.The reason why we still have a proof by standard translation and minimal valuation method is that it helps to recognize the“relational”pattern in this neighbourhood-type semantics.

    4.1 Sahlqvist formulas in normal modal logic

    In this subsection we recall the syntactic definition of Sahlqvist formulas in normal modal logic(see[6,Section 3.6,Definition 3.51]).

    Definition 4(Sahlqvist formulas in normal modal logic) Aboxed atomis a formula of thep,whereare (not necessarily distinct) boxes.In the case wheren0,the boxed atom is justp.

    ASahlqvist antecedent φis a formula built up from⊥,?,boxed atoms,and negative formulas,using∧,∨and existential modal operators◇(unary diamond)and Δ(polyadic diamond).ASahlqvist implicationis an implicationφ →ψin whichψis positive andφis a Sahlqvist antecedent.

    A Sahlqvist formula is a formula that is built up from Sahlqvist implications by applying boxes and conjunctions,and by applying disjunctions only between formulas that do not share any proposition variables.

    As we can see from the definition above,the Sahlqvist antecedents are built up by⊥,?,p,pand negative formulas using∧,∨,◇,Δ.If we consider the standard translations of Sahlqvist antecedents,the inner part is translated into universal quantifiers,and the outer part are translated into existential quantifiers.

    4.2 Special cases where the instantial neighbourhood modalities become“normal”

    As is mentioned in[4,Section 7]and as we can see in the definition of the standard translation,the quantifier pattern of□n(φ1,...,φn;φ)is similar to the case of monotone modal logic([10])which has an??pattern.As a result,even with two layers of INL modalities the complexity goes beyond the Sahlqvist fragment.However,we can still consider some special situations where we can reduce the modality to ann-ary normal diamond or a unary normal box.

    n-ary normal diamond.We first consider the case□n(φ1,...,φn;φ)whereφis apure formulawithout any propositional variables,i.e.,all propositional variables are substituted by⊥or?.In this caseSTx(φ)is a first-order formulaαφ(x)without any unary predicate symbolsP1,P2···.Therefore,in the shape of the standard translation of□n(φ1,...,φn;φ),the universal quantifier?yis not touched during the computation of minimal valuation,since there is no unary predicate symbol there.Indeed,we can consider the following equivalent form ofSTx(□n(φ1,...,φn;φ)):

    NowSTx(□n(φ1,...,φn;φ)) is essentially in a form similar toSTx(◇ψ) in the normal modal logic case;indeed,when we compute the minimal valuation here,RNxX ∧R?Xy1∧...∧R?Xyn ∧?y(R?Xy →αφ(y))can be recognized as an entirety and stay untouched during the process.Indeed,here we can use the formula?X(RNxX ∧R?Xy1∧...∧R?Xyn ∧?y(R?Xy →αφ(y)))to define an(n+1)-ary relation symbolRn,φxy1...yn,and we denote the semantic counterpart of this relation also byRn,φ,then it is easy to see that

    M,w?□n(φ1,...,φn;φ)iff there existv1,...,vnsuch thatRn,φwv1...vnand

    This is exactly how then-ary Δ modality is defined in standard modal logic settings.From now onwards we can denote□n(φ1,...,φn;φ)by Δn,φ(φ1,...,φn)whereφis pure.

    Unary Normal Box.As we can see from above,in□n(φ1,...,φn;φ),we can replace propositional variables inφby⊥and?to obtainn-ary normal diamond modalities.By using the composition with negations,we can get the unary normal box modality,i.e.we can have a modality

    Now we can consider the standard translation of?1,φ(φ1):

    where?y(R?Xy →αφ(y)) does not contain unary predicate symbolsP1,P2,···.Now we can see thatSTx(?1,φ(φ1)) has a form similar toSTx(□ψ) where□is a normal unary box,by takingRNxX ∧R?Xy1∧?y(R?Xy →αφ(y))as an entirety.

    4.3 The definition of INL-Sahlqvist formulas in instantial neighbourhood logic

    Now we can define the INL-Sahlqvist formulas in instantial neighbourhood logic step by step in the style of[6,Section 3.6].The basic proof structure is similar to the basic modal logic setting,namely we first rewrite the standard translation of the modal formula into a specific shape,and then read off the minimal valuation directly from the shape,while here the manipulation of quantifiers is more complicated and needs to take more care.

    4.3.1 Very simple INL-Sahlqvist implications

    Definition 5(Very simple INL-Sahlqvist implications) Avery simple INL-Sahlqvist antecedent φis defined as follows:

    wherep ∈Prop is a propositional variable,θis a pure formula without propositional variables.Avery simple INL-Sahlqvist implicationis an implicationφ →ψwhereψis positive,andφis a very simple INL-Sahlqvist antecedent.

    For very simple INL-Sahlqvist implications,we allown-ary normal diamonds Δn,θin the construction ofφ,while for the(n+1)-ary modality□n,we only allow propositional variables to occur in the(n+1)-th coordinate.

    We can show that very simple INL-Sahlqvist implications have first-order correspondents:

    Theorem 6.For any given very simple INL-Sahlqvist implication φ →ψ,there is a two-sorted first-order local correspondent α(x)such that for any neighbourhood frameF(W,N),any w ∈W,

    ProofThe proof strategy is similar to[6,Theorem 3.42,Theorem 3.49],with some differences in treating□n(φ1,...,φn;p).

    We first start with the two-sorted second-order translation ofφ →ψ,namely?P1...?Pn?x(STx(φ)→STx(ψ)),whereSTx(φ),STx(ψ) are the two-sorted first-order standard translations ofφ,ψ.

    For any very simple INL-Sahlqvist antecedentφ,we consider the shape ofβSTx(φ)defined inductively,

    Now we can denoteRNxX ∧R?Xy1∧...∧R?XynasRnXxy1...ynandR?1,θXfor?y(R?Xy →αθ(y)),and thus get

    By using the equivalences

    Itiseasy tosee thatthetwo-sorted first-orderformulaβSTx(φ)is equivalent to a f ormula ofthe form∧ATProp),where:

    ? ATProp is a conjunction of formulas of the form?y(R?Xy →Py)orPworwworww.

    Therefore,by using the equivalences

    and

    it is immediate that?P1...?Pn?x(STx(φ)→STx(ψ))is equivalent to

    2Notice that the quantifiers ?P1...?Pnare second-order quantifiers over the world domain,andare first-order quantifiers over the subset domain.

    Now we can use similar strategy as in[6,Theorem 3.42,Theorem 3.49].To make it easier for later parts in the paper,we still mention how the minimal valuation and the resulting first-order correspondent formula look like.Without loss of generality we suppose that for any unary predicatePthat occurs in the POS also occurs in AT;otherwise we can substitutePbyλu.uuforPto eliminateP(see[6,Theorem 3.42]).

    Now consider a unary predicate symbolPoccuring in ATProp,andPx1,...,Pxn,?y(R?X1y →Py),…,?y(R?Xmy →Py)are all occurences ofPin ATProp.By takingσ(P)to be

    we get the minimal valuation.The resulting first-order correspondent formula is

    From the proof above,we can see that the part corresponding to Δn,θ(φ1,...,φn)is essentially treated in the same way as ann-ary diamond in the normal modal logic setting,and□n(φ1,...,φn;p)is treated as Δ(◇φ1∧...∧◇φn ∧□p)where Δ is an(n+1)-ary normal diamond,◇is a unary normal diamond and□is a unary normal box,therefore we can guarantee the compositional structure of quantifiers in the antecedent to be??as a whole.

    4.3.2 Simple INL-Sahlqvist implications

    Similar to simple Sahlqvist implications in basic modal logic,here we can define simple INL-Sahlqvist implications:

    Definition 7(Simple INL-Sahlqvist implications) Apseudo-boxed atom ζis defined as follows:

    whereθis a pure formula without propositional variables.Based on this,asimple INL-Sahlqvist antecedent φis defined as follows:

    whereθis a pure formula without propositional variables andζis a pseudo-boxed atom.Asimple INL-Sahlqvist implicationis an implicationφ →ψwhereψis positive,andφis a simple INL-Sahlqvist antecedent.

    Theorem 8.For any given simple INL-Sahlqvist implication φ →ψ,there is a twosorted first-order local correspondent α(x)such that for any neighbourhood frameF(W,N),any w ∈W,

    ProofWe use similar proof strategy as [6,Theorem 3.49].The part that we need to take care of is the way to compute the minimal valuation.Now without loss of generality (by renaming quantified variables) we have the following shape ofβSTx(ζ)defined inductively for any pseudo-boxed atomζ:

    The shape ofβSTx(φ) is defined inductively for any simple Sahlqvist antecedentφ:

    Now we use the abbreviationRnXxy1...ynforRNxX∧R?Xy1∧...∧R?XynandR?1,θXfor?y(R?Xy →αθ(y)) (note that the only possible free variable inαθ(y) isy),then by the equivalence (?Xα →β)??X(α →β),the shape ofβSTx(ζ)can be given as follows:

    The shape ofβSTx(φ)can be given as follows:

    Now we denote?X(R1Xxy1∧R?1,θX)asR?2,θxy1,and we get the shape of pseudo-boxed atomβSTx(ζ)as follows:

    Now using the following equivalences:

    ? (φ →?z(ψ(z)→γ))??z(φ ∧ψ(z)→γ)(wherezdoes not occur inφ);

    ? (φ →(ψ →γ))?(φ ∧ψ →γ);

    ? (φ →(ψ ∧γ))?((φ →ψ)∧(φ →γ));

    ??z(ψ(z)∧γ(z))?(?zψ(z)∧?zγ(z));

    4.3.3 INL-Sahlqvist implications

    In the present section,we add negated formulas and disjunctions in the antecedent part,which is analogous to the first half of[6,Definition 3.51].

    Definition 9(INL-Sahlqvist implications) AnINL-Sahlqvist antecedent φis defined as follows:

    whereθis a pure formula without propositional variables,ζis a pseudo-boxed atom andγis a negative formula.AnINL-Sahlqvist implicationis an implicationφ →ψwhereψis positive,andφis an INL-Sahlqvist antecedent.

    Theorem 10.For any given INL-Sahlqvist implication φ →ψ,there is a two-sorted first-order local correspondent α(x)such that for any neighbourhood frameF(W,N),any w ∈W,

    ProofWe use similar proof strategy as[6,Theorem 3.54].The part that we need to take care of is the way to compute the minimal valuation.Now for each INL-Sahlqvist antecedentφ,we consider the shape ofβSTx(φ):

    whereθis a pure formula without propositional variables,ζis a pseudo-boxed atom andγis a negative formula.

    We use the abbreviationRnXxy1,...ynforRNxX ∧R?Xy1∧...∧R?XynandR?1,θXfor?y(R?Xy →αθ(y)),we can rewrite the shape ofβSTx(φ)as follows:

    whereθis a pure formula without propositional variables,ζis a pseudo-boxed atom andγis a negative formula.

    ? NEGiis a conjunction of formulas of the formSTy(γ)and?y(R?Xy →STy(γ))whereγis a negative formula.

    Now let us consider the standard translation of INL-Sahlqvist implicationφ →ψwhereφis an INL-Sahlqvist antecedent andψis a positive formula.ForβSTEx(φ →ψ),we have the following equivalence:

    Now it is easy to see that?NEGi ∨STx(ψ) is equivalent to a first-order formula which is positive in all unary predicates.We can now use essentially the same proof strategy as Theorem 8. □

    As we can see from the proofs above,the key point is the quantifier pattern of the two-sorted standard translation of the modalities,i.e.the outer part of the structure of an INL-Sahlqvist antecedent are translated into existential quantifiers,and the inner part is translated into universal quantifiers.

    4.3.4 INL-Sahlqvist formulas

    In the present section,we build Sahlqvist formulas from Sahlqvist implications by applying?1,θ(·)(whereθis pure),∧and∨,which is analogous to the second half of[6,Definition 3.51].

    Definition 11(INL-Sahlqvist formulas) AnINL-Sahlqvist formula φis defined as follows:

    whereφ0is an INL-Sahlqvist implication,θis a pure formula without propositional variables,is a disjunction such that the twoφs share no propositional variable.

    Theorem 12.For any given INL-Sahlqvist formula φ,there is a two-sorted first-order local correspondent α(x)such that for any neighbourhood frameF(W,N),any w ∈W,

    ProofSimilar to[6,Lemma 3.53]. □

    5 Bimodal Translation of Instantial Neighbourhood Logic

    In the present section we give the second proof of Sahlqvist correspondence theorem,by using a bimodal translation into a normal bimodal language.The methodology is similar to[10,7],but with slight differences.

    5.1 Normal bimodal language and two-sorted Kripke frame

    In this subsection,we introduce the normal bimodal language and two-sorted Kripke frame.For a more detailed treatment,see[10,7].

    As we can see in Section 3,for any given neighbourhood frame F(W,N),there is an associated two-sorted Kripke frame F2(W,P(W),R?,RN),where

    1.R??P(W)×Wsuch that for anyx ∈WandX ∈P(W),R?Xxiffx ∈X;

    2.RN ?W × P(W) such that for anyx ∈WandX ∈P(W),RNxXiffX ∈N(x).

    In this kind of semantic structures,we can define the following two-sorted normal bimodal language:

    whereφis a formula of theworld typeand will be interpreted in the first domain,andθis a formula of thesubset typeand will be interpreted in the second domain.We can also define□?and□Nin the standard way.

    Given a two-sorted Kripke frame F2(W,P(W),R?,RN),a valuationVis defined as a mapV:Prop→P(W),where propositional variables are interpreted as subsets of the first domain.The satisfaction relation ?is defined as follows,for anyw ∈Wand anyXinP(W)(here we omit the Boolean connectives):

    ? F2,V,w?piffw ∈V(p);

    ? F2,V,w?◇Nθiff there is anX ∈P(W)such thatRNwXand F2,V,X?θ;

    ? F2,V,X?◇?φiff there is aw ∈Wsuch thatR?Xwand F2,V,w?φ.

    5.2 Bimodal translation

    Now we are ready to define the translationτfrom the INL language to the twosorted normal bimodal language:

    Definition 13(Bimodal translation) Given any INL formulaφ,the bimodal translationτ(φ)is defined as follows:

    ?τ(p)p;

    ?τ(⊥)⊥;

    ?τ(?)?;

    ?τ(?φ)?τ(φ);

    ?τ(φ1∧φ2)τ(φ1)∧τ(φ2);

    ?τ(φ1∨φ2)τ(φ1)∨τ(φ2);

    ?τ(φ1→φ2)τ(φ1)→τ(φ2);

    ?τ(□n(φ1,...,φn;φ))◇N(◇?τ(φ1)∧...∧◇?τ(φn)∧□?τ(φ)).

    It is easy to see the following correctness result:

    Theorem 14.For any neighbourhood frameF(W,N),any valuation V onF,any w ∈W,any INL formula φ,

    5.3 Sahlqvist correspondence theorem via bimodal translation

    To discuss the Sahlqvist correspondence theorem via bimodal translation,we first discuss how the Sahlqvist fragment in normal bimodal logic looks like.

    First of all,we have the following observation that for?1,θ(ζ)whereθis pure,its bimodal translation is□N(□?τ(ζ)∨?□?τ(θ)),i.e.□N(□?τ(θ)→□?τ(ζ)).This formula is not a box itself applied toτ(ζ),but its standard translation into first-order logic is

    which means that we can treatRNxX ∧R?Xy1∧?y(R?Xy →αθ(y))as an entirety and therefore we can treat□N(□?τ(θ)→□?τ(ζ))like a boxed formula.From here onwards we will also call formulas of the shape□N(□?τ(θ)→□?τ(ζ)) boxed atoms ifτ(ζ)is a boxed atom.

    Now,similar to the normal modal logic case,we can define the bimodal Sahlqvist antecedents in the normal bimodal logic built up by boxed atoms and negative formulas in the inner part generated by∧,∨,◇?,◇N,where the formulas are of the right type,and therefore bimodal Sahlqvist implications are defined in the standard way.A bimodal Sahlqvist formula is built up from bimodal Sahlqvist implications by applying boxes,□N(□?τ(θ)→□?(·)),∧and∨whereθis pure and∨is only applied to formulas which share no propositional variable.

    Theorem 15.For any bimodal Sahlqvist formula φ,there is a two-sorted first-order local correspondent α(x)such that for any neighbourhood frameF(W,N),any w ∈W,

    ProofBy adaptation of the proofs of Theorem 3.42,3.49,3.54 and Lemma 3.53 in[6]to the bimodal setting. □

    Now we can prove Sahlqvist correspondence theorem by using bimodal translation:

    Theorem 16.For any INL-Sahlqvist implication φ →ψ,τ(φ →ψ)is a Sahlqvist implication in the normal bimodal language.

    ProofAs we know,the shape of an INL-Sahlqvist antecedent is given as follows:

    whereθis a pure INL formula without propositional variables,ζis a pseudo-boxed atom,andγis a negative formula.Therefore,the bimodal translations ofτ(ζ) andτ(φ)have the following shape:

    Now we analyze the shape above.For the bimodal translation of a pseudo-boxed atomζin the INL language,?◇N(◇??τ(ζ)∧□?τ(θ))is equivalent to□N(□?τ(ζ)∨?□?τ(θ)).sinceθis a pure formula without propositional variables,τ(ζ) can be treated as a conjunction of boxed atoms in the bimodal language.

    Now we examineτ(φ).It is built up byτ(ζ) (a conjunction of boxed atoms)andτ(γ) (a negative formula),generated by∧,∨and the three special shapes ofτ(□n(φ1,...,φn;φ))whereφare pure formulas without propositional variables(theθcase),pseudo-boxed atoms(theζcase)or negative formulas(theγcase).It is easy to see thatτ(φ) is built up by pure formulas3Indeed,pure formulas are both negative and positive formulas in every propositional variable p,since their values are constants and p does not occur in them.,boxed atoms and negative formulas in the bimodal language,generated by◇?,◇N,∧,∨,thus of the shape of Sahlqvist antecedent in the bimodal language.Therefore,τ(φ →ψ)is a Sahlqvist implication in the normal bimodal language. □

    Theorem 17.For any INL-Sahlqvist formula φ,its bimodal translation τ(φ)is a bimodal Sahlqvist formula.

    ProofWe prove by induction.For the basic case and the∧and∨case,it is easy.For the?1,θ(ζ)case whereθis pure andζis an INL-Sahlqvist formula,by induction hypothesis,τ(ζ)is a bimodal Sahlqvist formula.By our definition,□N(□?τ(θ)→□?τ(ζ))is also a bimodal Sahlqvist formula. □

    Theorem 18.For any INL-Sahlqvist formula φ,there is a two-sorted first-order local correspondent α(x)such that for any neighbourhood frameF(W,N),any w ∈W,

    ProofBy Theorem 15 and Theorem 17. □

    6 Examples

    In this section,we give some examples of INL-Sahlqvist implications.Example 19Consider the formula□1(p;?)→?□1(?p;?),its standard translation is

    the minimal valuation forPisλz.zy1,therefore the local first-order correspondent of□1(p;?)→?□1(?p;?)is

    Example 20Consider the formula□1(□1(p;?);?)→□1(p;?),its standard translation is

    the minimal valuation isλz.zy2,therefore the local first-order correspondent of□1(□1(p;?);?)→□1(p;?)is

    As we can see from the examples,instantial neighbourhood logic can talk about the“relational part”of the neighbourhood function,this is one of the reason to investigate the correspondence theory of instantial neighbourhood logic.

    7 Discussions and Further Directions

    In this paper,we give two different proofs of the Sahlqvist correspondence theorem for instantial neighbourhood logic,the first one by standard translation and minimal valuation,and the second one by reduction using the bimodal translation into a normal bimodal language.We give some remarks and further directions here.

    Algebraic correspondence method using the algorithm ALBA.In[8],Sahlqvist and inductive formulas(an extension of Sahlqvist formulas,see[9]for further details)are defined based on duality-theoretic and order-algebraic insights.The Ackermann lemma based algorithm ALBA is given,which effectively computes first-order correspondents of input formulas/inequalities,and succeed on the Sahlqvist and inductive formulas/inequalities.In this approach,Sahlqvist and inductive formulas are defined in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives.Indeed,in the dual complex algebra A of Kripke frame,the good properties of the connectives are the following:

    ? Unary◇is interpreted as a map◇A:A→A,which preserves arbitrary joins,i.e.◇A(∨a)∨◇Aaand◇A⊥⊥.Similarly,n-ary diamonds are interpreted as maps which preserve arbitrary joins in every coordinate.

    ? Unary□is interpreted as a map□A:A→A,which preserves arbitrary meets,i.e.□A(∧a)∧□Aaand□A??.Preserving arbitrary meets guarantees the map□A:A→A to have a left adjoint ?A:A→A such that ?Aa ≤biffa ≤□Ab.

    As we have seen from Section 2,the algebraic interpretation of□n(φ1,...,φn;φ)preserves arbitrary joins in the firstncoordinates,and is monotone in the last coordinate.Therefore,we can adapt the ALBA method to the instantial neighbourhood logic case.In addition to this,we can also define INL-inductive formulas based on the algebraic properties of the instantial neighbourhood connectives,to extend INLSahlqvist formulas to INL-inductive formulas as well as to the language of instantial neighbourhood logic with fixpoint operators.

    Completeness and canonicity.Other issues that we do not study in the present paper include completeness of logics axiomatized by INL-Sahlqvist formulas and canonicity.For the proof of completeness,we need to establish the validity of INLSahlqvist formulas on their corresponding canonical frames,where canonicity and persistence might play a role(see[6,Chapter 5]).

    狠狠精品人妻久久久久久综合| 大又大粗又爽又黄少妇毛片口| 日韩视频在线欧美| 亚洲久久久国产精品| 久久久久久久久久久免费av| 精品熟女少妇av免费看| 天天躁夜夜躁狠狠久久av| 一区二区三区精品91| 日本黄色片子视频| 亚洲国产精品国产精品| 少妇的逼水好多| 精品人妻熟女毛片av久久网站| 一个人免费看片子| 少妇高潮的动态图| 亚洲美女黄色视频免费看| 久久免费观看电影| 欧美少妇被猛烈插入视频| 国产免费视频播放在线视频| a级毛色黄片| 成人综合一区亚洲| 亚洲欧美日韩东京热| 永久网站在线| 一区二区av电影网| 少妇裸体淫交视频免费看高清| av女优亚洲男人天堂| 国产无遮挡羞羞视频在线观看| 99热这里只有是精品50| 日日摸夜夜添夜夜添av毛片| 午夜福利网站1000一区二区三区| 五月伊人婷婷丁香| 亚洲精品国产成人久久av| 中文字幕精品免费在线观看视频 | 成人免费观看视频高清| 久久99精品国语久久久| 亚洲av福利一区| 黄色怎么调成土黄色| 国内精品宾馆在线| 久久精品国产a三级三级三级| 国产精品国产av在线观看| 国产精品一区二区三区四区免费观看| 免费人妻精品一区二区三区视频| 精品午夜福利在线看| 国产视频首页在线观看| 一区二区三区乱码不卡18| 国产中年淑女户外野战色| 精品亚洲乱码少妇综合久久| 欧美+日韩+精品| 成年美女黄网站色视频大全免费 | 五月伊人婷婷丁香| 亚洲av欧美aⅴ国产| 日韩,欧美,国产一区二区三区| 99热这里只有是精品50| 免费黄网站久久成人精品| 精品一区二区三区视频在线| 精品卡一卡二卡四卡免费| 青春草亚洲视频在线观看| 18禁裸乳无遮挡动漫免费视频| 国产精品无大码| 亚洲成色77777| 青春草视频在线免费观看| 老司机影院成人| 亚洲精品乱久久久久久| av福利片在线| 蜜臀久久99精品久久宅男| 深夜a级毛片| 亚洲内射少妇av| 国精品久久久久久国模美| 麻豆乱淫一区二区| 蜜桃在线观看..| 国产熟女欧美一区二区| 九九久久精品国产亚洲av麻豆| 国产视频首页在线观看| 黄色视频在线播放观看不卡| 亚洲第一av免费看| 欧美最新免费一区二区三区| 精品久久久久久久久亚洲| 色哟哟·www| av国产久精品久网站免费入址| 青春草国产在线视频| 国产色婷婷99| 国产有黄有色有爽视频| 极品人妻少妇av视频| 人人澡人人妻人| 另类精品久久| 亚洲三级黄色毛片| 国产免费一级a男人的天堂| 在线观看三级黄色| 我要看黄色一级片免费的| 超碰97精品在线观看| 国产在线男女| 边亲边吃奶的免费视频| 中国国产av一级| 久久久久网色| 十八禁高潮呻吟视频 | 免费av中文字幕在线| 精品久久久精品久久久| 久久精品国产鲁丝片午夜精品| 97超碰精品成人国产| 2022亚洲国产成人精品| 免费久久久久久久精品成人欧美视频 | 少妇人妻 视频| 我要看日韩黄色一级片| 99热6这里只有精品| videos熟女内射| 黄色配什么色好看| 一区二区三区精品91| 色哟哟·www| 国产精品熟女久久久久浪| 久久精品国产亚洲av天美| 久久毛片免费看一区二区三区| 伦理电影大哥的女人| 一区二区三区精品91| 少妇的逼好多水| 午夜老司机福利剧场| 晚上一个人看的免费电影| a级片在线免费高清观看视频| 天天操日日干夜夜撸| 97超视频在线观看视频| 免费在线观看成人毛片| 免费看不卡的av| 肉色欧美久久久久久久蜜桃| 成人毛片60女人毛片免费| 人人妻人人澡人人看| 高清av免费在线| 久久人人爽av亚洲精品天堂| 丝袜在线中文字幕| 精品少妇黑人巨大在线播放| 日韩制服骚丝袜av| 久久久精品94久久精品| 秋霞在线观看毛片| 亚洲美女搞黄在线观看| 黄色一级大片看看| 99热国产这里只有精品6| 国产免费一区二区三区四区乱码| 新久久久久国产一级毛片| 成人毛片60女人毛片免费| 噜噜噜噜噜久久久久久91| 亚洲成人一二三区av| 少妇高潮的动态图| 黑人高潮一二区| 国产老妇伦熟女老妇高清| 人人妻人人看人人澡| 日本av免费视频播放| 91久久精品国产一区二区成人| 十八禁高潮呻吟视频 | 人妻少妇偷人精品九色| 丝袜喷水一区| 久久国产乱子免费精品| 91精品国产国语对白视频| 香蕉精品网在线| 久久久久国产网址| 亚洲伊人久久精品综合| 国产亚洲精品久久久com| 精品亚洲成国产av| av网站免费在线观看视频| 九色成人免费人妻av| 男人爽女人下面视频在线观看| av在线app专区| 美女脱内裤让男人舔精品视频| 亚洲欧美成人综合另类久久久| 美女福利国产在线| 老熟女久久久| 成年美女黄网站色视频大全免费 | 草草在线视频免费看| 亚洲欧洲精品一区二区精品久久久 | 亚洲欧洲国产日韩| 91aial.com中文字幕在线观看| 26uuu在线亚洲综合色| 精品久久久久久电影网| 啦啦啦在线观看免费高清www| 日本vs欧美在线观看视频 | 成人二区视频| 香蕉精品网在线| 亚洲国产毛片av蜜桃av| 久热这里只有精品99| 国产伦在线观看视频一区| 你懂的网址亚洲精品在线观看| 亚洲国产精品一区二区三区在线| 成人国产麻豆网| 大片免费播放器 马上看| 97在线人人人人妻| 永久网站在线| 丰满乱子伦码专区| 另类精品久久| 在线精品无人区一区二区三| 亚洲精品自拍成人| 十分钟在线观看高清视频www | 中文字幕人妻熟人妻熟丝袜美| 成年人免费黄色播放视频 | kizo精华| 亚洲激情五月婷婷啪啪| 国产高清国产精品国产三级| 如何舔出高潮| 九九在线视频观看精品| 久久久精品94久久精品| 国产精品伦人一区二区| 免费大片黄手机在线观看| 哪个播放器可以免费观看大片| 校园人妻丝袜中文字幕| 久久久国产欧美日韩av| 亚洲精品,欧美精品| 少妇裸体淫交视频免费看高清| 欧美成人精品欧美一级黄| 久久久久国产网址| 亚洲自偷自拍三级| 亚洲综合精品二区| 久久久久久久久久成人| 搡女人真爽免费视频火全软件| 国产精品久久久久久av不卡| 国产成人精品一,二区| 久久免费观看电影| 国产精品久久久久久av不卡| 国产乱人偷精品视频| 亚洲国产精品一区二区三区在线| 久久99热这里只频精品6学生| 中文字幕制服av| 久久久久久久久久人人人人人人| 人人妻人人添人人爽欧美一区卜| 熟妇人妻不卡中文字幕| 免费观看在线日韩| 国产男女内射视频| 麻豆乱淫一区二区| av福利片在线观看| 亚洲自偷自拍三级| 免费看av在线观看网站| 亚洲av欧美aⅴ国产| 青春草亚洲视频在线观看| 在线亚洲精品国产二区图片欧美 | 五月开心婷婷网| 日韩三级伦理在线观看| a级毛色黄片| 黄色一级大片看看| 十分钟在线观看高清视频www | 女性生殖器流出的白浆| 国产精品秋霞免费鲁丝片| 精品国产国语对白av| 国产成人精品一,二区| 欧美精品人与动牲交sv欧美| 亚洲欧洲精品一区二区精品久久久 | 国产精品无大码| 99九九线精品视频在线观看视频| 亚洲精品国产av蜜桃| 欧美日韩综合久久久久久| 女人精品久久久久毛片| 午夜激情福利司机影院| 亚洲国产精品一区二区三区在线| 9色porny在线观看| 91成人精品电影| 欧美日韩在线观看h| 卡戴珊不雅视频在线播放| 久久久久久久久久久丰满| 亚洲欧美精品自产自拍| 日韩成人av中文字幕在线观看| 夜夜爽夜夜爽视频| 欧美日韩视频精品一区| 欧美 亚洲 国产 日韩一| 日本欧美视频一区| 观看av在线不卡| 人妻人人澡人人爽人人| 中文资源天堂在线| 久久久久久久久大av| 99热全是精品| 人人妻人人澡人人爽人人夜夜| 97超视频在线观看视频| 成人二区视频| 国产有黄有色有爽视频| 亚洲成人手机| 国产精品国产av在线观看| 美女主播在线视频| 毛片一级片免费看久久久久| 蜜桃在线观看..| 国内揄拍国产精品人妻在线| 亚洲欧美一区二区三区国产| 国产伦理片在线播放av一区| 人人妻人人澡人人看| 五月天丁香电影| 99re6热这里在线精品视频| 99热网站在线观看| 蜜桃久久精品国产亚洲av| 寂寞人妻少妇视频99o| 六月丁香七月| 日韩成人伦理影院| 高清av免费在线| 欧美成人精品欧美一级黄| 精品熟女少妇av免费看| 视频中文字幕在线观看| 日韩在线高清观看一区二区三区| 日韩不卡一区二区三区视频在线| 国产成人aa在线观看| 免费看不卡的av| 国产成人免费观看mmmm| 91在线精品国自产拍蜜月| 黄色视频在线播放观看不卡| 99久国产av精品国产电影| 三级国产精品片| 亚洲丝袜综合中文字幕| 色网站视频免费| www.色视频.com| 国产成人免费无遮挡视频| 国产深夜福利视频在线观看| 国产成人精品福利久久| 久久久亚洲精品成人影院| 九色成人免费人妻av| 亚洲四区av| av在线app专区| 久久女婷五月综合色啪小说| 久久国产乱子免费精品| 亚洲av电影在线观看一区二区三区| 水蜜桃什么品种好| 久久这里有精品视频免费| 夫妻性生交免费视频一级片| 五月玫瑰六月丁香| 在线观看www视频免费| 老司机影院毛片| 狂野欧美激情性xxxx在线观看| 99热这里只有精品一区| 午夜福利网站1000一区二区三区| 日日摸夜夜添夜夜爱| 欧美一级a爱片免费观看看| 国产精品成人在线| 午夜福利影视在线免费观看| 日日摸夜夜添夜夜添av毛片| 久久久久久伊人网av| 下体分泌物呈黄色| 亚洲久久久国产精品| 18禁裸乳无遮挡动漫免费视频| 国产乱来视频区| 欧美日韩综合久久久久久| 91久久精品国产一区二区三区| 熟妇人妻不卡中文字幕| 男女边摸边吃奶| 免费观看性生交大片5| 国产在线一区二区三区精| 在线观看av片永久免费下载| 毛片一级片免费看久久久久| 黄色日韩在线| 国产精品女同一区二区软件| 国产伦理片在线播放av一区| av又黄又爽大尺度在线免费看| 久久久久国产精品人妻一区二区| 国产av精品麻豆| 欧美性感艳星| 纯流量卡能插随身wifi吗| 欧美日韩在线观看h| 色婷婷久久久亚洲欧美| 色94色欧美一区二区| 男女边吃奶边做爰视频| 国产在线男女| 免费不卡的大黄色大毛片视频在线观看| 亚洲av综合色区一区| 午夜福利网站1000一区二区三区| 国产高清有码在线观看视频| 91精品一卡2卡3卡4卡| 最近最新中文字幕免费大全7| a级毛色黄片| 精品熟女少妇av免费看| 亚洲欧美日韩卡通动漫| 精品酒店卫生间| 丰满乱子伦码专区| tube8黄色片| 国产精品偷伦视频观看了| 久久国内精品自在自线图片| 黄色配什么色好看| 丰满乱子伦码专区| 尾随美女入室| 各种免费的搞黄视频| 国产一级毛片在线| 久久国产乱子免费精品| 狂野欧美激情性bbbbbb| 国产女主播在线喷水免费视频网站| 好男人视频免费观看在线| 久久久久久久亚洲中文字幕| 少妇人妻久久综合中文| 国产一级毛片在线| 亚洲av成人精品一二三区| 一级黄片播放器| 国产av码专区亚洲av| 午夜福利影视在线免费观看| 亚洲国产日韩一区二区| 一级二级三级毛片免费看| 少妇精品久久久久久久| 五月玫瑰六月丁香| 中文在线观看免费www的网站| 欧美日韩在线观看h| 国产老妇伦熟女老妇高清| 成人毛片60女人毛片免费| 好男人视频免费观看在线| 亚洲在久久综合| 夫妻午夜视频| 极品少妇高潮喷水抽搐| 69精品国产乱码久久久| 天堂俺去俺来也www色官网| 纵有疾风起免费观看全集完整版| 一级毛片我不卡| 日韩,欧美,国产一区二区三区| 精品一区在线观看国产| 亚洲自偷自拍三级| 午夜免费观看性视频| 国产亚洲午夜精品一区二区久久| 久久精品国产a三级三级三级| 亚洲熟女精品中文字幕| 久久精品夜色国产| 大话2 男鬼变身卡| 能在线免费看毛片的网站| 成年人免费黄色播放视频 | 一级二级三级毛片免费看| 欧美一级a爱片免费观看看| 69精品国产乱码久久久| 精品人妻熟女av久视频| 秋霞伦理黄片| 国产亚洲91精品色在线| 国产色爽女视频免费观看| 日韩伦理黄色片| 亚洲不卡免费看| av免费观看日本| 最近2019中文字幕mv第一页| 两个人的视频大全免费| 最近手机中文字幕大全| 久久女婷五月综合色啪小说| 在线观看免费高清a一片| 日日摸夜夜添夜夜添av毛片| 91久久精品国产一区二区三区| 亚洲三级黄色毛片| 中文精品一卡2卡3卡4更新| 国产精品蜜桃在线观看| 久久久久久伊人网av| 高清毛片免费看| 3wmmmm亚洲av在线观看| 妹子高潮喷水视频| 精品久久久久久久久亚洲| 啦啦啦啦在线视频资源| 蜜臀久久99精品久久宅男| 国产淫片久久久久久久久| 久久免费观看电影| 亚洲人与动物交配视频| 欧美精品人与动牲交sv欧美| 五月天丁香电影| 夜夜看夜夜爽夜夜摸| 天美传媒精品一区二区| 欧美最新免费一区二区三区| 国产精品久久久久久av不卡| h日本视频在线播放| 日韩免费高清中文字幕av| 三级经典国产精品| 日日摸夜夜添夜夜爱| 亚洲经典国产精华液单| 久久韩国三级中文字幕| 亚洲国产精品一区二区三区在线| 日韩一区二区三区影片| 亚洲欧美成人综合另类久久久| 99久久人妻综合| 老熟女久久久| 精品人妻熟女毛片av久久网站| 91aial.com中文字幕在线观看| 亚洲情色 制服丝袜| 另类精品久久| 久久亚洲国产成人精品v| 最近中文字幕2019免费版| 在线观看av片永久免费下载| av又黄又爽大尺度在线免费看| 国产精品久久久久久精品电影小说| 国产爽快片一区二区三区| 成年美女黄网站色视频大全免费 | av专区在线播放| 久久国产精品男人的天堂亚洲 | 色视频在线一区二区三区| 亚洲av不卡在线观看| 欧美+日韩+精品| 亚洲精品久久久久久婷婷小说| 又大又黄又爽视频免费| 99久久中文字幕三级久久日本| 美女cb高潮喷水在线观看| 中文字幕人妻熟人妻熟丝袜美| 欧美最新免费一区二区三区| av免费在线看不卡| 美女cb高潮喷水在线观看| a级片在线免费高清观看视频| 天天躁夜夜躁狠狠久久av| 激情五月婷婷亚洲| av女优亚洲男人天堂| 欧美变态另类bdsm刘玥| 免费高清在线观看视频在线观看| 有码 亚洲区| 韩国高清视频一区二区三区| 少妇高潮的动态图| 99久久中文字幕三级久久日本| 女性被躁到高潮视频| 伊人久久精品亚洲午夜| 啦啦啦视频在线资源免费观看| 国产成人精品福利久久| 啦啦啦视频在线资源免费观看| 大香蕉久久网| 亚洲欧美日韩卡通动漫| 久久久久久久久久久免费av| 精品卡一卡二卡四卡免费| 国产在线免费精品| 精品一区二区三区视频在线| 精品国产一区二区三区久久久樱花| 水蜜桃什么品种好| 日韩av在线免费看完整版不卡| 精品人妻熟女av久视频| 日韩伦理黄色片| 高清毛片免费看| 亚洲国产精品专区欧美| 少妇的逼水好多| 亚洲av电影在线观看一区二区三区| 国产伦理片在线播放av一区| 偷拍熟女少妇极品色| 麻豆成人av视频| 人人妻人人添人人爽欧美一区卜| 日本免费在线观看一区| 99久国产av精品国产电影| 午夜福利网站1000一区二区三区| 一级av片app| 五月伊人婷婷丁香| 欧美成人午夜免费资源| 人人妻人人澡人人看| 男女无遮挡免费网站观看| a级毛片免费高清观看在线播放| 国产av一区二区精品久久| 久久影院123| 国产精品人妻久久久久久| av天堂久久9| 大陆偷拍与自拍| 大香蕉97超碰在线| 欧美日韩在线观看h| 久久久久久久大尺度免费视频| 亚洲欧洲国产日韩| a级一级毛片免费在线观看| 成人18禁高潮啪啪吃奶动态图 | 狂野欧美白嫩少妇大欣赏| 久久精品久久久久久噜噜老黄| 亚洲人成网站在线播| 极品人妻少妇av视频| 少妇的逼水好多| 综合色丁香网| 国产黄片美女视频| 久久国内精品自在自线图片| 91久久精品电影网| 寂寞人妻少妇视频99o| 国产精品一区www在线观看| 亚洲精品日韩在线中文字幕| 99久久精品国产国产毛片| av网站免费在线观看视频| 午夜精品国产一区二区电影| 桃花免费在线播放| 日日啪夜夜爽| 免费久久久久久久精品成人欧美视频 | 黄色欧美视频在线观看| 精品少妇久久久久久888优播| 人人妻人人澡人人爽人人夜夜| 夜夜骑夜夜射夜夜干| 中文天堂在线官网| 妹子高潮喷水视频| 一区二区av电影网| 蜜桃在线观看..| 亚洲欧美日韩卡通动漫| 黄色日韩在线| 久久韩国三级中文字幕| 欧美日韩一区二区视频在线观看视频在线| 一区二区三区乱码不卡18| 亚洲精品视频女| 91精品国产九色| 日韩大片免费观看网站| h视频一区二区三区| 美女xxoo啪啪120秒动态图| 欧美激情极品国产一区二区三区 | 久久久久久久大尺度免费视频| 免费播放大片免费观看视频在线观看| 欧美变态另类bdsm刘玥| 国模一区二区三区四区视频| 边亲边吃奶的免费视频| 少妇人妻精品综合一区二区| 我的老师免费观看完整版| 亚洲人成网站在线播| 一级,二级,三级黄色视频| 啦啦啦啦在线视频资源| 国内揄拍国产精品人妻在线| 久久国产精品男人的天堂亚洲 | www.av在线官网国产| 18禁在线无遮挡免费观看视频| 亚洲精品自拍成人| 女的被弄到高潮叫床怎么办| 国产伦精品一区二区三区视频9| 亚洲精品一二三| 偷拍熟女少妇极品色| 国产欧美亚洲国产| 国内精品宾馆在线| 国产极品天堂在线| 国产精品久久久久久久久免| 欧美国产精品一级二级三级 | 免费久久久久久久精品成人欧美视频 | 久久女婷五月综合色啪小说| 久久人人爽人人片av| 日韩精品有码人妻一区| 久久久a久久爽久久v久久| 人人澡人人妻人| 99精国产麻豆久久婷婷| 水蜜桃什么品种好| 亚洲av男天堂| 赤兔流量卡办理| 久久99热这里只频精品6学生| 女人久久www免费人成看片| 一级黄片播放器| 精品国产一区二区久久| 中国美白少妇内射xxxbb| 国产免费一区二区三区四区乱码| 亚洲美女黄色视频免费看| 亚洲av在线观看美女高潮| 一级二级三级毛片免费看| 久久久久久久久久人人人人人人| 男人和女人高潮做爰伦理| 亚洲欧洲国产日韩| 精品视频人人做人人爽| 成人影院久久|