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

    Neighborhood Contingency Logic:A New Perspective*

    2018-12-26 03:40:18JieFan
    邏輯學(xué)研究 2018年4期

    Jie Fan

    School of Humanities,University of Chinese Academy of Sciences

    jiefan@ucas.ac.cn

    Abstract.In this paper,we propose a new neighborhood semantics for contingency logic,by introducing a simple property in standard neighborhood models.This simplifies the neighborhood semantics given in Fan and van Ditmarsch(2015),but does not change the set of valid formulas.Under this perspective,among various notions of bisimulation and respective Hennessy-Milner Theorems,we show that c-bisimulation is equivalent to nbh-?-bisimulation in the literature,which guides us to understand the essence of the latter notion.This perspective also provides various frame definability and axiomatization results.

    1 Introduction

    Under Kripke semantics,contingency logic(CL for short)is non-normal,less expressive than standard modal logic(ML for short),and the five basic frame properties(seriality,reflexivity,transitivity,symmetry,Eucludicity)cannot be defined in CL.This makes the axiomatizations of CL nontrivial:although there have been a mountain of work on the axiomatization problem since the 1960s[15,9,10,11,12],overK,D,T,4,5 and any combinations thereof,no method in the cited work can uniformly handle all the five basic frame properties.This job has not been addressed until in[5],which also contains an axiomatization of CL onBand its multi-modal version.This indicates that Kripke semantics may not be suitable for CL.

    Partly inspired by the above motivation(in particular,the non-normality of CL),and partly by a weaker logical omniscience in Kripke semantics(namely,all theorems are known to be true or known to be false),a neighborhood semantics for CL is proposed in[4],which interprets the non-contingency operator?in a way such that its philosophical intuition,viz.necessarily true or necessarily false,holds.However,under this(old)semantics,as shown in[4],CL is still less expressive than ML on various classes of neighborhood models,and many usual neighborhood frame properties are undefinable in CL.Moreover,based on this semantics,[1]proposes a bisimulation(called ‘nbh-?-bisimulation’there)to characterize CL within ML and within first-order logic(FOL for short),but the essence of the bisimulation seems not quite clear.

    In retrospect, no matter whether the semantics for CL is Kripke-style or neigborhoodstyle in the sense of[4],there is an asymmetry between the syntax and models of CL:on the one hand,the language is too weak,since it is less expressive than ML over various model classes;on the other hand,the models are too strong,since its models are the same as those of ML.This makes it hard to handle CL.1Analogous problem occurs in the setting of knowing-value logic[13,14].

    Inspired by[6],we simplify the neighborhood semantics for CL in[4],and meanwhile keep the logic(valid formulas)the same by restricting models.This can weaken the too strong models so as to balance the syntax and models for CL.Under this new perspective,we can gain a lot of things,for example,bisimulation notions and their corresponding Hennessy-Milner Theorems,and frame definability.Moreover,we show that one of the bisimulation notions is equivalent to the notion of nbh-?-bisimulation,which helps us understand the essence of nbh-?-bisimulation.We also obtain some simple axiomatizations.

    2 Preliminaries

    2.1 Language and old neighborhood semantics

    First,we introduce the language and the old neighborhood semantics of CL.Fix a countable set Prop of propositional variables.The language of CL,denotedL?,is an extension of propositional logic with a sole primitive modality?,wherep∈Prop.

    ?φis read “it is non-contingent thatφ”.?φ,read “it is contingent thatφ”,abbreviates??φ.

    A neighborhood model forL?is defined as that for the languageL□of ML.That is,to sayM=?S,N,V?is a neighborhood model,ifSis a nonempty set of states,N:S→22Sis a valuation assigning each propositional variable inSa set of neighborhoods,andV:Prop→2Sis a valuation assigning each propositional variable in Prop a set of states in which it holds.A neighborhood frame is a neighborhood model without any valuation.

    There are a variety of neighborhood properties.The following list is taken from[4,Def.3].

    Definition 1(Neighborhood properties)

    (n):N(s)contains the unit,ifS∈N(s).

    (r):N(s)contains its core,if∩N(s)∈N(s).

    (i):N(s)is closed under intersections,ifX,Y∈N(s)impliesX∩Y∈N(s).

    (s):N(s)issupplemented,orclosed under supersets,ifX∈N(s)andX?Y?SimpliesY∈N(s).We also call this property ‘monotonicity’.

    (c):N(s)isclosed under complements,ifX∈N(s)impliesSX∈N(s).

    (d):X∈N(s)impliesSX/∈N(s).

    (t):X∈N(s)impliess∈X.

    (b):s∈Ximplies{u∈S|SX/∈N(u)}∈N(s).

    (4):X∈N(s)implies{u∈S|X∈N(u)}∈N(s).

    (5):X/∈N(s)implies{u∈S|X/∈N(u)}∈N(s).

    FrameF=?S,N?(and the corresponding model)possesses such a propertyP,ifN(s)has the propertyPfor eachs∈S,and we call the frame(resp.the model)P-frame(resp.P-model).

    Given a neighborhood modelM=?S,N,V?ands∈S,the old neighborhood semantics ofL?[4]is defined as follows,whereφM?={t∈S|M,t?φ}.

    2.2 Existing results on old neighborhood semantics

    Under the above old neighborhood semantics,it is shown in[4,Props.2-7]that on the class of(t)-models or the class of(c)-models,L?is equally expressive asL□;however,on other class of models in Def.1,L?is less expressive thanL□;moreover,noneof frame properties in the above list are definable in CL.

    Based on the above semantics for CL,a notion of bisimulation is proposed in[1],which is inspired by the definition ofprecocongruencesin[8]and the old neighbourhood semantics of?.

    Definition 2(nbh-?-bisimulation)LetM=?S,N,V?andM′=?S′,N′,V′?be neighborhood models.A nonempty relationZ?S×S′isanbh-?-bisimulationbetweenMandM′,if for all(s,s′)∈Z,

    (Atoms)s∈V(p)iffs′∈V′(p)for allp∈Prop;

    (Coherence)if the pair(U,U′)isZ-coherent,2Let R be a binary relation.We say(U,U′)is R-coherent,if for any(x,y)∈ R,we have x ∈ U iff y ∈ U′.We say U is R-closed,if(U,U)is R-coherent.It is obvious that(?,?)is R-coherent for any R.then

    (M,s)and(M′,s′)isnbh-?-bisimilar,notation(M,s)~?(M′,s′),if there is a nbh-?-bisimulation betweenMandM′containing(s,s′).3In fact,the notion of nbh-?-bisimilarity is defined in a more complex way in[1].It is easy to show that our definition is equivalent to,but simpler than,that one.

    Although it is inspired by both the definition ofprecocongruencesin[8]and the old neighbourhood semantics of?,the essence of nbh-?-bisimulation seems not so clear.

    It is then proved that Hennessy-Milner Theorem holds for nbh-?-bisimulation.For this,a notion of?-saturated model is required.

    Definition 3(?-saturated model) [1,Def.11]LetM=?S,N,V?be a neighborhood model.A setX?Sis?-compact,if every set ofL?-formulas that is finitely satisfiable inXis itself also satisfiable inX.Mis said to be?-saturated,if for alls∈Sand all≡L?-closed neighborhoodsX∈N(s),bothXandSXare?-compact.

    Theorem 1(Hennessy-Milner Theorem for nbh-?-bisimulation) [1,Thm.1]On?-saturated modelsMandM′and statessinMands′inM′,if(M,s)≡L?(M′,s′),then(M,s)~?(M′,s′).

    3 A new semantics for CL

    As mentioned above,there is an asymmetry between the syntax and neighborhood models of CL,which makes it hard to tackle CL.In this section,we propose a new neighborhood semantics for this logic.This semantics is simpler than the old one,but the two semantics are equivalent in that their logics(valid formulas)are the same.

    The new neighborhood semantics?and the old one?differ only in the case of non-contingency operator.

    whereφM={t∈M|M,t?φ}.To say two models with the same domain arepointwise equivalent,if every world in both models satisfies the same formulas.

    We hope that although we change the semantics,the validities are still kept the same as the old one.So how to make it out?Recall that non-contingency means necessarily true or necessarily false,which implies that?p???pshould be valid.However,although the formula is indeed valid under the old neighborhood semantics,it is invalid under the new one.In order to make this come about,we need make some restriction to the models.Look at a proposition first.

    Proposition 1Under the new semantics,?p???pdefines the property(c).

    ProofLetF=?S,N?be a neighborhood frame.

    First,supposeFpossesses(c),weneedtoshowF??p???p.Forthis,assume any modelMbased onFands∈Ssuch thatM,s??p,thuspM∈N(s).By(c),SpM∈N(s),i.e.,(?p)M∈N(s),which means exactlyM,s???p.Now assumeM,s? ??p,we have(?p)M∈N(s),that isSpM∈N(s).By(c),S(SpM)∈N(s),i.e.pM∈N(s),and thusM,s? ?p.HenceM,s? ?p???p,and thereforeF??p???p.

    Conversely,supposeFdoes not possess(c),we need to showF?? ?p???p.By supposition,there existsXsuch thatX∈N(s)butSX/∈N(s).Definea valuationVonFasV(p)=X.We have nowpM=V(p)∈N(s),thusM,s? ?p.On the other side,V(?p)=SX/∈N(s),thusM,s?p.HenceM,sp→??p,and thereforeF?? ?p???p. □

    This means that in order to guarantee the validity?p???punder new semantics,we(only)need to ‘force’the model to have the property(c).Thus from now on,we assume(c)to be theminimalcondition of a neighborhood model,and call this type of model‘c-models’.

    Definition 4(c-structures) A model is ac-model,if it has the property(c);intuitively,if a proposition is non-contingent at a state in the domain,so is its negation.A frame is ac-frame,if the models based on it arec-models.

    The following proposition states that onc-models,the new neighborhood semantics and the old one coincide with each other in terms ofL?satisfiability.

    Proposition 2LetM=?S,N,V?be ac-model.Then for allφ∈L?,for alls∈S,we haveM,s?φ??M,s?φ,i.e.,φM=φM?.

    ProofBy induction onφ∈L?.The only nontrivial case is?φ.

    First,supposeM,s? ?φ,thenφM∈N(s).By induction hypothesis,φM?∈N(s).Of course,φM?∈N(s)or(?φ)M?∈N(s).This entails thatM,s??φ.

    Conversely,assumeM,s? ?φ,thenφM?∈N(s)or(?φ)M?∈N(s).SinceMis ac-model,we can obtainφM?∈N(s).By induction hypothesis,φM∈N(s).Therefore,M,s??φ. □

    Definition 5(c-variation)LetM=?S,N,V?be a neighborhood model.We sayc(M)is ac-variationofM,ifc(M)=?S,cN,V?,where for alls∈S,cN(s)={X?S:X∈N(s)orSX∈N(s)}.

    The definition ofcNis very natural,in that just as“X∈N(s)orSX∈N(s)”corresponds to the old semantics of?,X∈cN(s)corresponds to the new semantics of?.It is easy to see that every neighborhood model has a solec-variation,that every suchc-variation is a c-model,and moreover,for any neighborhood modelM,ifMis already ac-model,thenc(M)=M.

    Proposition 3LetMbe a neighborhood model.Then for allφ∈L?,for alls∈M,we haveM,s?φ??c(M),s?φ,i.e.,φM?=φc(M).

    ProofThe proof is by induction onφ,where the only nontrivial case is?φ.We have

    Let Γ ?cφdenote that Γ entailsφover the class of allc-models,i.e.,for eachc-modelMand eachs∈M,ifM,s?ψfor everyψ∈Γ,thenM,s?φ.With Props.2 and 3 in hand,we obtain immediately that

    Corollary 1For all ?!葅φ}?L?,Γ?cφ??Γ?φ.Therefore,for allφ∈L?,?cφ???φ.

    In this way,we strengthened the expressive power of CL,since it is now equally expressive as ML,and kept the logic(valid formulas)the same as the old neighborhood semantics.The noncontingency operator? can now be seen as a package of□ and?in the old neighborhood semantics;under the new neighborhood semantics,on the one hand,it is interpreted just as□;on the other hand,it retains the validity?p???p.

    4 c-Bisimulation

    Recall that the essence of the notion of nbh-?-bisimulation proposed in[1]is not so clear.In this section,we introduce a notion ofc-bisimulation,and show that this notion is equivalent to nbh-?-bisimulation.Thec-bisimulation is inspired by both Prop.1 and the definition ofprecocongruencesin[8,Prop.3.16].Intuitively,the notion is obtained by just adding the property(c)into the notion of precocongruences.

    Definition 6(c-bisimulation)LetM=?S,N,V?andM′=?S′,N′,V′?becmodels.A nonempty relationZ?S×S′is ac-bisimulationbetweenMandM′,if for all(s,s′)∈Z,

    (i)s∈V(p)iffs′∈V′(p)for allp∈Prop;

    (ii)if the pair(U,U′)isZ-coherent,thenU∈N(s)iffU′∈N′(s′).

    We say(M,s)and(M′,s′)arec-bisimilar,written(M,s)?c(M′,s′),if there is a c-bisimulationZbetweenMandM′such that(s,s′)∈Z.

    Notethatbothc-bisimulation andc-bisimilarity are defined betweenc-models,rather than between any neighborhood models.L?formulas are invariant underc-bisimilarity.

    Proposition 4LetMandM′bec-models,s∈Mand

    ProofLetM=?S,N,V?andM′=?S′,N′,V′?be bothc-models.By induction onφ∈L?.The nontrivial case is?φ.

    (?)follows from the fact that-coherent plus the condition(ii)ofcbisimulation.To see why-coherent,the proof goes as follows:if for anythen by induction hypothesis,M,x?φiff

    Now we are ready to show the Hennessy-Milner Theorem forc-bisimulation.Sincec-bisimulation is defined betweenc-models,we need also to add the propertycinto the notion of?-saturated models in Def.3.

    Definition 7(?-saturatedc-model) LetM=?S,N,V?be ac-model.A setX?Sis?-compact,if every set ofL?-formulas that is finitely satisfiable inXis itself also satisfiable inX.Mis said to be?-saturated,if for alls∈Sand all≡L?-closed neighborhoodX∈N(s),Xis?-compact.4Note that we do not distinguish≡L? here from that in Def.3 despite different neighborhood semantics.This is because as we show in Prop.2,on c-models the two neighborhood semantics are the same in terms of L?satisfiability.Thus it does not matter which semantics is involved in the current context.

    In the above definition of?-saturatedc-model,we write“Xis?-compact”,rather than “bothXandSXare?-compact”,since under the condition thatX∈N(s)and the property(c),these two statements are equivalent.Thus each?-saturatedc-model must be a?-saturated model.

    We will demonstrate that on?-saturatedc-models,L?-equivalence impliesc-bisimilarity,for which we prove that the notion of c-bisimulation is equivalent to that of nbh-?-bisimulation,in the sense that every nbh-?-bisimulation(between neighborhood models)is a c-bisimulation(betweenc-models),and vice versa.By doing so,we can see clearly the essence of nbh-?-bisimulation,i.e.precocongruences with property(c).

    Proposition 5LetM=?S,N,V?andM′=?S′,N′,V′?be neighborhood models.IfZis a nbh-?-bisimulation betweenMandM′,thenZis a c-bisimulation betweenc(M)andc(M′).

    ProofSuppose thatZis a nbh-?-bisimulation betweenMandM′,to showZis a c-bisimulation betweenc(M)andc(M′).

    First,one can easily verify thatc(M)andc(M′)are bothc-models.

    Second,assume that(s,s′)∈Z.SinceMandc(M)have the same domain and valuation,item(i)can be obtained from the supposition and(Atoms).For item(ii),let(U,U′)beZ-coherent.We need to show thatU∈cN(s)iffU′∈cN′(s′).For this,we have the following line of argumentation:U∈cN(s)iff(by definition ofcN)(U∈N(s)orSU∈N(s))iff(by(Coherence))(U′∈N′(s′)orS′U′∈N′(s′))iff(by definition ofcN′)U′∈cN′(s′). □

    Proposition 6LetM=?S,N,V?andM′=?S′,N′,V′?bec-models.IfZis a c-bisimulation betweenMandM′,thenZis a nbh-?-bisimulation betweenMandM′.

    ProofSuppose thatZis a c-bisimulation betweenc-modelsMandM′,to showZis a nbh-?-bisimulation betweenMandM′.Assume that(s,s′)∈Z,we only need to show(Atoms)and(Coherence)holds.(Atoms)is clear from(i).

    For(Coherence),letthepair(U,U′)isZ-coherent.Thenby(ii),U∈N(s)iffU′∈N′(s′).We also have that(SU,S′U′)isZ-coherent.Using(ii)again,we infer thatSU∈N(s)iffS′U′∈N′(s′).Therefore,(U∈N(s)orSU∈N(s))iff(U′∈N′(s′)orS′U′∈N′(s′)),as desired. □

    Since everyc-variation of ac-model is just the model itself,by Props.5 and 6,we obtain immediately that

    Corollary 2LetM=(S,N,V)andM′=?S′,N′,V′?be bothc-models.ThenZis ac-bisimulation betweenMandM′iffZis an nbh-?-bisimulation betweenMandM′.

    Theorem 2(Hennessy-Milner Theorem forc-bisimulation) LetMandM′be?-saturatedc-models,ands∈M,s′∈M′.If for all

    ProofSupposeMandM′are?-saturatedc-modelssuchthatforallφ∈L?,M,s?By Prop.2,we have that for allM′,s′?φ.Since each?-saturatedc-model is a?-saturated model,by Hennessy-Milner Theorem of nbh-?-bisimulation(Thm.1),we obtain(M,s)~?(M′,s′).Then by Coro.2,we conclude that

    5 Monotonic c-bisimulation

    This section proposes a notion of bisimulation for CL over monotonic,c-models.This notion can be obtained via two ways:one is to add the property of monotonicity(s)intoc-bisimulation,the other is to add the property(c)into monotonic bisimulation(for ML).5For the notion of monotonic bisimulation,refer to[7,Def.4.10].For the sake of reference,we call the notion obtained by the first way‘monotonicc-bisimulation’,and that obtained by the second way ‘c-monotonic bisimulation’.We will show that the two notions are indeed the same.

    Definition 8(Monotonicc-bisimulation)LetM=?S,N,V?andM′=?S′,N′,V′?bebothmonotonic,c-models.A nonempty binary relationZisamonotonicc-bisimulationbetweenMandM′,ifsZs′implies the following:

    (i)sands′satisfy the same propositional variables;

    (ii)If(U,U′)isZ-coherent,thenU∈N(s)iffU′∈N′(s′).

    (M,s)and(M′,s′)is said to bemonotonic c-bisimilar,written(M,s)?sc(M′,s′),if there is a monotonicc-bisimulation betweenMandM′such thatsZs′.

    Definition 9(c-monotonic bisimulation)LetM=?S,N,V?andM′=?S′,N′,V′?be both monotonic,c-models.A nonempty binary relationZis ac-monotonic bisimulationbetweenMandM′,ifsZs′implies the following:

    (Prop)sands′satisfy the same propositional variables;

    (c-m-Zig)ifX∈N(s),then there existsX′∈N′(s′)such that for allx′∈X′,there is anx∈Xsuch thatxZx′;

    (c-m-Zag)ifX′∈N′(s′),then there existsX∈N(s)such that for allx∈X,there is anx′∈X′such thatxZx′.

    (M,s)and(M′,s′)is said to bec-monotonic bisimilar,writtens′),if there is ac-monotonic bisimulation betweenMandM′such thatsZs′.

    Note that both monotonicc-bisimulation andc-monotonic bisimulation are defined between monotonic,c-models.

    Proposition 7Everyc-monotonic bisimulation is a monotonicc-bisimulation.

    ProofSuppose thatZis ac-monotonic bisimulation betweenMandM′,both of which are monotonic,c-models,to show thatZis also a monotonicc-bisimulation betweenMandM′.For this,assume thatsZs′,it suffices to show the condition(ii).

    Assume that(U,U′)isZ-coherent.IfU∈N(s),by(c-m-Zig),there existsX′∈N′(s′)such that for allx′∈X′,there is ax∈Usuch thatxZx′.By assumption andx∈UandxZx′,we havex′∈U′,thusX′?U′.Then by(s)andX′∈N′(s′),we conclude thatU′∈N′(s′).The converse is similar,but by using(c-m-Zag)instead. □

    Proposition 8Every monotonicc-bisimulation is ac-monotonic bisimulation.

    ProofSuppose thatZis a monotonicc-bisimulation betweenMandM′,both of which are monotonic,c-models,to show thatZis also ac-monotonic bisimulation betweenMandM′.For this,given thatsZs′,we need to show the condition(c-m-Zig)and(c-m-Zag).We show(c-m-Zig)only,since(c-m-Zag)is similar.

    Assume thatX∈N(s),defineX′={x′|xZx′for somex∈X}.It suffices to show thatX′∈N′(s′).The proof is as follows:by assumption and monotonicity ofM,we haveS∈N(s),then by(c),?∈N(s).Since(?,?)isZ-coherent,by(ii),we infer?∈N′(s′).From this and monotonicity ofM′,it follows thatX′∈N′(s′),as desired.□

    As a corollary,the aforementioned two ways enable us to get the same bisimulation notion.

    Corollary 3The notion of monotonicc-bisimulation is equal to the notion ofc-monotonic bisimulation.

    So we can choose either of the two bisimulation notions to refer to the notion of bisimulation of CL over monotonic,c-models.In the sequel,we choose the simpler one,that is,monotonicc-bisimulation.One may easily see that this notion is stronger than monotonic bisimulation(for ML).

    Similar to the case forc-bisimulation in Sec.4,we can show that

    Proposition 9LetMandM′be monotonic,c-models,s∈Mands′∈M′.Ifthen for all

    Theorem 3(Hennessy-Milner Theorem for monotonicc-bisimulation)LetMandM′be monotonic,?-saturatedc-models,s∈Mands′∈M′.If for allφ∈L?,M,s?

    Similarly,we can define regularc-bisimulation,which is obtained by adding the property(i)intomonotonicc-bisimulation,and show the corresponding Hennessy-Milner Theorem.We omit the details due to space limitation.

    6 Quasi-filter structures

    We define a class of structures,called ‘quasi-filter structures’.6Note that our notion of quasi-filter is different from that in[2,p.215],where quasi-filter is defined as(s)+(i).For example,the latter notion is not necessarily closed under complements.

    Definition 10(Quasi-filter frames and models) A neighborhood frameF=?S,N?is aquasi-filter frame,ifforalls∈S,N(s)possesses the properties(n),(i),(c),and(ws),where(ws)means being closed under supersets or co-supersets:for allX,Y,Z?S,X∈N(s)impliesX∪Y∈N(s)or(SX)∪Z∈N(s).

    We say a neighborhood model is aquasi-filter model,if its underlying frame is a quasi-filter frame.

    Note that in the above definition,the property(n)can be replaced with the property of“N(s)being nonempty”;in symbol,N(s)?=?.

    The main result of this section is the following:for CL,every Kripke model has a pointwise equivalent quasi-filter model,butnotvice versa.

    Definition 11(qf-variation) LetM=?S,R,V?is a Kripke model.qf(M)is said to be aqf-variationofM,ifqf(M)=?S,qfN,V?,where for anys∈S,qfN(s)={X?S:for anyt,u∈S,ifsRtandsRu,then(t∈Xiffu∈X)}.

    The definition ofqfNis also quitenatural,sincejustas“for anyt,u∈S,ifsRtandsRu,then(t∈Xiffu∈X)”corresponds to the Kripke semantics of?,X∈qfN(s)corresponds to the new neighborhood semantics of the operator,as will be seen more clearly in Prop.10.Note that the definition ofqfNcan be simplified as follows:

    It is easy to see that every Kripke model has a(sole)qf-variation.We will demonstrate that,every such qf-variation is a quasi-filter model.

    The following proposition states that every Kripke model and its qf-variation are pointwise equivalent.

    Proposition 10LetM=?S,R,V?be a Kripke model.Then for allφ∈L?,for alls∈S,we haveM,s?φ??qf(M),s?φ,i.e.,φM?=φqf(M),whereφM?={t∈S|M,t?φ}.

    ProofBy induction onφ.The nontrivial case is?φ.

    Proposition 11LetMbe a Kripke model.Thenqf(M)is a quasi-filter model.

    ProofLetM=?S,R,V?.For anys∈S,we show thatqf(M)has those four properties of quasi-filter models.

    (n):it is clear thatS∈qfN(s).

    (i):assume thatX,Y∈qfN(s),we showX∩Y∈qfN(s).By assumption,for alls,t∈S,ifsRtandsRu,thent∈Xiffu∈X,and for alls,t∈S,ifsRtandsRu,thent∈Yiffu∈Y.Therefore,for allt,u∈S,ifsRtandsRu,we have thatt∈X∩Yiffu∈X∩Y.This entailsX∩Y∈qfN(s).

    (c):assume thatX∈qfN(s),to showSX∈qfN(s).By assumption,for alls,t∈S,ifsRtandsRu,thent∈Xiffu∈X.Thus for alls,t∈S,ifsRtandsRu,thent∈SXiffu∈SX,i.e.,SX∈qfN(s).

    (ws):assume,for a contradiction,that for someX,Y,Z?Sit holds thatX∈qfN(s)butX∪Y/∈qfN(s)and(SX)∪Z/∈qfN(s).W.l.o.g.we assume that there aret1,u1such thatsRt1,sRu1andt1∈X∪Ybutu1/∈X∪Y,and there aret2,u2such thatsRt2,sRu2andt2/∈(SX)∪Zbutu2∈(SX)∪Z.Thent2∈Xandu1/∈X,which is contrary to the fact thatX∈qfN(s)andsRu1,sRt2.□

    The following result is immediate by Props.10 and 11.

    Corollary4ForCL,every Kripke model has a pointwise equivalent quasi-filter model.

    However,for CL,not every quasi-filter model has a pointwise equivalent Kripke model.The point is that quasi-filter models may not be closed underinfinite(i.e.arbitrary)intersections(see the property(r)in Def.1).

    Proposition 12For CL,there is a quasi-filter model that has no pointwise equivalent Kripke model.

    ProofConsider an infinite modelM=?S,N,V?,where

    7{2n for some n∈N}denotes the union of finitely many sets of the form{2n for some n∈N},e.g.{0}∪{2}∪{4}.

    It is not hard to check thatMis a quasi-filter model.8To verify(ws),we need only show the nontrivial caseFor this,we show a stronger result:for allThe cases for Z=S or Z=?are clear.For other cases,we partition the elements in Z nto three disjoint(possibly empty)parts:odd numbers,even numbers in even numbers inNote that the first and third parts all belong;moreover,the union of the second part andis also in N(s).Note that for alls∈S,pM/∈N(s),thusIn particular

    Suppose that there is a pointwise equivalent Kripke modelM′,thenThus there must be 2mand 2n+1 that are accessible from 0,wherem,n∈N.Since

    However,when we restrict quasi-filter models to finite cases,the situation will be different.

    Proposition 13For every finite quasi-filter modelM,there exists a pointwise equivalent Kripke modelM′,that is,for allφ∈L?,for all worldss,M′,s?φ??M,s?

    ProofLetM=?S,N,V?be a finite quasi-filter model.DefineM′=?S,R,V?,whereRis defined as follows:for anys,t∈S,

    We will show that for allφ∈L?and alls∈S,we have that

    The proof proceeds with induction onφ∈L?.The nontrivial case is?φ,that is to show,M′,s??φ??M,s??φ.

    “?=:”Suppose,for a contradiction,thatM,s? ?φ,butM′,s? ?φ.ThenφM∈N(s),and there aret,u∈Ssuch thatsRtandsRuandM′,t?φandM′,u?φ.SinceφM∈N(s),by(c),we getSφM∈N(s);moreover,by(ws),we obtain thatφM∪{u}∈N(s)orSφM∪{t}∈N(s).IfφM∪{u}∈N(s),then bySφM∈N(s)and(i),we derive that(φM∪{u})∩SφM∈N(s),i.e.,{u}∩SφM∈N(s),by induction hypothesis,{u}={u}∩SφM∈N(s),contrary tosRuand the definition ofR.IfSφM∪{t}∈N(s),similarly we can show that{t}∈N(s),contrary tosRtand the definition ofR.

    “=?:”Suppose thatto show thatthat is,there aret,u∈Ssuch thatsRt,sRuandM′,t?φandM′,u??φ.By supposition,φM/∈N(s).We show that there is at∈φMsuch that{t}/∈N(s)as follows:if not,i.e.,for allt∈φMwe have{t}∈N(s),then by(c),we getS{t}∈N(s),and using(i)we obtainviz.SφM∈N(s).9Since M is finite,we need only use the property that N is closed under finite intersections,which is equivalent to the property(i).This is unlike the case in Prop.12.Therefore using(c)again,we conclude thatφM∈N(s),which contradicts with the supposition.

    Therefore,there is at∈φMsuch that{t}/∈N(s).Sincet∈SandS∈N(s)(by(n)),by the definition ofR,it follows thatsRt;furthermore,fromt∈φMand induction hypothesis,it follows thatM′,t?φ.

    Similarly,we can show that there is au∈(?φ)Msuch that{u}/∈N(s).ThussRuandM′,u??φ,as desired. □

    In spite of Prop.12,as we shall see in Coro.5,logical consequence relations over Kripke semantics and over the new neighborhood semantics on quasi-filter models coincide with each other for CL.

    7 qf-Bisimulation

    This section proposes the notion of bisimulation for CL over quasi-filter models,called ‘qf-bisimulation’.The intuitive idea of the notion is similar to monotoniccbisimulation andc-bisimulation,i.e.the notion of precocongruences with particular properties(in the current setting,those four properties of quasi-filter models).

    Definition 12(qf-bisimulation)LetM=?S,N,V?andM′=?S′,N′,V′?be quasifilter models.A nonempty relationZ?S×S′is aqf-bisimulationbetweenMandM′,if for all(s,s′)∈Z,

    (qi)s∈V(p)iffs′∈V′(p)for allp∈Prop;

    (qii)if the pair(U,U′)isZ-coherent,thenU∈N(s)iffU′∈N′(s′).

    We say(M,s)and(M′,s′)areqf-bisimilar,writtenif there is a qf-bisimulationZbetweenMandM′such that(s,s′)∈Z.

    Note that the notion ofqf-bisimulation is defined between quasi-filter models.It is clear that every qf-bisimulation is ac-bisimulation,but it is not necessarily a monotonicc-bisimulation,since it is easy to find a quasi-filter model which is not closed under supersets.

    Analogous to the case forc-bisimulation in Sec.4,we can show that

    Proposition 14LetM,M′be both quasi-filter models,s∈M,s′∈M′.If(M,s)then for all

    Theorem 4(Hennessy-Milner Theorem for qf-bisimulation)LetMandM′be?-saturated quasi-filter models,ands∈M,s′∈M′.If for allφ∈L?,M,s?φ??

    We conclude this section with a comparison between the notion of qf-bisimulation and that of rel-?-bisimulation in[1,Def.6].

    Definition 13(rel-?-bisimulation) LetM=?S,R,V?andM′=?S′,R′,V′?be Kripke models.A nonempty relationZ?S×S′is arel-?-bisimulationbetweenMandM′,if for all(s,s′)∈Z,

    (Atoms)s∈V(p)iffs′∈V′(p)for allp∈Prop;

    (Coherence)if the pair(U,U′)isZ-coherent,then

    We say(M,s)and(M′,s′)arerel-?-bisimilar,writtenif there is a rel-?-bisimulationZbetweenMandM′such that(s,s′)∈Z.

    The result below asserts that every rel-?-bisimulation between Kripke models can be transformed to a qf-bisimulation between quasi-filter models.

    Proposition 15LetM=?S,R,V?andM′=?S′,R′,V′?be Kripke models.IfZis a rel-?-bisimulation betweenMandM′,thenZis a qf-bisimulation betweenqf(M)andqf(M′).

    ProofSupposeZisarel-?-bisimulation betweenMandM′.ByProp.11,qf(M)andqf(M′)are both quasi-filter models.It suffices to show thatZsatisfies the two conditions of a qf-bisimulation.For this,assume that(s,s′)∈Z.(qi)is clear from(Atoms).

    For(qii):let(U,U′)beZ-coherent.We have the following line of argumentation:U∈qfN(s)iff(by definition ofqfN)(R(s)?UorR(s)?SU)iff(by Coherence)(R′(s′)?U′orR′(s′)?S′U′)iff(by definition ofqfN′)U′∈qfN′(s′). □

    In the current stage,we do not know whether every qf-bisimulation between quasifilter models can be transformed to a rel-?-bisimulation between Kripke models.Note that this is important,since if it holds,then we can see clearly the essence of rel-?-bisimulation,i.e.precocongruences with those four quasi-filter properties.We leave it for future work.

    8 Frame definability

    Recall that under the old neighborhood semantics,all the ten neighborhood properties in Def.1are undefinable inL?.In contrast,under the new semantics,almost all these properties are definable in the same language.The following witnesses the properties and the corresponding formulas defining them.Recall that(c)is the minimal condition of neighborhood frames.

    Proposition16The right-hand formulas define the corresponding left-hand properties.

    ProofBy Prop.1,?p???pdefines(c).For other properties,we take(d)and(b)as examples,which resort to the property(c).Given anyc-frameF=?S,N?.

    Suppose thatFhas(d),to show thatF??p.Assume,for a contradiction that there is a valuationVonF,ands∈S,such thatwhereM=?F,V?.ThenpM∈N(s).On the one hand,by supposition,SpM/∈N(s);on the other hand,by(c),SpM∈N(s),contradiction.Conversely,assume thatFdoes not have(d),to show thatF???p.By assumption,there is anXsuch thatX∈N(s)andSX∈N(s).Define a valuationVonFsuch thatV(p)=X,and letM=?F,V?.ThuspM∈N(s),i.e.,M,s? ?p,and hence

    SupposeFhas(b),to showF?p→??p.For this,given anyM=?S,N,V?ands∈S,assume thatM,s?p,thens∈pM.By supposition,{u∈S|SpM/∈N(u)}∈N(s).By(c),this is equivalent to that{u∈S|pM/∈N(u)}∈N(s),i.e.,{u∈S|M,u??p}∈N(s),viz.,(?p)M∈N(s),thusM,s? ??p.Conversely,supposeFdoes not have(b),to showBy supposition,there is ans∈SandX?S,such thats∈Xand{u∈S|SX/∈N(u)}/∈N(s).Define a valuationVonFsuch thatV(p)=X,and letM=?F,V?.ThenM,s?p,and{u∈S|SpM/∈N(u)}/∈N(s).By(c)again,this means that{u∈S|pM/∈N(u)}/∈N(s),that is,{u∈S|M,u??p}/∈N(s),i.e.,(?p)M/∈N(s),thereforeM,s??p. □

    The following result will be used in the next section.

    Proposition 17?p→?(p→q)∨?(?p→r)defines the property(ws),where(ws)is as defined in Def.10.

    ProofLetF=?S,N?be a neighborhood frame.

    First supposeFhas(ws),we need to showF??p→?(p→q)∨?(?p→r).For this,assume for any modelMbased onFands∈SthatM,s??p.ThenpM∈N(s).By supposition,pM∪rM∈N(s)or(?p)M∪qM∈N(s).The former implies(?p→r)M∈N(s),thusM,s? ?(?p→r);the latter implies(p→q)M∈N(s),thusM,s? ?(p→q).Either case impliesM,s? ?(p→q)∨?(?p→r),henceM,s??p→?(p→q)∨?(?p→r).ThereforeF??p→?(p→q)∨?(?p→r).

    Conversely,supposeFdoes not have(ws),we need to showF?? ?p→?(p→q)∨?(?p→r).From the supposition,it follows that there areX,YandZsuch thatX∈N(s),X?YandY/∈N(s),SX?ZandZ/∈N(s).DefineVas a valuation onFsuch thatV(p)=X,V(q)=ZandV(r)=Y.SincepM=V(p)∈N(s),we haveM,s??p.SinceX?Y,(?p→r)M=X∪Y=Y/∈N(s),thusM,?(?p→r).SinceSX?Z,(p→q)M=(SX)∪Z=Z/∈N(s),and thusM,s?(p→q).HenceM,s?p→?(p→q)∨?(?p→r),and thereforeF?? ?p→?(p→q)∨?(?p→r). □

    Note that in the above proposition,we do not use the property(c),that is to say,it holds for the class of all neighborhood frames.

    9 Axiomatizations

    This section presents axiomatizations ofL?over various classes of frames.The minimal system E?consists of the following axiom schemas and inference rule.

    Note that E?is the same as CCL in[4,Def.7].Recall that(c)is the minimal neighborhood property.

    Theorem 5E?is sound and strongly complete with respect to the class ofc-frames.

    ProofImmediate by the soundness and strong completeness of E?w.r.t.the class of all neighborhood frames under?[4,Thm.1]and Coro.1. □

    Now consider the following extensions of E?,which are sound and strongly complete with respect to the corresponding frame classes.We omit the proof detail since it is straightforward.

    notation axioms systems frame classes?M ?(φ∧ψ)→?φ∧?ψ M?=E?+?M cs?C ?φ∧?ψ→?(φ∧ψ)R?=M?+?C csi

    One may ask the following question:is R?+??sound and strongly complete with respect to the class of filters,i.e.the frame classes possessing(s),(i),(n)?The answer is negative,since the soundness fails,although it is indeed sound and strongly complete with respect to the class of filters satisfying(c).

    Now consider the following axiomatization K?,which is provably equivalent to CL in[5,Def.4.1].

    Definition 14(Axiomatic system K?) The axiomatic system K?is the extension of E?plus the following axiom schemas:

    Theorem 6K?is sound and strongly complete with respect to the class of quasi-filter frames.

    ProofSoundness is immediate by frame definability results of the four axioms.

    For strong completeness,since every K?-consistent set is satisfiable in a Kripke model(cf.e.g.[5]),by Coro.4,every K?-consistent is satisfiable in a quasi-filter model,thus also satisfiable in a quasi-filter frame. □

    Note that the strong completeness of E?and of K?can be shown directly,by defining the canonical neighborhood functionNc(s)={|φ||?φ∈s}.

    As claimed at the end of Sec.6,for CL,although not every quasi-filter model has a pointwise equivalent Kripke model,logical consequence relations over Kripke semantics and over the new neighborhood semantics on quasi-filter models coincide with each other.Now we are ready to show this claim.

    Corollary 5The logical consequence relations?qfand?coincide for CL.That is,for all ?!葅φ}?L?,Γ ?qfφ??Γ?φ,where,by Γ ?qfφwe mean that,for every quasi-filter modelMandsinM,ifM,s? Γ,thenM,s?φ.Therefore,for allφ∈L?,?qfφ???φ,i.e.,the new semantics over quasi-filter models has the same logic(valid formulas)on CL as the Kripke semantics.

    ProofBy the soundness and strong completeness of K?with respect to the class of all Kripke frames(cf.e.g.[5]),Γ?K?φiff Γ ?φ.Then using Thm.6,we have that Γ ?qfφiff Γ ?φ. □

    10 Conclusion and Discussions

    In this paper,we proposed a new neighborhood semantics for contingency logic,which simplifies the original neighborhood semantics in[4]but keeps the logic the same.This new perspective enables us to define the notions of bisimulation for contingency logic over various model classes, one of which can help us understand the essence of nbh-Δ-bisimulation, and obtain the corresponding Hennessy-Milner Theorems, in a relatively easy way.Moreover,we showed that for this logic,almost all the ten neighborhood properties,which are undefinable under the old semantics,are definable under the new one.And we also had some simple results on axiomatizations.Besides,under the new semantics,contingency logic has the same expressive power as standard modal logic.It also gives us a neighborhood perspective that necessity is amount to non-contingency plus the property(c).We conjecture that our method may apply to other non-normal modal logics,such as logics of unknown truths and of false beliefs.We leave it for future work.

    Another future work would be axiomatizations of monotonic contingency logic and regular contingency logic under the old neighborhood semantics. Note that our axiomatizations M?and R?are not able to be transformed into the corresponding axiomatizations under the old semantics, since our underlying frames arec-frames.For example,although we do have?cs?(φ∧ψ)→?φ∧?ψ,we donothave?s?(φ∧ψ)→?φ∧?ψ;consequently,although M?is sound and strongly complete with respect to the class ofcs-frames under the new neighborhood semantics,it isnotsound with respect to the class ofs-frames under the old one.Thus the axiomatizations of these logics under the old neighborhood semantics are still open.10Update:These two open questions were raised in[1]and have been answered in[3].

    亚洲国产欧美日韩在线播放| 女性被躁到高潮视频| 国产精品嫩草影院av在线观看| 中文字幕免费在线视频6| 午夜福利,免费看| 成人免费观看视频高清| 一区在线观看完整版| 亚洲国产欧美在线一区| 老司机亚洲免费影院| 新久久久久国产一级毛片| 另类亚洲欧美激情| 天堂中文最新版在线下载| 美女主播在线视频| 青青草视频在线视频观看| 亚洲精品日本国产第一区| 亚洲av在线观看美女高潮| 18+在线观看网站| 亚洲国产精品一区二区三区在线| 亚洲伊人久久精品综合| 王馨瑶露胸无遮挡在线观看| 久久久久久人妻| 日韩成人伦理影院| 肉色欧美久久久久久久蜜桃| 日本vs欧美在线观看视频| 免费观看无遮挡的男女| 丝袜在线中文字幕| 在线精品无人区一区二区三| 国产极品天堂在线| 国产国拍精品亚洲av在线观看| 国产免费一区二区三区四区乱码| 亚洲av在线观看美女高潮| 亚洲精品美女久久av网站| 免费人妻精品一区二区三区视频| 搡老乐熟女国产| 欧美日韩av久久| 一级黄片播放器| 亚洲五月色婷婷综合| 国产精品久久久久久精品古装| 在线观看免费视频网站a站| 女人久久www免费人成看片| 超色免费av| 国产精品免费大片| 国产 精品1| 久久久久久久久久久丰满| 人人妻人人爽人人添夜夜欢视频| 如日韩欧美国产精品一区二区三区 | 亚洲第一区二区三区不卡| 国产熟女午夜一区二区三区 | 成人亚洲精品一区在线观看| 一级毛片 在线播放| 久久久久久久精品精品| 超碰97精品在线观看| 国产精品人妻久久久久久| 国产成人精品无人区| 最近最新中文字幕免费大全7| 男男h啪啪无遮挡| 亚洲人成网站在线播| 久久精品国产亚洲av涩爱| 国产黄频视频在线观看| 精品少妇久久久久久888优播| 人妻系列 视频| 考比视频在线观看| 婷婷色麻豆天堂久久| 日本猛色少妇xxxxx猛交久久| 在线 av 中文字幕| 少妇的逼水好多| 母亲3免费完整高清在线观看 | 久久久久久久久久久久大奶| 国产精品一区二区在线不卡| 亚洲五月色婷婷综合| 久热这里只有精品99| 午夜福利网站1000一区二区三区| 亚洲精品国产色婷婷电影| 久久久久精品性色| 少妇的逼水好多| 亚洲激情五月婷婷啪啪| 久久ye,这里只有精品| 女性被躁到高潮视频| 日本欧美视频一区| 天天躁夜夜躁狠狠久久av| 大码成人一级视频| 在线免费观看不下载黄p国产| 一级毛片aaaaaa免费看小| 亚洲av欧美aⅴ国产| 亚洲综合色网址| 99久久精品国产国产毛片| 亚洲第一av免费看| 中文天堂在线官网| 9色porny在线观看| 免费黄网站久久成人精品| 久久精品人人爽人人爽视色| 亚洲一级一片aⅴ在线观看| 性色avwww在线观看| 丁香六月天网| 日本黄大片高清| 国产精品免费大片| 久久精品久久久久久久性| 国产成人一区二区在线| 亚洲国产av新网站| a级毛片黄视频| h视频一区二区三区| 亚洲精品亚洲一区二区| 精品少妇久久久久久888优播| 国产欧美日韩一区二区三区在线 | 国产老妇伦熟女老妇高清| av专区在线播放| 日产精品乱码卡一卡2卡三| 9色porny在线观看| 精品亚洲乱码少妇综合久久| 中文天堂在线官网| 丰满迷人的少妇在线观看| 国产视频内射| 大陆偷拍与自拍| 成人国产av品久久久| 国产在线视频一区二区| 十分钟在线观看高清视频www| 亚洲欧美清纯卡通| 亚洲精品一二三| 欧美日韩在线观看h| 黄色怎么调成土黄色| 国产一级毛片在线| 亚洲av二区三区四区| 亚洲av.av天堂| 99久久精品国产国产毛片| 国产淫语在线视频| 男人操女人黄网站| 2021少妇久久久久久久久久久| 日韩精品免费视频一区二区三区 | 3wmmmm亚洲av在线观看| 亚洲四区av| 精品人妻在线不人妻| 国产黄频视频在线观看| 午夜老司机福利剧场| 国产日韩欧美在线精品| 22中文网久久字幕| 午夜福利视频精品| 天天影视国产精品| 在线观看免费日韩欧美大片 | 插逼视频在线观看| 亚洲国产精品一区三区| 午夜精品国产一区二区电影| 日本免费在线观看一区| 免费大片18禁| 涩涩av久久男人的天堂| 中文欧美无线码| 美女福利国产在线| 成人午夜精彩视频在线观看| 国产精品一国产av| 王馨瑶露胸无遮挡在线观看| 另类亚洲欧美激情| 日日撸夜夜添| 午夜激情福利司机影院| 成人亚洲欧美一区二区av| 午夜激情久久久久久久| 中文字幕亚洲精品专区| 天天操日日干夜夜撸| 夫妻午夜视频| 精品99又大又爽又粗少妇毛片| 精品国产露脸久久av麻豆| 精品久久久久久久久av| 女的被弄到高潮叫床怎么办| 伊人亚洲综合成人网| 成人漫画全彩无遮挡| 纯流量卡能插随身wifi吗| 伦理电影大哥的女人| 日韩中文字幕视频在线看片| 欧美成人精品欧美一级黄| 久久久久久久久久人人人人人人| 一级毛片电影观看| 中文字幕人妻熟人妻熟丝袜美| 交换朋友夫妻互换小说| 精品少妇内射三级| 精品视频人人做人人爽| 国产黄频视频在线观看| 成年人午夜在线观看视频| 国产伦理片在线播放av一区| 18禁裸乳无遮挡动漫免费视频| 在线免费观看不下载黄p国产| 大香蕉久久网| 午夜久久久在线观看| 啦啦啦啦在线视频资源| 国产成人精品无人区| 中国国产av一级| 亚洲美女搞黄在线观看| 国产永久视频网站| 一区二区三区免费毛片| 精品久久久噜噜| 亚洲av国产av综合av卡| 一本久久精品| 一个人看视频在线观看www免费| 99久久中文字幕三级久久日本| 最近2019中文字幕mv第一页| 国产av精品麻豆| 国国产精品蜜臀av免费| 国产在线一区二区三区精| 午夜福利网站1000一区二区三区| 日日摸夜夜添夜夜爱| 午夜影院在线不卡| 成年美女黄网站色视频大全免费 | 欧美精品高潮呻吟av久久| 国产日韩欧美亚洲二区| 国产白丝娇喘喷水9色精品| 日韩伦理黄色片| 国精品久久久久久国模美| av黄色大香蕉| 亚洲欧美精品自产自拍| 国国产精品蜜臀av免费| 超碰97精品在线观看| 久久av网站| 69精品国产乱码久久久| 久久国产亚洲av麻豆专区| 国产精品久久久久久精品古装| 成年人免费黄色播放视频| 久久久久精品久久久久真实原创| 国产av国产精品国产| 久久精品国产亚洲av天美| 高清午夜精品一区二区三区| 亚洲怡红院男人天堂| 国产av国产精品国产| 性色av一级| 国产午夜精品一二区理论片| 日本免费在线观看一区| 精品国产乱码久久久久久小说| 久久午夜综合久久蜜桃| 简卡轻食公司| 又黄又爽又刺激的免费视频.| 一级毛片黄色毛片免费观看视频| 亚洲欧美成人综合另类久久久| 黄色毛片三级朝国网站| 免费黄网站久久成人精品| 亚洲经典国产精华液单| 人人妻人人澡人人看| 亚洲高清免费不卡视频| 国产乱人偷精品视频| 99精国产麻豆久久婷婷| 美女国产视频在线观看| videossex国产| 精品人妻一区二区三区麻豆| 免费观看av网站的网址| 少妇人妻久久综合中文| 国产视频内射| 天天操日日干夜夜撸| 国产成人a∨麻豆精品| 精品一品国产午夜福利视频| 成人国语在线视频| 中文字幕制服av| 亚洲精品aⅴ在线观看| 久久 成人 亚洲| av视频免费观看在线观看| 久久精品国产自在天天线| 亚洲欧美中文字幕日韩二区| 在线天堂最新版资源| 校园人妻丝袜中文字幕| 18+在线观看网站| 一本色道久久久久久精品综合| 日韩一区二区三区影片| 久久热精品热| 大香蕉97超碰在线| 国产高清不卡午夜福利| 在线观看免费高清a一片| 久久久欧美国产精品| 我的女老师完整版在线观看| 飞空精品影院首页| 日产精品乱码卡一卡2卡三| 亚洲四区av| 女性生殖器流出的白浆| 国产成人av激情在线播放 | 日韩中字成人| a级毛色黄片| 亚洲av日韩在线播放| 国产免费视频播放在线视频| 尾随美女入室| 丰满乱子伦码专区| 国产淫语在线视频| 国产男人的电影天堂91| 中文字幕人妻熟人妻熟丝袜美| 亚洲色图 男人天堂 中文字幕 | 国产精品久久久久久久久免| 一区二区三区精品91| 老司机亚洲免费影院| 人人妻人人澡人人爽人人夜夜| 搡老乐熟女国产| 亚洲三级黄色毛片| 一本—道久久a久久精品蜜桃钙片| 婷婷成人精品国产| 18在线观看网站| 亚洲四区av| 国产精品一区二区在线观看99| 国产精品女同一区二区软件| 18+在线观看网站| 中文精品一卡2卡3卡4更新| 亚洲不卡免费看| 中文欧美无线码| 狂野欧美激情性bbbbbb| 成人毛片a级毛片在线播放| videossex国产| 精品少妇黑人巨大在线播放| 成人漫画全彩无遮挡| h视频一区二区三区| 97超视频在线观看视频| 97在线人人人人妻| 99热网站在线观看| 国产深夜福利视频在线观看| 26uuu在线亚洲综合色| 麻豆乱淫一区二区| 汤姆久久久久久久影院中文字幕| 亚洲欧美一区二区三区国产| 两个人的视频大全免费| 精品一区二区三区视频在线| 两个人的视频大全免费| 热99国产精品久久久久久7| 久久精品人人爽人人爽视色| 久久韩国三级中文字幕| 国产在线免费精品| av国产精品久久久久影院| 免费看不卡的av| 国产男女内射视频| 久久精品熟女亚洲av麻豆精品| 亚洲不卡免费看| tube8黄色片| 九色成人免费人妻av| 制服丝袜香蕉在线| 国产永久视频网站| 国产女主播在线喷水免费视频网站| 欧美亚洲 丝袜 人妻 在线| 桃花免费在线播放| 人人澡人人妻人| 国产精品熟女久久久久浪| 少妇 在线观看| 中文精品一卡2卡3卡4更新| 亚洲,欧美,日韩| 午夜福利在线观看免费完整高清在| 蜜臀久久99精品久久宅男| 亚洲内射少妇av| 国产精品久久久久久精品电影小说| 中文字幕人妻熟人妻熟丝袜美| 亚洲经典国产精华液单| 欧美日韩视频精品一区| 欧美国产精品一级二级三级| 久久久久网色| 久久狼人影院| 亚洲欧美一区二区三区黑人 | 亚洲精品日韩av片在线观看| 美女xxoo啪啪120秒动态图| 狂野欧美激情性bbbbbb| 成年女人在线观看亚洲视频| 久久人妻熟女aⅴ| 精品久久久久久电影网| 综合色丁香网| 国产日韩欧美视频二区| 亚洲欧美成人精品一区二区| a级毛片在线看网站| 有码 亚洲区| 亚洲国产精品成人久久小说| 午夜视频国产福利| 日韩一本色道免费dvd| 免费av中文字幕在线| 老司机亚洲免费影院| 国产成人精品一,二区| 久久女婷五月综合色啪小说| 99热网站在线观看| 国模一区二区三区四区视频| 国产乱人偷精品视频| 精品国产一区二区三区久久久樱花| 亚洲欧洲国产日韩| 男男h啪啪无遮挡| 亚洲精品456在线播放app| 国产精品99久久久久久久久| 国产精品一国产av| 极品人妻少妇av视频| 一区二区三区免费毛片| 另类亚洲欧美激情| 亚洲怡红院男人天堂| 狂野欧美激情性bbbbbb| 老司机影院毛片| 青春草亚洲视频在线观看| av在线老鸭窝| 国产精品一国产av| 男人爽女人下面视频在线观看| 亚洲精品美女久久av网站| 五月玫瑰六月丁香| 91精品国产九色| 人成视频在线观看免费观看| 一二三四中文在线观看免费高清| 免费人成在线观看视频色| 国产国语露脸激情在线看| 亚洲欧美日韩另类电影网站| 免费高清在线观看日韩| 亚洲av电影在线观看一区二区三区| 涩涩av久久男人的天堂| 黄片无遮挡物在线观看| 我要看黄色一级片免费的| 亚洲在久久综合| 2018国产大陆天天弄谢| 亚洲精品乱码久久久v下载方式| 久久久亚洲精品成人影院| 精品国产国语对白av| 熟女av电影| 一级毛片 在线播放| a级毛色黄片| 亚洲欧美精品自产自拍| 精品少妇久久久久久888优播| 免费人成在线观看视频色| 性少妇av在线| 黄网站色视频无遮挡免费观看| 久久人妻熟女aⅴ| 国产99久久九九免费精品| 久久精品熟女亚洲av麻豆精品| 国产欧美日韩综合在线一区二区| 97人妻天天添夜夜摸| 俄罗斯特黄特色一大片| 午夜免费鲁丝| 成年动漫av网址| 菩萨蛮人人尽说江南好唐韦庄| 建设人人有责人人尽责人人享有的| 亚洲av第一区精品v没综合| 99国产精品99久久久久| 人妻一区二区av| 久久久精品94久久精品| 91成人精品电影| 欧美日韩福利视频一区二区| 一级a爱视频在线免费观看| 久久人妻熟女aⅴ| 丝袜美足系列| 国产在线视频一区二区| 久久ye,这里只有精品| 国产在线观看jvid| 18禁黄网站禁片午夜丰满| 亚洲三区欧美一区| 久久久久久久精品吃奶| 99久久99久久久精品蜜桃| 91精品三级在线观看| 色尼玛亚洲综合影院| 欧美精品高潮呻吟av久久| 日本vs欧美在线观看视频| av线在线观看网站| 视频区图区小说| 丝瓜视频免费看黄片| 久久久国产成人免费| 久热爱精品视频在线9| 日本黄色日本黄色录像| 免费不卡黄色视频| 国产成人免费无遮挡视频| 91字幕亚洲| 国产伦人伦偷精品视频| 国产aⅴ精品一区二区三区波| 日韩制服丝袜自拍偷拍| 最近最新免费中文字幕在线| 日日摸夜夜添夜夜添小说| 精品人妻在线不人妻| 后天国语完整版免费观看| 久久精品国产综合久久久| 欧美老熟妇乱子伦牲交| 操美女的视频在线观看| 亚洲成人免费电影在线观看| 午夜福利在线免费观看网站| 美女扒开内裤让男人捅视频| 国产无遮挡羞羞视频在线观看| 国产精品一区二区在线观看99| www.精华液| 欧美亚洲日本最大视频资源| 老熟女久久久| 国产一区二区激情短视频| 午夜久久久在线观看| 三上悠亚av全集在线观看| 欧美在线一区亚洲| 美女福利国产在线| 在线观看免费视频网站a站| 一进一出抽搐动态| 久热爱精品视频在线9| 国内毛片毛片毛片毛片毛片| 正在播放国产对白刺激| 新久久久久国产一级毛片| 在线观看免费日韩欧美大片| 两性午夜刺激爽爽歪歪视频在线观看 | 欧美国产精品一级二级三级| 每晚都被弄得嗷嗷叫到高潮| 欧美在线一区亚洲| 美女福利国产在线| 欧美老熟妇乱子伦牲交| 成人国语在线视频| 亚洲中文字幕日韩| 免费女性裸体啪啪无遮挡网站| 一级毛片精品| 国产精品国产av在线观看| e午夜精品久久久久久久| 精品少妇一区二区三区视频日本电影| 精品久久久久久久毛片微露脸| 国产高清videossex| 久久人人97超碰香蕉20202| 啪啪无遮挡十八禁网站| 精品高清国产在线一区| 国产不卡av网站在线观看| 两人在一起打扑克的视频| 免费在线观看影片大全网站| 人成视频在线观看免费观看| 91九色精品人成在线观看| 国产精品二区激情视频| 国产成人啪精品午夜网站| 国产亚洲精品第一综合不卡| 人人妻人人澡人人看| 一边摸一边做爽爽视频免费| 肉色欧美久久久久久久蜜桃| 日本av手机在线免费观看| 精品一品国产午夜福利视频| 夜夜夜夜夜久久久久| 12—13女人毛片做爰片一| 国产精品 国内视频| 久久精品亚洲熟妇少妇任你| 9191精品国产免费久久| 国产日韩一区二区三区精品不卡| 一本大道久久a久久精品| 十八禁网站免费在线| 多毛熟女@视频| 亚洲成人免费av在线播放| 最黄视频免费看| 欧美成人午夜精品| 欧美精品一区二区大全| 久久精品国产综合久久久| 一二三四社区在线视频社区8| 多毛熟女@视频| 欧美在线黄色| 精品国产乱码久久久久久小说| 少妇 在线观看| 久久精品国产亚洲av高清一级| 色综合婷婷激情| 十八禁网站免费在线| 最新美女视频免费是黄的| 国产精品久久久人人做人人爽| 两人在一起打扑克的视频| 日韩免费av在线播放| 两性夫妻黄色片| 国产精品免费视频内射| 亚洲七黄色美女视频| 精品国产国语对白av| 一本一本久久a久久精品综合妖精| 成人18禁在线播放| 国产xxxxx性猛交| e午夜精品久久久久久久| 好男人电影高清在线观看| 男人操女人黄网站| 国产亚洲av高清不卡| 51午夜福利影视在线观看| 9191精品国产免费久久| 日韩熟女老妇一区二区性免费视频| 两个人看的免费小视频| av视频免费观看在线观看| 国产亚洲欧美精品永久| 涩涩av久久男人的天堂| 国产极品粉嫩免费观看在线| 亚洲熟女毛片儿| 久久天躁狠狠躁夜夜2o2o| 中文字幕精品免费在线观看视频| 老司机影院毛片| 99久久99久久久精品蜜桃| 亚洲av电影在线进入| 黄色毛片三级朝国网站| 精品少妇黑人巨大在线播放| 国产精品一区二区免费欧美| av视频免费观看在线观看| 多毛熟女@视频| avwww免费| 首页视频小说图片口味搜索| 成人国产一区最新在线观看| 欧美日韩视频精品一区| 国产亚洲一区二区精品| 久久免费观看电影| 老司机在亚洲福利影院| 久久人妻熟女aⅴ| 高清欧美精品videossex| 黄色视频,在线免费观看| netflix在线观看网站| 一个人免费在线观看的高清视频| 久久 成人 亚洲| 国产在线免费精品| 一区二区三区国产精品乱码| 女人久久www免费人成看片| 国产免费视频播放在线视频| 捣出白浆h1v1| 美女福利国产在线| 五月开心婷婷网| 黄色毛片三级朝国网站| 美女高潮到喷水免费观看| 日日夜夜操网爽| 久久久水蜜桃国产精品网| 啦啦啦在线免费观看视频4| 国产在线视频一区二区| 免费在线观看日本一区| 精品人妻熟女毛片av久久网站| 精品国产乱子伦一区二区三区| 久久中文看片网| 9色porny在线观看| 午夜福利,免费看| 淫妇啪啪啪对白视频| 亚洲精品美女久久久久99蜜臀| 啦啦啦中文免费视频观看日本| www.999成人在线观看| 国精品久久久久久国模美| 国产三级黄色录像| 少妇猛男粗大的猛烈进出视频| 国产精品.久久久| 亚洲欧美一区二区三区久久| 精品久久久久久久毛片微露脸| netflix在线观看网站| 叶爱在线成人免费视频播放| 无限看片的www在线观看| 性色av乱码一区二区三区2| 成年人午夜在线观看视频| 日韩人妻精品一区2区三区| 亚洲欧美日韩另类电影网站| 嫁个100分男人电影在线观看| 丰满饥渴人妻一区二区三| 亚洲一卡2卡3卡4卡5卡精品中文| 伊人久久大香线蕉亚洲五| 亚洲精品乱久久久久久|