Spring 2004, Stanford, We 4:30 - 6:30 PM, 60-62J

Johan van Benthem

Abstract

This course is a tour of current interfaces between logic and game theory. 
Logical argumentation or model checking can be cast as games between 
players trying to achieve purposes through optimal strategies. Such 'logic 
games' suggest new links between logic and game theory, including 
calculi of game equivalences, game-forming operations, and players' 
strategies. The resulting machinery can also analyze general games, 
using dynamic and linear logics for processes from computer science. 
But real game theory is also about knowledge, preferences, expectations, 
and rational equilibrium between social agents. We illustrate how key 
issues of imperfect information and future prediction during the course 
of games can be brought into play as well.

Preliminary schedule

Week 1      Introduction:
                    interfaces between games, logic, and computation
Week 2      Games as processes: 
                   modal logic, dynamic logic, MU-calculus
Weeks 3, 4, 5 
                   Imperfect information and changing expectations:
                   dynamic-epistemic logic, information update, 
                   and connections with belief revision
Weeks 6, 7 
                   Logics of special game features: players' preferences, 
                   reaching equilibrium, long-term phenomena
Weeks 8, 9
                  Applications: games in language and philosophy

Perhaps also (If I can fit it in without scaring you off):
                  game logics as process logics, game algebra, etc.

This might still be revised, to include some material on probability.

I will emphasize open questions, and direct interested students
toward paper topics that link up with current research(-ers).

Prerequisites

Basic logic, preferably up to 160A. Some modal logic is essential.

General course materials

Here is a general hand-out for a mini-course on 'Logic & Games' 
taught at various universities in Europe. You might also look at this 
programmatic Mini-Guide to Logic in Action to be published in Beijing.

You can also check the Logic and Games website in Amsterdam.

Finally, some papers and a set of Amsterdam lecture notes have
been put on closed reserve in Tanner Library.

Further material by week

Week 1  A general introduction from an earlier course, with many 
examples showing the wide range of the notion of a game, from
logic and computer science to economics and philosophy.
And here is that sabotage game.

Week 2  You may want to check some basic modal and dynamic logic
(see the material for Philosophy 169 ). And here is a recent paper on
logical options for describing Games as Processes .

Basically, I showed how games can be viewed as processes of the 
sort studied in computer science. This can be done at various levels 
of detail, of which I discussed two: (a) extensive games, all moves 
and actions count, same level as models for modal logic, and (b) 
strategic forms, players' powers for determining the outcomes of 
the game. The paper also mentions possible intermediate levels.

I then showed how the extensive form level involves:

       (i)    basic modal logic with operators [a], <b>, ...
       (ii)   dynamic logic for explicit reasoning about 
              strategies (complex actions), and even
      (iii)   MU-calculus (modal logic with fixed-points)
               for defining the Zermelo coloring algorithm 
               and game-theoretic solution procedures 
               that look for equilibria generally.

Week 3   The topics discussed were:

      (a)  games of imperfect information as models for
             dynamic-epistemic logic: importance of
             iterated and common knowledge
      (b)  analyzing special properties of players:
             e.g., Perfect Recall as knowledge/action
             interchange. Or rather: bounded memory!

For this and realated material read this paper on Games & Epistemic Logic    .
Then we moved to dynamic mechanisms that generate the 'dotted lines':

      (c)  public update and its logic

We will continue with more general information update next week. 
Here is a survey paper with basic notions and open questions.

And here is a paper with some philosophical applications , partly
related to the problem of formulas A that do not satisfy [A!]C-G A.

Week 4  We stayed with public announcement, reviewing the
reduction axioms, this time, in terms of the existential modality.
Then we looked at open questions, as well as some questions 
for which solutions have been announced this year:

       (a) complexity of satsfiablility (and model checking)
       (b) extension to include (relativized!) common knowledge
       (c) axiomatize/decide (?) the schematic validities, which include
             new laws such as <A!><B!> phi  <=>  A & <(<A!>B)!> phi.
       (d) syntactic description of the self-fulfilling assertions A
             satisfying the validity |= [A!]C-G A

After that, the Muddy Children puzzle was used to highlight the 
program structures in conversation: sequential compositions ;, 
guarded choice IF P THEN S ELSE T, iterations WHILE P DO S
Propositional dynamic logic describes this extension of modal
logic (cf. the "Modal Logic " book by Blackburn, de Rijke & Venema,
or the standard text on " Dynamic Logic " by Harel, Kozen & Tiuryn).

Recent result: the logic of public announcement with iteration is
undecidable ( Miller and Moss , mathematics Bloomington, 2002).

Week 5   More general epistemic updates

We actually wandered off to some further new developments 
triggered by the homework, then into philosophical angles with
the Fitch Paradox showing the inconsistency of the Verificationist 
Thesis "phi -> <>K phi" -- and then to some new issues of 

    modeling epistemic scenarios,

such as natural ways of  forming products of models for separate 
agents, and the amount of 'joint information' produced by the mode
of combination. E.g., direct products with natural lifted relations ~-i
validate the interchange axiom K-1 K-2 phi  ->K-2 K-1 phi which is
not in multi-S5. I will try to produce a little Note on this, because 
these 'folklore' issues are seldom discussed in their generality.

The main topic of discussion: product update of an initial epistemic
model M and an action model A to form MxA, according to Baltag,
Moss & Solecki. This covers many cases with hiding information.
Please read the first parts of the main paper, and we will continue 
with this system and its properties next week. That may also be a
good opportunity to prove a significant theorem in this course.

The original key paper is A. Baltag, L. Moss & S. Solecki, 1998, 
'The Logic of Public Announcements,  Common Knowledge 
and Private Suspicions', Proceedings TARK 1998,  43?56, 
Morgan Kaufmann Publishers, Los Altos. Try to download an
updated version from 2003 or 2004 from Moss' webpage.

Week 6  More of the Same

We discussed technical background to the material so far, including 

1. uses of unique outcomes in games for coalition power axioms
2. quick survey of modal game languages: ML, PDL, MU
3. bottom-up and top-down approximation in the MU-calculus
4. basics of public announcement logic, difference (AvB)!, A!VB!
5. Iterations lose finite model property: [(<>T)!*]<>[]False                                         and 'shearing the infinte hedge-hog'

Next we reviewed product update with some more examples:

definition, valid reduction axioms for <A, a><i> phi (reading aid for BMS).

We discussed two follow-up issues in particular:

1. Finite Evolution Problem: given finite initial M and A,

For ongoing computational work on this, see the webpage of 
Jan van Eijck at CWI Amsterdam - or write to jve@cwi.nl.

1. Diversity of Agents: product update presupposes                                        Perfect Recall, by its 'past world' clause s ~-i t.

This also generates an epistemic logic, but with different axioms. 
Interesting issue: describe situations where logical agents with 
different capacities interact . Exploratory paper on this: Johan van
Benthem & Fenrong Liu (2004): 'Diversity of Logical Agents in 
Games' - try to get advance copy via liu@science.uva.nl.
It also deals with truly memory-bounded agents, whose 
update engine is more like a finite-state automaton.

Sascia suggested that this situation of contact (and exploitation) 
is just what happens in the movie Mementoabout a man who 
lost his long-term memory, and is manipulated by girl + cop.

Finally, we saw that epistemic product update can be turned into
doxastic belief update, with arbitrary directed accessibility relations.
But this does not yet yield genuine belief revision, because events
that contradict current beliefs lead to an agent's believing the false,
i.e., everything  instead of an agent adapting his relation arrows.
Next week we will discuss a recent proposal for 

       merging update logic with belief revision theory. 

For a preview, cf. the 2003 Master of LogicThesis of Guillaume 
Aucher at the ILLC Preprint Server in Amsterdam.

Week 7       Belief Revision and Conditional Logic

First we did some theorem proving: the theorem that every finite
epistemic model has an epistemic formula (involving common
knowledge) which defines it up to bisimulation. Details of this
in my paper "One is a Lonely Number" ILLC preprint Server).
This is a special case of a general technique in model theory:
 so-called 'Scott sentences' definig models up to some desired 
structural relation. You can find this in Barwise's "Admissible
Sets and Structures" (Springer 1975), or briefly in the 1999 
paper J. Barwise & J. van Benthem: 'Interpolation, Preservation, 
and Pebble Games',  Journal of Symbolic Logic 64:2, 881-903. 

General issue here: duality between 'group information state' as
a model and as a theory. Could there be a natural formulation
of (product) update directly on syntactic theories? The latter more
syntactic perspective has been more dominant in our next  area:

Then basics of belief revision. A classic is Peter Gärdenfors 1987
book "Knowledge in Flux", MIT Books. For the full AGM story, see 
the survey chapter by Gärdenfors & Rott in the Handbook of Logic
in AI and Logic Programming , Vol. 4, Oxford University Press, 1995.

Best short semantic reference, Adam Grove's paper 'Two Modelings 
for Theory Change',  Journal of Philosophical Logic, 157-170, 1988. 
Do make a copy of this! It has the AGM postulates, and explains the
semantic models with a relative plausibility ordering among worlds.
Basic idea: update is intersection of theories (now viewed as sets 
of models or worlds), belief revision T*A selects those worlds in A
that are closest in the plausibility ordering of worlds according to T.
It is also interesting to check Levi and Harper identities in this case.

Note: these are abstract approaches, as revision can be different
according to one's policy : say, more conservative, or more radical.
Thus, AGM offers no unique 'constructive' account of its operations
T+A (update), T*A (revision) and T-A (contraction) - and likewise,
Grove's models have a 'free parameter' in the form of the abstract
plausibility ordering, which can differ for different epistemic agents.

Next, we looked intot the strong connections between all this and
conditional logic in the Lewis style. You can look up the chapter 
on this topic in the Handbook of Philosophical Logic. Basic idea:
A => B is true at world w if all closest A-worlds according to the 
ordering among worlds induced by w are B-worlds. We saw the 
basic logic (non-monotonic, non-transitive, but with valid modified
versions of such structural rules), which encoded AGM postulates 
'avant la lettre'. Incidentally, Lewis' book Counterfactuals from the 
early 1970s is still a classic! An AI reference that is relevant here:
Yoav Shoham's  Reasoning about Change, MIT Press, 1988.

Transition: how to do this in an update format? Two things needed:

1. richer models, including a plausibility ordering among world                           and a matching richer static language for talking about beliefs                            as truth in all most plausible accessible worlds according to                              the relevant agent
2. update procedures, suitable dynamic language,  and then                    reduction axioms for belief. We already looked at the pilot                                case of public announcement: [A!]B-i phi <=> B-i(A, [A!]phi)                             with a binary belief modality which is really just (again!) a                    conditional A =>-i [A!]phi with its minimality semantics.

Week 8      More on belief revision and merging with update logic

We looked at a more significant AGM postulate in 'sphere semantics':
             T * (A&B) = (T*A) + B
to show how a relative plausibility semantics works.

Then we looked at epistemic models with relative plausibility relations,
interpreting agents' belief as what is true in their most plausible 
epistemically accessible worlds. Result: combined K, B logic. 

The problem of 'qualitative belief revision': how to modify product 
update with a new clause for relative plausibility if we are given r.p. 
relations on the previous stage Maswell as the action model A.

Excursion into qualitative abstract approaches to update and revision.

(1) The only operations f that arise from intersecting sets X with 
some fixed set A are those satisfying (a) introversion f(X) ? X, 
and (b) continuity: f commutes with arbitary unions of sets.

(2) The operation min of taking just the minimal elements of a set
under some given ordering is characterized by the three principles
(a) introversion, (n) intersection min(X-i) for all i is contained in
min (union of all X-i), (c) min(A) intersect B is contained in
min (A intersect B). (I looked it up: these were my 1987 conditions.
You can look up the simple representation argument in this Note .)

A thought: the third condition is exactly the above AGM postulate!
Tomasz and Kyna pointed out this result has long been known 
to economists as the Houthakker (?) conditions? I also seem
to recall now that Hans Rott has published on analogies 
between AGM postulates and formal economics.

Then we did the Aucher system: please read the relevant passages
from his thesis, which you can download from the ILLc server. As we
saw, the update rule is very slanted toward the last observation,
and you are welcome to produce more 'conservative' variants of the
rule reflecting other revision policies. As we we noted, there should 
be many plausible proposals since unlike information update, 
revision is not a unique process from a logical point of view.

Week 9     Connections with game theory

Here are the main points of the final survey: 

1 Logic and Game Theory. 
 Add fine-structure of reasoning and action, merge concerns?

2 Setting the description level:  extensive games,strategic forms.
 Possible invariances (bisimulation), matching languages.
 Analogies with interactive processes in computer science,
 with AI-type concerns added (belief revision), 'agents'.

3 Coarse level: normal form games.
 Strategy profiles, Nash equilibrium, existence results.
 Refinements: too many, or too few equilibria.
 Philosophical worries about consistency of it all.

4 Epistemic characterizations of solution concepts: Aumann a.o.
 Perceptive analysis by logicians in 1990s: Stalnaker, Halpern.
 ILLC Ph.D. Thesis de Bruin, 2004: Rationality Assumptions  behind Game-Theoretic Solution Concepts. Desideratum: systematize it all!

5 Update logic for strategic forms. E.g., analyze solution procedures
 like 'Iterated Removal of Strongly Dominated Strategies' via  iterated
 public announcement of rationality ? cf. Muddy Children puzzles.

6 Finer level: extensive games with all local moves represented.
 Stages of structure,  matching richer logical description languages.

7 Game forms as labeled transition systems: modal-dynamic logic 
 (m-calculus) allows explicit reasoning about moves and strategies.

8 Preferences: deontic logics ('best' outcomes), finer comparisons
 using preference logics Pify, developed originally for social choice.

9 Imperfect information: dynamic-epistemic logic: knowledge.
 Sources of uncertainty:  observation, memory, expectations.

10 Beliefs about where we are, and about future courses of the 
game. In terms of binary (ternary?) plausibility order over worlds.

11 Needs to be put together for study of games: 'logic combinations'.
 New area that can have surprises. E.g., epistemic-temporal logic of 
 Perfect Recall agents is undecidable, even though components are 
 decidable. Reason:  'grid encoding' by the commutation axioms.

12 Our main topic: dynamification. Describe the underlying processes!
 Changing uncertainties that players may have in the course of a game.
 Different sources: observation, expectations, limitations, ... 

13 Information update: public events eliminate parts of epistemic model. 
 Variation 1: different observation powers for agents. Product update
 changes current epistemic model into next after observing an action.

14 Belief revision: how to accommodate new conflicting information?
 Variation 2: different modes of revising. Plausibility update of models.

15 Variation 3: processing limitations: memory, machines, learning rules.
 'Parametrize' the earlier product mechanisms to bounded agents...

16 Dynamification continues. Recent: update preferences via commands. 

17 Expectations and beliefs about the future.
 Backward induction arguments: what is their logic?
 Connection Rationality Postulates:  (TurnE & PREFE phi) => EXP phi
 From utilities to expectations. Philosophy: 'practical syllogism'.

18  Examples: our logical standard mini-tree, a small Centipede game. 
 (This is an IOU, since I did not do it in class.)
 Model: relative plausibility ?i between branches, or between nodes?
 What sort of hypotheses about the future drive expectations about behavior?
 Just about branches/histories, or complete trees with strategic behavior?
 Technical model: branching temporal logic.
 Philosophy again: Belnap et al., "Facing the Future": 'See to it that'.
 Just model constraints, or  again a sort of update mechanism needed for
 hypotheses about future play? Global 'future-oriented' belief revision?

19 BUT...  'Local' versus 'global' update: possibility of 'folding back'?
 Global future-oriented update into local update on BMS/Aucher models?
 Richer worlds which encode strategy profiles. Technical note next week.

20 Related issue: game as complete structure, or game as evolving process
 Equivalence via representation theorems. E.g., game tree is result of  conti-
nued update iff three mathematical conditions hold (van Benthem & Liu).

Summary: see our final class note on Update and Revision in Games .

21 Important topics that we did not address at all. 
 Role of probability. Mixed strategies . Probabilistic beliefs.
 Analyze strategies in more detail. Coalitions. Infinite games, coinduction.

22 Purpose of logical analysis. Fine-structure, see interesting analogies 
with other areas, clarify the reasoning: but not necessarily solve it?

Week 10     Student project presentations and Guest Speaker

Elliott Sober has kindly agreed to speak to us about his own interests in
(probabilistic) game-theoretic considerations in methodologyical problems.

Wednesday June 2,  Room 100-101K

4:30 - 5           Patrick Girard
5 - 5:45           Elliott Sober (guest lecture)
                        "To Give a Surprise Exam, Use Game Theory",
                        Synthese, 1998, 115: 355-373. Check here .
5:45 - 6:15     Tomasz Sadzik
6:15 - 6:45     Audrey Yap
6:45 - 7:15     Itamar Rosenn

Thursday June 3, Room 90-92Q

1:30 - 2          Ian Comfort
2 - 2:30          Kyna Fong
2:30 - 3          Josh Snyder
3 - 3:30         Tomoyuki Yamada

Preliminary topics, with student  emails to get the papers:

1. Josh-1, Product update for agents with bounded memory,                                    
2. Josh-2, Dynamic-epistemic product update, jjj@stanford.edu
3. Tomasz' solution of the Finite Evolution Conjecture,               tsadzik@stanford.edu
4. Patrick: Segerberg and doxastic logic applied to belief                                revision,  pgirard@stanford.edu
5. Ian: Action emulation in the dynamic-epistemic universe,  ian.comfort@stanford.edu
6. Kyna: Signalling games and dynamic update logics,                                             a first pass, kyfong@stanford.edu
7. Audrey: Lying, cheating, and plausibility updating,                    ayap@stanford.edu
8. Tomoyuki: Update logic for commands and changing                             obligations, tomoyuki@csli.stanford.edu
9. Itamar: A discussion of fusion, itam627@stanford.edu

Credits and Projects

Homework + a little project of your own in connection with current research
(10 page paper, half-hour presentation during the final week).

Homework

Test your understanding on the following!
Due date: the next Wednesday after.

Week 1

1A  Prove Hintikka's Lemma which says that a formula phi is true in a 
model under assignment s IFF Verifier has a winning strategy in the 
associated evaluation game GAME(M, s, phi).

1B The method of Backward Induction in game theory solves finite 
extensive games with numerical values for players indicating their 
utilities of outcomes. How would you extend Zermelo's 'coloring 
rule' to assign such numerical values to all nodes?

1C (bonus ) Compare numerical methods like Backward Induction
 to the use of numerical heuristic values at nodes in AI search 
methods like the well-known 'alpha-beta algorithm'.

1D (bonus ) Prove the Pspace upperbound on the sabotaged version of
oGraph Reachability by translating the problem of determining who wins 
into an evaluation game for a suitable corresponding first-order formula.

Week 2

2A Show: all strategies are explicitly definable in a dynamic language when 
the game tree is finite, and no two nodes satisfy the same modal formulas.

2B (You have to find some exposition of MU-calculus for this, e.g., in the 
book on "Dynamic Logic" by Kozen, Harel & Tiuryn, or Colin Stirling, 1999,
'Bisimulation, modal logic and model checking games', "Logic Journal 
of the IGPL" 7, 103-124, 1999) Give an example showing the analogy 
between the Zermelo algorithm and approximative evaluation of the
corresponding fixed-point formula. Also, give one other kind of
fixed-point formula with game-theoretic content.

2C (bonus ) How could you extend your analysis in 2B to describe
 the method of 'backward induction' in game theory?

2D (bonus ) Find a representation theorem for properties of players'
 powers when outcomes are unique, and different on each branch 
of the game tree. Show first that the set of three principles given in 
class does not suffice then.

Week 3

3A  Prove the soundness of the 'reduction axioms' given in class 
for the dynamic-epistemic logic of public announcement.

3B (bonus ) Try to find a similar axiom for common knowledge:
[A!]C-G phi: what is the difficulty?

3C  Compare the reduction axiom for [A1]K-i phi to the earlier
discussion of Perfect Recall. Which additional feature is expressed 
in general imperfect information games by the fact that we now 
have an equivalence, instead of just one implication?

3D Explain the failure of the principle that announcing phi always
leads to common knowledge of phi. Show that this fails, even if
we only allow assertions phi which speakers know to be true.
Try to prove why the given special syntax "atoms | and | or | K | C"
does guarantee that formulas of this form do have this property.

Week 4

4A  Look up the (program reduction) axioms of propositional 
dynamic logic in some textbook, and show that they are sound. 

4B  What happens in our Muddy Children example when the
father announces "at least one of you is clean"? And what
happens when the children speak in turn in the rounds?

4C  Show how you can translate the language of epistemic logic 
with the relativized common knowledge operator into a language 
for dynamic logic where agents relations ~-i are atomic actions.

4D (bonus )  Prove that all formulas of the epistemic language 
with public announcements and all three program operations
are still invariant for epistemic bisimulations between models.

4E (bonus )  Muddy Children as originally stated in class really
involves one more program construction, going beyond standard
imperative programs. Which one, and what about its dynamic logic?

4F (bonus )  Find a consistent formula of public update logic 
with iterated announcements w hich has only infinite models.
(This already suggests some complexity...)

Week 5

5A  Model the following scenarios in our Three Cards example
with product update: (a) 1 shows some card to 2, but 3 does
not see which one, (b) no one has read his card, but  now 1
shows his to the others, without seeing himself what it is.

5B  Also model these email scenarios in a group of 3 people:
(a) 1 sends a true message "A" to 2 with a cc to 3, 
(b) the same thing, but now with a bcc to 3.
(Here, you should know of course what bcc is supposed to do...)
Could you think of other interesting 'epistemic buttons' for email?

5C  Suppose that 1 shows his card to 2 while 3 does not notice.
Then 3 may be misled. How does this change the framework?
What guaranteed in the cases of product update seen so far
that the new models MxA remain epistemic S5-models?

5D (bonus ) Suppose that we keep repeating product with A,
starting from some initial model M: i.e.,   M, MxA , (MxA)xA, ... 
Investigate what happens in some simple cases of M and A. 
Show in particular that, even though the successive models 
may keep growing in size according to the definition of product
update, the successive stages may contract under bisimulation.
Note: I gave one example of this in class: now find new ones!

Things are going well with the homework. We looked at some 
general issues in Week 5: e.g., (a) the precise argument for the
complexity of sabotage, and (b) the background for the given
common-knowledge producing modal forms: these were the 
counterpart of the universal formulas in first-order logic, which 
remain true when passing to any submodel of the current one.

Week 6 

6A   Define the greatest fixed-point NUq* phi(q) in terms of a 
       smallest fixed-point MU. Explain why your definition works.

6B   Define product update for an agent without memory.
        Explain why the Perfect Recall axiom can fail for such agents.
        Give a correct reduction axiom for formulas <A, a><i> phi 
        for such an agent. (Hint: you need an additional existential 
        modality E meaning 'in some world' to get this right.) 

(bonus) How would you deal with, say, a 2-cell memory?

6C  (continuing 5C) Explain in a bit more detail how product 
        update works as a system for belief rather than knowledge. 
         Why does not it perform genuine belief revision?

Comments on homework so far: it is going mostly really well.

5A  you should have explained what the updates do
5B drawing action models is the simplest sort of answer
It gets into issues of security. For a recent paper on email 
via product update: write to Ruan Ji at ILLC.
5C leading to false beliefs is not the same as revision.
The logical reason that the relevant properties are preserved
under product update is that they are all universal Horn.
5D a partial solution (for non-epistemic preconditions)
was announced by Tomasz
6A you need three negations: NOT MUq. NOT phi (NOT q)
6B do not just discuss, but give concrete examples.
The reduction axiom is like that forordinary update, but
replacing the epistemic modality <i> on the right-hand 
side by a global existential modality E.

Week 7

7A  Check the soundness of the AGM postulates in Grove's sphere models.
(bonus) Are the AGM postulates plausible when you think of update (or
revision) involving explicit knowledge statements and many agents?

7B Check the soundness of the given principles for conditional logic
in Lewis-style models. (bonus ) Can you prove a correspondence for 
some further special axiom and the extra 'connectedness property'?

7C Give the correct reduction axiom for postconditions [A1]B-i(C, phi).
(bonus) Can you connect properties of conditionals with the update logic?

Week 8

8A  Discuss some examples of Aucher update, and show how his
ploicy is radical (biased toward the action model plausibilities).
Can you propose a modification that becomes more 'conservative'?

8B Discuss some similarities/differences between belief revision
in AGM style and the way it works out in dynamic update logics.

8C (bonus) Explain Aucher's reduction axiom for postconditions 
of the form B-i alpha phi. 

8D (bonus) Prove the representation result for picking subsets
in some given plausibility ordering (I hope I got them right now)

Varia
See this LOFT 2004 conference site for some current interfaces 
between logic, game theory, and computer science.