逻辑、计算和博弈 (18).pdf
|5 TABLE OF CONTENTS Preface Introduction 1 A whirlwind history,and changes in perspective Core Concepts 2 Basic language and semantics 3 Expressive power and invariance 4 Validity and decidability 5 Axioms,proofs,and completeness 6 Computation and complexity Basic Theory 7 Classical translation and expressive power 8 Increasing deductive power:the landscape of modal logics 9 What axioms say:frame correspondence 10 Descriptive power:extended modal languages 11 The next level:modal predicate logic Selected applications 12 Epistemic logic 13 Doxastic and conditional logic 14 Dynamic logic of action 15 Dynamic logic of information 16 Preference and deontic logic 17 Modal logic and games 18 The structure and flow of time 19 Modal patterns in space 20 Intuitionistic logic 21 Provability logic Recent theoretical themes 22 Fixed-points,computation,and equilibrium 23 Issues in information dynamics 24 System combination and undecidability 219 CHAPTER 19 MODAL PATTERNS IN SPACE 19.1 Spatial structures When thinking about the physical world,logicians have taken Time as their main interest,because it fits so well with flow of information and computation.Spatial logics have been more marginal even though historically,the axiomatic method was largely geometrical.An exception is Tarskis work on new geometrical primitives for space,and his famous decidable first-order axiomatization of elementary geometry.Today Space remains intriguing in many disciplines,and you can get a good impression of the whole field of spatial reasoning by looking at the Handbook of Spatial Logics,Springer,Dordrecht,2007.In this chapter,we just look at a few patterns from a modal perspective.Even then,Space can be studied at many levels,depending on ones interest,that come with their own mathematical transformations.You must first choose some level of structure(topological,affine,metric)providing its invariances(homeomorphism,affine transformations,etc.).At each of these,a logician will then try to design some language that brings out interesting laws,preferably in a calculus of some reasonable complexity.19.2 Modal logic and topology Let M be a topological space(X,O,V)with points X,a family of open sets O,and a valuation V as in modal models.Now we can interpret the modal language as follows:Definition Topological semantics.?is true at point s in M,written M,s|=?,if s is in the topological interior of M:the set of points satisfying in M.Formally,OO:sO&tO:M,t|=.177 Dually,the existential modality?will then denote a topological closure operator.Typical examples of topologies are metric spaces like the real line,or the real plane,etcetera.Please try to think of this semantics then as concretely as you can in visual terms:177 This recalls the neighbourhood models of Chapter 10:we elaborate on this connection below.220 Example Defining parts of spoons.Let the proposition letter p denote the following spoon in IR2.We explain the topological regions defined by various other modal formulas(note that these need not be open):p?p?p?p?p p?p?p?p)?p You see how modal formulas of various operator depths define the interior,the boundary,the handle,and even the special point connecting the handle to the main oval part.This interpretation is attractive because the following Fact The modal axioms of S4 express the following topological properties:?expresses inclusion,?expresses idempotence,?()?expresses closure of open sets under intersections.There is no modal analogue of closure of open sets under arbitrary unions,given the finite nature of the language,but we do have this derivable principle in the logic S4:?(?)More generally,one can prove the following general completeness result:Theorem A modal formula is topologically valid iff it is provable in S4.The proof is a bit disappointing.Soundness is seen by direct inspection,as we just did.For completeness,one just finds an S4-style possible worlds model for a consistent formula,where the order is reflexive and transitive.Now,any such model generates a topology:Fact Each pre-order induces a topology,where topological modal evaluation amounts to standard modal evaluation on relational models.221 Proof sketch The open sets in the topology are all subsets of the model that are closed under taking successors.In particular,an open basis is given by all upward cones of the form s=(tW|st.It is easy to see that,with this transformation,truth throughout some open neighbourhood of a world is equivalent to truth in all its relational successors.Structures of this special sort are called Alexandroff topologies:they have the special feature that arbitrary intersections of open sets are open,not just finite ones.Our modal models are such topologies and vice versa,and this analogy can be made quite precise.For instance,in an infinitary modal language,we have a matching unrestricted distribution law?iI i iI?i But the most central spaces in topology come from the earlier metric spaces,so the interest of our current setting is precisely how modal logic behaves on that unfamiliar territory.Example Unlimited distribution fails on metric spaces.Interpret the proposition letter pi as the open interval(1/i,+1/i),for all iN.Then the formulas?pi denote the same interval,and hence their intersections are the intersection of all these intervals,i.e.,0.But the expression?iI pi denotes the topological interior of the singleton set 0,which is the empty set.There are indeed two major families of topologies:metric spaces,and tree-like ones.The following point is overlooked by people who think life started in the 1950s.Historically,the first semantic interpretation for modal languages was in terms of the former,by Tarski in the 1930s,and the standard relational semantics in the 1950s then switched to tree-like models.Only nowadays,broader topological models are picking up interest again.19.3 Special topics:invariance,expressive and deductive power All the earlier topics from general modal logic return with new twists here.Comparison games One can analyze the expressive power of our modal language with games between Spoiler and Duplicator,comparing points in two topological models:222 Definition Topo-games.Rounds proceed as follows,starting from some current match s t.Spoiler takes one of these points,and chooses an open neighbourhood U in its model.Duplicator responds with an open neighbourhood V of the other current point.Still in the same round,Spoiler chooses a point vV,and then Duplicator chooses a point uU,making u v the new match.Duplicator loses if the two points differ qua atomic properties.This looks abstract,but it is concrete.Here are some illustrations.Example Comparing points on spoons.In the above spoons,compare the following sets of intuitively different points:(a)(b)(c)For a start,here is a useful auxiliary result.It does not matter if players choose small or large open neighbourhoods in the game.You can see this by trying a few moves,but there is also a general result,which is like the earlier fact that on relational models,evaluation of formulas only needs to look at Rclosed generated submodels around the current point:Fact(Locality Lemma)For any model M,s and modal formula,and any open neighbourhood O of s,the following are equivalent:(a)M,s|=,and (b)M|O,s|=,where M|O is the model M restricted to the subset O.This Fact is easy to prove by induction on modal formulas.Now we consider games for the above three situations,where the black lines indicate the initial match between points.178 For vividness,the description will be stated largely from 178 Note that we are comparing points in figures,not figures as a whole.To do the latter,we would have to change the game slightly,and let Spoiler first mark two points that he wants to play from.223 the perspective of Spoiler,since we have chosen cases where there is a topologically significant difference.If you want to see a case where Duplicator has a winning strategy,look at some subgames described in what follows or just let the game start with two points in the interior of the spoon:whatever Spoiler does,Duplicator serenely tags along.Case(a).If Spoiler chooses a neighbourhood to the left,then Duplicator chooses a small interior disk to the right,and whatever Spoiler chooses,there it will be an inside point which duplicator can match in the open to the left.So,this is a bad idea.If Spoiler starts with a small disk on the right,however,then Duplicator must respond with a disk on the edge to the left,which then allows Spoiler to choose an object outside of the spoon,and every response by Duplicator is losing,since it must be inside the spoon.So,Spoiler has a winning strategy in one round.This is reflected in the earlier observation that there is a modal difference formula of operator depth 1 distinguishing the two positions say?p.Case(b).Spoilers winning strategy starts with an open on the handle to the left,where Duplicator must choose an open on the rim of the oval.Now Spoiler chooses an object there inside the spoon,and Duplicator can only respond by either choosing outside of the spoon(an immediate loss),or on the handle.But the latter reduces the game to case(a),which Spoiler could win in one round.The difference formula this time has modal depth 2.Case(c)is the most complicated one,since the special point connecting rim and handle is most like an ordinary rim point,but Spoiler has a winning strategy in 3 rounds,matching a modal difference formula of modal depth 3,for instance,?p?p)?p.Again,one can easily prove an Adequacy result:Fact Duplicator has a winning strategy in the comparison game over k rounds starting from two models M,s and N,t iff these two pointed models satisfy the same modal formulas up to modal operator depth k.The proof is similar to that for relational models in Chapter 3:you might give it a try.Topo-bisimulation Here is the matching relation for topological spaces plus valuations:224 Definition Topo-bisimulation.A topo-bisimulation is a relation E between points in two models M,M connecting only points verifying the same proposition letters,and satisfying the zigzag clauses (a)Whenever s E t and sUO,then there exists an open V with (a1)tVO and(a2)vV uU:u E v.(b)The same vice versa.179 These zigzag clauses are reminiscent of the definition of a continuous open function in topology,which says that both images and inverse images of open sets are open.Topo-bisimulation may be viewed a coarse variant of topological homeomorphism.Obviously,topo-bisimulations leave the modal language invariant,and even its infinitary extension with arbitrary set conjunctions and disjunctions.The proof is a simple induction.In this setting,it is of interest to also consider the logical transfer behaviour of continuous maps,beloved by topologists.A continuous map is a function that has all its inverse images of open sets open and typically,it preserves basic properties of topological spaces like Compactness:each open cover of the space contains a finite sub-cover.Which properties precisely?Consider a continuous map from a topological space M onto a space N.Any valuation V on N can be copied back to M via f1V.Once we do that,the relation between points x in M and f(x)in N is half a topo-bisimulation with just the backward zigzag clause:take the required U to be the open set f1V.An easy induction shows that Fact Continuous maps with their induced valuations preserve,going from N to M,all modal formulas created by the following syntax:p|p|?Extended modal languages But actually,something more is true,using the further feature that functions are defined throughout their domains M,while continuous functions are even surjective,ranging across the whole domain of the model N.The inductive syntax for preserved statements in the preceding Fact can then also include two operators studied in Chapter 7,viz.the universal modality U and the existential modality E.Looking in the 179 This is similar to the earlier bisimulations for neighbourhood models in Chapter 10.225 opposite direction then,we can see what continuous maps preserve,taking negations.And the explanation of the transfer of Compactness is now simply this:it has the syntactic form U iI?i J finite I:U jJ?j whose negation is of the form described,in an obvious infinitary version.Such extended languages also make sense for defining topological notions beyond the expressive power of the basic language.Here is an illustration.A topological space is called connected if it cannot be written as a disjoint union of two non-empty open sets.A simple topo-bisimulation argument shows that this is not definable in our basic language.But we can show that an extended language does,via a correspondence argument.Example Connectedness.The following formula holds in a topological space for all valuations(in the frame sense)if and only if that space is connected:(U(?p?q)Ep Eq)E(p q).Special completeness theorems Another interesting topic is the earlier deductive power and completeness of modal logics for topological structures.Here is a famous result by McKinsey&Tarski in the 1940s:it shows that S4 is not just adequate for tree topologies,but also,so to speak,for the opposite side of topology:Theorem The modal logic of any metric space without isolated points equals S4.The proof for this result is difficult,and simplifications and variants are still generating new research.This result may seem to show how little the modal language can say about topological structures:not even a very rich metric space like the reals can elicit more music from the modal language than S4.But in another sense,by its very weakness,the completeness gives attractive concrete connections between the modal language and spatial patterns.For,it follows that any consistent modal formula in reflexive transitive S4-models can be made true by choosing a suitable valuation on the reals.This is non-trivial:Example Satisfying consistent formulas on the reals.Consider this tree,where the numbers stand for unique proposition letters true at the nodes:226 p q r s t Remember that this a reflexive transitive S4-model(we have omitted some arrows for convenience),so for instance,formulas true at end points are necessarily true there.We can make p true at some real number.Now the fact that it sees a q-world means that our chosen p-world is in the closure of the set of q-worlds,meaning that there must be a convergent sequence of q-worlds toward it.In fact,we see a?q-world(it is an endpoint),so we see a convergent sequence of open qintervals toward the initial point.Analyzing the successor node with r,we have to put another convergent sequence,this time of rpoints which themselves have converging sequences of open s and tintervals around them.This can quickly get very complicated,and indeed,the whole procedure for satisfying consistent statements on S4-trees involve fractal-like nested geometrical duplications.Stronger logics than S4 arise with more special structures.For instance,suppose we do not want all se
