逻辑、计算和博弈 (27).pdf

《逻辑、计算和博弈 (27).pdf》由会员分享，可在线阅读，更多相关《逻辑、计算和博弈 (27).pdf（83页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、“lig-09-25”2013/10/29 9:44 page 315#333iiiiiiiiIntroduction to Part IVThis is a turning point where this book changes both content and style.PartsI,II,and III have completed our general analysis of games and play in a logicalstyle.But,as we have seen in the Introduction,while logic can be applied to

2、anything,in the case of games,there is a more intimate connection.Many basiclogical notions can themselves be cast in the form of games.We now proceed toexplore this perspective of logic as games versus the earlier logic of games.In thispart,we survey some basic logic games for evaluating formulas,c

3、omparing models,constructing models,and carrying on dialogue.Many logicians use these gamessolely as didactic tools;and indeed,they are powerful for this purpose,since gameintuitions pack a lot of complex structure into something easily imagined.But thereis more to it.Logic games contain lots of gen

4、eral ideas and themes with a broaderthrust,as will become clear in the coming chapters,while we will also discusssome broader themes explicitly in the concluding Chapter 18.In particular,in anappendix to that chapter,we provide a window onto some related work on gamesin computational logic,where a f

5、lourishing theory has emerged in recent years.Ourgeneral themes will then be taken further in Parts V and VI of this book,wherethe latter also closes the circle with the game logics of Parts I,II and III.A note on sources The material in this part comes largely from my lecture notes,Logic in Games(v

6、an Benthem 1999),that have circulated until now in severalprinted and electronic versions.A compact compendium is given in van Benthem(2011c),while an excellent regularly updated survey can be found in Hodges(2001).The educational origin of much of the coming material shows in the style of thechapte

7、rs.Even without the grand design of this book,the reader might appreciatewhat follows as an unusual tour of basic logic.“lig-09-25”2013/10/29 9:44 page 317#335iiiiiiii14Formula EvaluationLogical languages usually have a model-theoretic semantics defining when a formula is true in a model M,perhaps w

8、ith an auxiliary setting.The paradigm is first-order logic,with its notion M,s|=where s is an assignment of objects in M tovariables.Now,stepwise evaluation of first-order assertions can be cast dynamicallyas a game of evaluation for two players.“Verifier”claims that is true in the settingM,s,“falsi

9、fier”that it is false.This is our most basic logic game.In this chapterwe explain first-order evaluation games,establish their adequacy with respect totruth and falsity,explore their more general game-theoretic character,demonstratehow other logics can be gamified in the same style,and identify some

10、 general issuesof game logic behind first-order games,including the role of players strategies andgame operations.16914.1Evaluation games for predicate logicTwo parties disagree about a proposition in some situation M,s:verifier Vclaims that it is true,falsifier F that it is false.Here are the natur

11、al moves of defenseand attack in the first-order evaluation game,that we will indicate henceforth asgame(,M,s).Definition 14.1Moves in evaluation gamesThe moves of evaluation games follow the inductive construction of formulas.They169 Games like this occur in Hintikka(1973).Since then,evaluation gam

12、es have beengiven for many logics.Hintikka&Sandu(1997)has a game-theoretical semantics fornatural language,and Chapter 21 will pursue the resulting independence-friendly logic.“lig-09-25”2013/10/29 9:44 page 318#336iiiiiiii318Logic Gamesinvolve typical notions in the dynamics of games,such as choice

13、,switch,andcontinuation,in dual pairs with both players allowed the initiative once:atoms Pd,Rde,.V wins if the atom is true,F if it is falsedisjunction _ V chooses which disjunct to playconjunction F chooses which conjunct to playnegation role switch between the two players,play continues with resp

14、ect to Next,the quantifiers make players look inside Ms domain of objects:existential 9x(x)V picks an object d,play continues with(d)universal 8x(x)the same move,but now for FHere the clause for atoms may look circular,but one might think of it as theplayers consulting the model to see whether it su

15、pports such a bottom-level state-ment.As for complex structure,the schedule of the game is determined by the formof the statement.Example 14.1Formulas and schedule of playTo see how this works,consider a model M with two objects s,t.Here is a gamefor 8x9y x6=y,pictured as a tree of moves,with the sc

16、heduling from top to bottom:y:=sy:=tx:=sy:=sy:=tx:=tFVVloseVwinVwinVloseVWe interpret this as a game of perfect information:players know throughout whathas happened.Falsifier starts,and verifier must respond.There are four possibleplays,with two wins for each player.But verifier has a winning strate

17、gy,in thestandard sense of our earlier chapters.Trees such as this are not a complete definition of the game yet,but for manypurposes,we are better o without further detail.Evaluation games for slightlymore complex formulas in richer models have proved attractive in teaching logic.“lig-09-25”2013/10

18、/29 9:44 page 319#337iiiiiiiiFormula Evaluation319Example 14.2Find noncommunicatorsConsider the following communication network with arrows for directed links,andwith all self-loops present but suppressed in the drawing:45123The formula 8x8y(Rxy _ 9z(RxzRzy)says that every two nodes in this networkc

19、an communicate in at most two steps.Here is a run of the evaluation game:playermovenext formulaFpicks 28y(R2y _ 9z(R2z Rzy)Fpicks 1R21 _ 9z(R2z Rz1)Vchooses9z(R2z Rz1)Vpicks 4R24 R41FchoosesR41testF losesFalsifier started with a threat by picking object 2,but then picked 1.Verifier chosethe true rig

20、ht conjunct,and picked the witness 4.Now,falsifier loses with eitherchoice.Still,falsifier could have won,by choosing object 3 that 2 cannot reach in2 steps.Falsifier even has another winning strategy,namely,x=5,y=4.In this way,each formula is a game form of fixed depth but indefinite branchingwidth

21、,with a schedule of turns and moves.It becomes a real game when a modelM is given that supplies possible quantifier moves and outcomes for atomic tests,while an assignment s to the free variables in sets the initial position of the game.14.2Truth and winning strategies of verifierIn our first exampl

22、e,participants were not evenly matched.Player V can alwayswin:after all,a verifier is in line with the truth of the matter.More precisely,Vhas a winning strategy,a map from V s turns to moves following which guarantees,“lig-09-25”2013/10/29 9:44 page 320#338iiiiiiii320Logic Gamesagainst any play by

23、F,that the game ends in outcomes where V wins.F has nowinning strategy,as this would contradict V s having one.170Even more can besaid.F does not have a losing strategy either:F cannot force V to win,but in ourexample,player V does have a losing strategy.Thus,players powers of controllingoutcomes in

24、 a game may be quite dierent.Here is the key to the behavior of evaluation games,the“success lemma.”Fact 14.1The following are equivalent for all models M,s and formulas:(a)M,s|=,(b)V has a winning strategy in game(,M,s).Proof The proof is a direct induction on formulas.One shows simultaneously:If a

25、 formula is true in(M,s),then verifier has a winning strategy.If a formula is false in(M,s),then falsifier has a winning strategy.The steps show the close analogy between logical operators and ways of combiningstrategies.171The following typical cases will give the idea.(a)If _ is true,thenat least

26、one of or is true,say,.By the inductive hypothesis,V has a winningstrategy?for.But then V has a winning strategy for the game _ :the firstmove is left,after which the rest is the strategy?.(b)If _ is false,both and are false,and so by the inductive hypothesis,F has winning strategies?and for and ,re

27、spectively.But then the combination of an initial wait-and-see stepplus these two is a winning strategy for F in the game _ .If V goes left in thefirst move,then F should play?,while,if V goes right,F should play strategy.(c)If the formula is a negation we use a role switch.Example 14.3Role SwitchCo

28、nsider the game for a formula p _ q in a model where p is true and q is false,aswell as its dual game(p _ q),that switches all turns and win markings:p _ qVwinVwinF(p _ q)FwinFwinV170 Playing two winning strategies against each other yields a contradiction at the end.171 This inductive proof is virt

29、ually the argument for Zermelos Theorem in Chapter 1.“lig-09-25”2013/10/29 9:44 page 321#339iiiiiiiiFormula Evaluation321The second game works out to that for the De Morgan equivalent p q.Thus,strategies for V in a game for are strategies for F in the game for ,and vice versa.Now we prove case(c).Su

30、ppose that is true.Then is false,and by the inductive hypothesis,F has a winning strategy in the -game forcingan outcome in the set of Fs winning positions.But this is a strategy for V inthe -game,and indeed one forcing a set of winning positions for V.The otherdirection is similar.This is our first

31、 link between a key notion in logic(truth)and one in gametheory(strategy).We will broaden the interface as we continue.Some critics seethe success lemma as showing how games yield nothing new.To them,a game-theoretic analysis is good only if it captures some pre-existing logical notion.Ourfocus is t

32、he opposite:what new themes are intrinsic to games,and might enrichthe old agenda of logic?14.3Exploring the game view of predicate logicSimple as it is,there is more to the success lemma than meets the eye.In particular,this result suggests new perspectives on what makes standard predicate logic ti

33、ck.Many technical distinctions to be formulated in the following discussion will recurin subsequent chapters.Dierent winning strategies Truth occurs if and only if there is a winningstrategy for player V,and likewise for falsity and F.But there can be more thanone such strategy.For instance,F had tw

34、o winning strategies in our Example 14.2,using two dierent counterexamples to the claim.Thus,winning strategies are morerefined semantic objects than standard truth values,that we might call reasons fortruth or falsity.Games and game boards The success lemma compares two semantic settings.One is the

35、 model M,or its associated space of assignments s of individual objectss(x)to all relevant first-order variables x.Here a notion from Chapter 11 returns.This space serves as a“game board,”a setting where evaluation games can beplayed,or even other games.Compare a Chess board with possible positions.

36、Chessexpands this with conventions,defining turns for players,as well as their winningpositions.The latter are game-internal:there is nothing intrinsic to the distributionof pieces on the board that makes it a win for White or Black.“lig-09-25”2013/10/29 9:44 page 322#340iiiiiiii322Logic GamesCompar

37、ing two dierent languages The success lemma compares the gameand its board using expressions from dierent languages appropriate to them:V has a winning strategy in game(,M,s)iM,s|=The expression on the left can be rewritten in a game language referring to forcingpowers of players(cf.Chapter 11),whil

38、e that on the right-hand side is best viewedas a modal formula referring to actions on the board,as in Chapter 1:game(,M,s)|=winViM,s|=This dual perspective can be generalized.On the left,one can talk about bothplayers powers for forcing any set of positions in the game.This corresponds tonested sub

39、stitutions in modal assertions about the game board on the right.The general topic of matching games and game boards will be pursued in greaterdepth in Chapters 19 and 24.Defining the games formally Defining complete trees for logic games is largelyroutine.Still,formalization brings out interesting

40、twists to understanding first-orderlogic.Let us define the tree for game(,M,s)as follows.Nodes are all pairs(s,)where s is an M-assignment,and is a subformula of Game moves reflect the earlier ones,changing one or both components of a state.In particular,atomic tests do not change the state,while ch

41、oices only change itsformula,moving from a current node(s,_ )to one of its daughters(s,)and(s,).But formalizing the other rules leads to departures from received views inpredicate-logical semantics.Consider assignment change with quantifiers.Startingat(s,9x),verifier chooses an object d from the dom

42、ain of M,and s is set tosx:=d.Play then continues with (d):that is,it starts afresh from the formalgame state(sx:=d,).But this analysis suggests that,unlike in standard logicalsyntax,we can view the quantifier symbol 9x by itself as a separate interpretableentity,and more specifically,that quantifie

43、rs are atomic games of object picking.Standard thinking assimilates quantifiers to Boolean disjunctions or conjunctions.By contrast,here,the real game operation involved in 9x is sequential composition,gluing the game for after the independent atomic game for 9x.On this view,Predicate-logical semant

44、ics is really a system of games of object pickingand fact testing,related by suitable game operations.“lig-09-25”2013/10/29 9:44 page 323#341iiiiiiiiFormula Evaluation323Next,we need game-internal predicates of turn taking and winning.A formula tells us who is to move at which stage,although we need

45、 to take care with roleswitches for negations.Definition 14.2Formal game treesWe define game(,M,s)inductively,for any assignment s,starting from an initialstate(s,).The first two clauses are for the two kinds of atomic game:(a)game(,M,s)for atomic is a one-node end game,which is a win for verifierif

46、 M,s|=,and for falsifier otherwise.(b)game(9x,M,s)is a one-move game starting at s where it is V s turn,withpossible moves to any state sx:=d,always ending in a win for V.Next we turn to game constructions:(c)game(_ ,M,s)is the disjoint union of the two games game(,M,s)andgame(,M,s)put under a commo

47、n root(s,_ )that is V s turn.(d)game(,M,s)is defined likewise,but with an initial turn for F.(e)game(,M,s)is game(,M,s)with turn and win markings reversed.The negation switch was illustrated with the success lemma.Finally,to deal withquantifiers,we add a clause for an operation of composition for ev

48、aluation games:(f)game(;,M,s)is the tree arising by first taking game(,M,s)andcontinuing at end states with assignment t with a copy of game(,M,t).These tree constructions for games will return in Chapters 20 and 25.Emancipation of syntax The above semantics interprets more than just theusual well-f

49、ormed formulas.For instance,it makes perfect sense to play a game forthe stringPx;9xwhich translates to“First test that P holds for object s(x)under the currentassignment s,then change the value of x,and stop.”In contrast with this,thegame for 9x;Px would first change the value of s(x)to obtain an o

50、bject withthe property P.With composition as a new syntax construction,predicate logic“lig-09-25”2013/10/29 9:44 page 324#342iiiiiiii324Logic Gamesextends to a language of discourse chunks;?;.that might be interesting toaxiomatize.172Even not-so-well-formed formulas now get their chance.Propositions