• <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]).

    五月开心婷婷网| 亚洲va在线va天堂va国产| av国产精品久久久久影院| 能在线免费看毛片的网站| 人妻系列 视频| 韩国高清视频一区二区三区| 丝袜喷水一区| 日韩大片免费观看网站| 大片免费播放器 马上看| 狂野欧美激情性bbbbbb| 乱码一卡2卡4卡精品| 欧美高清成人免费视频www| 欧美日韩综合久久久久久| 精品人妻偷拍中文字幕| 国国产精品蜜臀av免费| 免费观看的影片在线观看| 亚洲久久久久久中文字幕| 国产毛片在线视频| 国产一区二区三区av在线| 久久久精品94久久精品| 在线 av 中文字幕| 亚洲三级黄色毛片| 国产熟女欧美一区二区| 我的女老师完整版在线观看| 一区二区三区四区激情视频| 18禁动态无遮挡网站| 久久亚洲国产成人精品v| 午夜福利网站1000一区二区三区| 国产成人福利小说| 日本一二三区视频观看| 成人美女网站在线观看视频| 三级经典国产精品| 亚洲av成人精品一二三区| 午夜亚洲福利在线播放| 久热久热在线精品观看| www.av在线官网国产| 欧美亚洲 丝袜 人妻 在线| 国产av不卡久久| 好男人视频免费观看在线| 欧美xxxx性猛交bbbb| 狂野欧美激情性bbbbbb| 午夜免费观看性视频| 制服丝袜香蕉在线| 日韩av免费高清视频| 高清欧美精品videossex| 别揉我奶头 嗯啊视频| 黄色配什么色好看| 日韩中字成人| 国产免费一区二区三区四区乱码| 乱码一卡2卡4卡精品| 欧美日韩综合久久久久久| 日韩制服骚丝袜av| 国产亚洲av嫩草精品影院| 亚洲欧美日韩另类电影网站 | 一级二级三级毛片免费看| 狂野欧美白嫩少妇大欣赏| 大又大粗又爽又黄少妇毛片口| 国产高清不卡午夜福利| 免费av毛片视频| 亚洲国产精品成人综合色| 成人鲁丝片一二三区免费| 尾随美女入室| 午夜日本视频在线| 午夜免费鲁丝| 亚洲精品乱码久久久v下载方式| 亚洲最大成人中文| 亚洲美女视频黄频| 男插女下体视频免费在线播放| 国产 一区 欧美 日韩| 欧美激情国产日韩精品一区| 视频区图区小说| 天天躁日日操中文字幕| 伊人久久国产一区二区| 亚洲欧美精品自产自拍| 久久久久久国产a免费观看| 人妻少妇偷人精品九色| av专区在线播放| 午夜福利高清视频| 国产高清国产精品国产三级 | 午夜免费男女啪啪视频观看| 亚洲激情五月婷婷啪啪| 天美传媒精品一区二区| 干丝袜人妻中文字幕| 欧美人与善性xxx| 日本色播在线视频| 校园人妻丝袜中文字幕| 国产在线一区二区三区精| 国产老妇女一区| 七月丁香在线播放| 免费黄色在线免费观看| 国产精品国产av在线观看| 国产乱人视频| 日韩强制内射视频| 日韩一区二区三区影片| 97超碰精品成人国产| 精品人妻偷拍中文字幕| 91在线精品国自产拍蜜月| 久热久热在线精品观看| 美女脱内裤让男人舔精品视频| av免费在线看不卡| 久久久久网色| 国产毛片在线视频| 国产成人91sexporn| 最近手机中文字幕大全| 国产欧美日韩精品一区二区| 亚洲欧美日韩无卡精品| 大片免费播放器 马上看| 极品少妇高潮喷水抽搐| 高清午夜精品一区二区三区| 久久久久久久午夜电影| 国语对白做爰xxxⅹ性视频网站| 色视频www国产| 欧美高清成人免费视频www| 国产精品无大码| 日日摸夜夜添夜夜爱| 99久久人妻综合| 精品国产一区二区三区久久久樱花 | av福利片在线观看| av又黄又爽大尺度在线免费看| 下体分泌物呈黄色| 日韩欧美一区视频在线观看 | 在线看a的网站| 国产男女内射视频| 欧美成人精品欧美一级黄| 岛国毛片在线播放| 啦啦啦在线观看免费高清www| 最近手机中文字幕大全| 国产伦理片在线播放av一区| 国产黄频视频在线观看| 国模一区二区三区四区视频| 久久久a久久爽久久v久久| 亚洲欧美一区二区三区黑人 | 亚洲av二区三区四区| 久久久久久伊人网av| 亚洲欧美清纯卡通| 亚洲性久久影院| 久久精品国产自在天天线| 成人无遮挡网站| 午夜精品一区二区三区免费看| 久久久亚洲精品成人影院| 偷拍熟女少妇极品色| 麻豆乱淫一区二区| 免费av不卡在线播放| 国产精品一及| 99热这里只有是精品在线观看| 国产成人freesex在线| 一区二区av电影网| 免费在线观看成人毛片| 看十八女毛片水多多多| 男女国产视频网站| 亚洲精品国产av蜜桃| 国产伦理片在线播放av一区| 成人国产av品久久久| 精品熟女少妇av免费看| 综合色av麻豆| 亚洲精品国产av蜜桃| 欧美日韩一区二区视频在线观看视频在线 | 高清欧美精品videossex| 男女无遮挡免费网站观看| 最近中文字幕2019免费版| 午夜激情久久久久久久| 久热久热在线精品观看| 两个人的视频大全免费| 丝袜美腿在线中文| 亚洲av中文字字幕乱码综合| 91午夜精品亚洲一区二区三区| 久久久久久国产a免费观看| 婷婷色av中文字幕| 中国美白少妇内射xxxbb| 欧美bdsm另类| 观看美女的网站| 国产乱人偷精品视频| 欧美三级亚洲精品| 欧美一区二区亚洲| 国产一区有黄有色的免费视频| 三级国产精品欧美在线观看| 久久久精品94久久精品| 在线观看人妻少妇| 男女啪啪激烈高潮av片| 国模一区二区三区四区视频| 人人妻人人爽人人添夜夜欢视频 | 大陆偷拍与自拍| 国国产精品蜜臀av免费| 国产大屁股一区二区在线视频| 欧美日韩一区二区视频在线观看视频在线 | 亚洲欧美中文字幕日韩二区| 女人久久www免费人成看片| 五月玫瑰六月丁香| 特大巨黑吊av在线直播| 国产免费一级a男人的天堂| 观看美女的网站| 又黄又爽又刺激的免费视频.| 成人毛片60女人毛片免费| 国产精品精品国产色婷婷| 丝瓜视频免费看黄片| 永久免费av网站大全| 亚洲精品久久午夜乱码| 在线观看一区二区三区激情| 国产精品国产三级专区第一集| 91精品伊人久久大香线蕉| 黄色欧美视频在线观看| 亚洲美女视频黄频| 99热全是精品| 永久网站在线| 大片免费播放器 马上看| 亚洲av中文字字幕乱码综合| 搡女人真爽免费视频火全软件| 男人和女人高潮做爰伦理| 国产精品99久久久久久久久| 色吧在线观看| 久久99热6这里只有精品| 最近中文字幕2019免费版| 久久ye,这里只有精品| 亚洲av在线观看美女高潮| 亚洲精品乱码久久久久久按摩| 亚洲国产精品成人综合色| 美女被艹到高潮喷水动态| 看非洲黑人一级黄片| 久久久久九九精品影院| 伦理电影大哥的女人| 久久久国产一区二区| 国产精品伦人一区二区| 国产成人freesex在线| 国产成人精品婷婷| 免费看av在线观看网站| 亚洲激情五月婷婷啪啪| 国产精品嫩草影院av在线观看| 尾随美女入室| 国产精品三级大全| 国产综合懂色| 亚洲欧美成人综合另类久久久| 下体分泌物呈黄色| 伦理电影大哥的女人| 久久久久久久久大av| 国内精品宾馆在线| 欧美97在线视频| 国产爱豆传媒在线观看| 亚洲美女视频黄频| 少妇的逼好多水| 美女cb高潮喷水在线观看| 久久精品夜色国产| 国产色婷婷99| 免费观看av网站的网址| 亚州av有码| 日韩欧美精品免费久久| 成年av动漫网址| 夫妻性生交免费视频一级片| 午夜福利在线在线| 免费电影在线观看免费观看| 精品久久久久久久末码| 秋霞在线观看毛片| 女人被狂操c到高潮| 国产探花极品一区二区| 日本午夜av视频| 免费大片18禁| 青春草国产在线视频| 天堂网av新在线| 99久久精品一区二区三区| av线在线观看网站| 国产毛片在线视频| 少妇被粗大猛烈的视频| 国产免费一区二区三区四区乱码| 精品久久久噜噜| 亚洲av日韩在线播放| 久久久久久国产a免费观看| 青春草国产在线视频| a级一级毛片免费在线观看| 国产av码专区亚洲av| 18禁裸乳无遮挡动漫免费视频 | 69人妻影院| 中文字幕制服av| 精品国产露脸久久av麻豆| 一区二区三区精品91| 亚洲av日韩在线播放| 美女国产视频在线观看| 精品久久国产蜜桃| 少妇人妻精品综合一区二区| a级一级毛片免费在线观看| 亚洲av日韩在线播放| 91久久精品国产一区二区三区| 国产淫片久久久久久久久| 成人综合一区亚洲| 久久久久久九九精品二区国产| 免费电影在线观看免费观看| 精品久久久久久久久av| 国模一区二区三区四区视频| 亚洲美女搞黄在线观看| 波野结衣二区三区在线| 少妇丰满av| 免费高清在线观看视频在线观看| 精品人妻视频免费看| 国产精品三级大全| 久久午夜福利片| 色视频www国产| 91狼人影院| 国产探花极品一区二区| 亚洲精品日韩av片在线观看| 久久影院123| 久久久久精品性色| 日韩一区二区视频免费看| 亚洲色图av天堂| 日日撸夜夜添| 国产淫片久久久久久久久| 亚洲无线观看免费| 中文在线观看免费www的网站| 寂寞人妻少妇视频99o| av一本久久久久| 女的被弄到高潮叫床怎么办| 黄色日韩在线| 精品久久国产蜜桃| 熟妇人妻不卡中文字幕| av网站免费在线观看视频| 久久久久久久精品精品| 国产日韩欧美亚洲二区| 国内精品美女久久久久久| 亚洲精品色激情综合| 亚洲欧美一区二区三区国产| 国产精品99久久久久久久久| 亚洲综合色惰| 丝袜脚勾引网站| 内射极品少妇av片p| 国产精品一及| 天堂俺去俺来也www色官网| 精品国产一区二区三区久久久樱花 | 如何舔出高潮| 在线a可以看的网站| 亚洲熟女精品中文字幕| 边亲边吃奶的免费视频| 亚洲欧美日韩无卡精品| av在线播放精品| av线在线观看网站| 永久免费av网站大全| 偷拍熟女少妇极品色| 亚洲欧美中文字幕日韩二区| 国产一区有黄有色的免费视频| 两个人的视频大全免费| 日韩强制内射视频| 久热久热在线精品观看| 精品视频人人做人人爽| 国产熟女欧美一区二区| 嫩草影院精品99| 国产精品久久久久久精品古装| 91狼人影院| www.色视频.com| 亚洲欧美中文字幕日韩二区| 国产一区二区三区综合在线观看 | 国产伦精品一区二区三区四那| 久久久久精品久久久久真实原创| 国产 精品1| 久久久久久久久久久免费av| 噜噜噜噜噜久久久久久91| 久久久久久久大尺度免费视频| 欧美三级亚洲精品| 久久综合国产亚洲精品| 99热这里只有是精品50| 国产精品成人在线| 亚洲国产精品成人久久小说| 午夜福利视频精品| 最近最新中文字幕大全电影3| 永久网站在线| 久久精品综合一区二区三区| 亚洲不卡免费看| 午夜福利高清视频| 亚洲aⅴ乱码一区二区在线播放| 夜夜爽夜夜爽视频| 日韩欧美精品v在线| 男插女下体视频免费在线播放| 精品久久久噜噜| 搡女人真爽免费视频火全软件| 在线 av 中文字幕| 亚洲国产日韩一区二区| 3wmmmm亚洲av在线观看| 免费大片18禁| 联通29元200g的流量卡| 韩国av在线不卡| 久久久久性生活片| 国产精品.久久久| 成人特级av手机在线观看| 中文字幕制服av| 国产永久视频网站| 国产精品久久久久久av不卡| 搞女人的毛片| 国产亚洲午夜精品一区二区久久 | 日本色播在线视频| 51国产日韩欧美| 国产午夜福利久久久久久| 亚洲国产精品成人综合色| 高清视频免费观看一区二区| 一级毛片 在线播放| 国产久久久一区二区三区| 亚洲av国产av综合av卡| 精品久久久精品久久久| 亚洲美女搞黄在线观看| 3wmmmm亚洲av在线观看| 女人被狂操c到高潮| 久久久午夜欧美精品| av女优亚洲男人天堂| 国产熟女欧美一区二区| 亚洲婷婷狠狠爱综合网| 看免费成人av毛片| 美女xxoo啪啪120秒动态图| 一级爰片在线观看| 久久久久久伊人网av| 日本三级黄在线观看| 日本三级黄在线观看| 国产极品天堂在线| 久久午夜福利片| 看免费成人av毛片| 高清av免费在线| 又黄又爽又刺激的免费视频.| 国产精品av视频在线免费观看| 国产精品久久久久久精品电影小说 | 欧美性感艳星| 久久久a久久爽久久v久久| 寂寞人妻少妇视频99o| 亚洲av日韩在线播放| 一级毛片 在线播放| 亚洲最大成人手机在线| 色5月婷婷丁香| 国产成人91sexporn| 一边亲一边摸免费视频| 性色av一级| 交换朋友夫妻互换小说| 69av精品久久久久久| 99热这里只有是精品50| 亚洲国产精品专区欧美| 麻豆乱淫一区二区| 身体一侧抽搐| 欧美日韩国产mv在线观看视频 | 可以在线观看毛片的网站| 国产成人午夜福利电影在线观看| av免费观看日本| 亚洲最大成人手机在线| 亚洲欧美成人精品一区二区| 久久精品久久久久久噜噜老黄| 热99国产精品久久久久久7| 欧美激情国产日韩精品一区| 久久久国产一区二区| 亚洲精品国产av蜜桃| 国产永久视频网站| 色网站视频免费| 我要看日韩黄色一级片| 国产亚洲精品久久久com| 国产伦理片在线播放av一区| 国产精品人妻久久久影院| 亚洲精品一区蜜桃| 免费看a级黄色片| 在现免费观看毛片| 久久久精品免费免费高清| 国产一区二区三区av在线| 久久精品夜色国产| 国产高潮美女av| 日韩成人av中文字幕在线观看| 男女那种视频在线观看| 成人毛片60女人毛片免费| 久久精品综合一区二区三区| av线在线观看网站| 大陆偷拍与自拍| 色哟哟·www| 极品少妇高潮喷水抽搐| 国产精品福利在线免费观看| 一级毛片我不卡| 波多野结衣巨乳人妻| 高清日韩中文字幕在线| 欧美丝袜亚洲另类| 人妻制服诱惑在线中文字幕| 国产亚洲5aaaaa淫片| 午夜老司机福利剧场| 国产欧美亚洲国产| 久久人人爽人人爽人人片va| 中文字幕制服av| 亚洲精品自拍成人| 偷拍熟女少妇极品色| 亚洲精品国产av蜜桃| 免费观看a级毛片全部| 国产在视频线精品| 美女脱内裤让男人舔精品视频| 久久这里有精品视频免费| 亚洲熟女精品中文字幕| 国产亚洲av片在线观看秒播厂| 日韩三级伦理在线观看| 波多野结衣巨乳人妻| 免费观看性生交大片5| 九九在线视频观看精品| 国产中年淑女户外野战色| eeuss影院久久| tube8黄色片| 中国三级夫妇交换| 国产精品不卡视频一区二区| 听说在线观看完整版免费高清| 熟女av电影| 一区二区av电影网| 嫩草影院新地址| 人人妻人人看人人澡| xxx大片免费视频| 国产久久久一区二区三区| 又大又黄又爽视频免费| 欧美 日韩 精品 国产| 亚洲精品成人久久久久久| 热re99久久精品国产66热6| av在线观看视频网站免费| 少妇熟女欧美另类| 只有这里有精品99| 免费看av在线观看网站| 精品人妻视频免费看| 女的被弄到高潮叫床怎么办| 欧美bdsm另类| 亚洲不卡免费看| 久久久久久久久大av| 国产日韩欧美亚洲二区| 一级毛片 在线播放| 亚洲av成人精品一区久久| 国产欧美另类精品又又久久亚洲欧美| 一级爰片在线观看| 高清av免费在线| 久久久精品免费免费高清| av一本久久久久| 日韩在线高清观看一区二区三区| 亚洲av电影在线观看一区二区三区 | 男人添女人高潮全过程视频| 一级a做视频免费观看| 欧美变态另类bdsm刘玥| 在线观看国产h片| a级一级毛片免费在线观看| 久久精品综合一区二区三区| 久久久欧美国产精品| 超碰av人人做人人爽久久| 亚洲三级黄色毛片| 精品一区在线观看国产| 色5月婷婷丁香| 啦啦啦中文免费视频观看日本| 少妇高潮的动态图| 久久午夜福利片| av.在线天堂| 嫩草影院入口| 亚洲精品456在线播放app| 精品人妻视频免费看| 免费看av在线观看网站| 久久精品久久久久久噜噜老黄| 免费黄频网站在线观看国产| 国产黄a三级三级三级人| 晚上一个人看的免费电影| 99热网站在线观看| 国产日韩欧美在线精品| 久久久久国产网址| 一级毛片我不卡| 三级经典国产精品| 欧美另类一区| 国产伦在线观看视频一区| 91久久精品国产一区二区成人| 成年版毛片免费区| 最近手机中文字幕大全| 亚洲av日韩在线播放| 少妇熟女欧美另类| 精品久久久久久久久亚洲| 高清在线视频一区二区三区| 日韩av免费高清视频| 伦精品一区二区三区| 能在线免费看毛片的网站| 寂寞人妻少妇视频99o| 日本黄色片子视频| 久久久久久久久大av| 亚洲三级黄色毛片| 超碰av人人做人人爽久久| 波野结衣二区三区在线| 久久午夜福利片| 午夜福利在线观看免费完整高清在| 亚洲欧美一区二区三区国产| 亚洲在久久综合| 国产免费一区二区三区四区乱码| 永久网站在线| 亚洲欧美日韩另类电影网站 | 国产午夜精品一二区理论片| 麻豆国产97在线/欧美| 中国美白少妇内射xxxbb| 69av精品久久久久久| 国产av码专区亚洲av| 国产精品99久久99久久久不卡 | 久久精品国产自在天天线| 精品亚洲乱码少妇综合久久| 欧美精品国产亚洲| 日韩成人伦理影院| 在线观看免费高清a一片| 全区人妻精品视频| 国产美女午夜福利| 国产黄频视频在线观看| 日本三级黄在线观看| 午夜激情久久久久久久| 亚洲国产精品999| 国产成人免费无遮挡视频| 国产成人精品久久久久久| 日韩 亚洲 欧美在线| av免费观看日本| 国产日韩欧美亚洲二区| 久久久久久国产a免费观看| 不卡视频在线观看欧美| 国产在视频线精品| 亚洲av国产av综合av卡| 蜜桃久久精品国产亚洲av| 久久久国产一区二区| 亚洲欧美日韩东京热| 欧美日韩国产mv在线观看视频 | 各种免费的搞黄视频| www.av在线官网国产| 99热全是精品| 又粗又硬又长又爽又黄的视频| .国产精品久久| 成人二区视频| 国产男人的电影天堂91| 久久久a久久爽久久v久久| 一二三四中文在线观看免费高清| 亚洲真实伦在线观看| 一级爰片在线观看| 亚洲高清免费不卡视频| 少妇人妻一区二区三区视频|