| Logic, Games, and Computation
Stanford, We 4:30 - 6:30 PM, 60-62J
Johan van Benthem
This course is
a tour of current interfaces between logic and game theory.
or model checking can be cast as games between
to achieve purposes through optimal strategies. Such 'logic
new links between logic and game theory, including
calculi of game
equivalences, game-forming operations, and players'
resulting machinery can also analyze general games,
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.
interfaces between games, logic, and computation
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
(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).
preferably up to 160A. Some modal logic is essential.
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
papers and a set of Amsterdam lecture notes have
been put on closed
reserve in Tanner Library.
material by week
A general introduction
from an earlier course, with many
the wide range of the notion of a game, from
logic and computer
science to economics and philosophy.
And here is that
You may want to check some basic modal and dynamic logic
(see the material
169 ). And here is a recent paper on
for describing Games as Processes
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)
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.
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.
We stayed with public announcement, reviewing the
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)!>
(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
in conversation: sequential compositions ;,
IF P THEN S ELSE T, iterations WHILE P DO S
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).
the logic of public announcement with iteration is
Miller and Moss , mathematics Bloomington, 2002).
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
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
issues are seldom discussed in their generality.
The main topic
of discussion: product update of an initial epistemic
and an action model A to form MxA, according
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
to prove a significant theorem in this course.
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,
Publishers, Los Altos. Try to download an
from 2003 or 2004 from Moss' webpage.
More of the Same
technical background to the material so far, including
More technicalities of update
computation (order dependence in Muddy
- uses of unique outcomes
in games for coalition power axioms
- quick survey of modal
game languages: ML, PDL, MU
- bottom-up and top-down
approximation in the MU-calculus
- basics of public announcement
logic, difference (AvB)!, A!VB!
- Iterations lose finite
model property: [(<>T)!*]<>False
and 'shearing the infinte hedge-hog'
invariance for PDL and update logics, etc.
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
must the iterated update sequence M, MxA, (MxA)xA ,...
- Finite Evolution Problem: given
finite initial M and A,
(plausible for games!) stabilize modulo bisimulation?
For ongoing computational work
on this, see the webpage of
Jan van Eijck at CWI Amsterdam
- or write to email@example.com.
Alternative: forgetful updaters, with just a ~-i b.
- Diversity of Agents: product
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
It also deals with truly memory-bounded
update engine is more like a
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
merging update logic with belief revision theory.
For a preview, cf. the 2003 Master
of LogicThesis of Guillaume
Aucher at the ILLC Preprint Server
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:
More on this, and Aucher's product update
system for belief revision
next week. We will also compare 'backward-looking' and 'forward-
looking' update and revision systems then, e.g., for games.
- 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
- 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.
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
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
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.
Connections with game theory
Here are the main points of the
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),
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
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
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
'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
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
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?
Student project presentations and Guest Speaker
Elliott Sober has kindly agreed
to speak to us about his own interests in
considerations in methodologyical problems.
Wednesday June 2,
4:30 - 5
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
6:15 - 6:45
6:45 - 7:15
Thursday June 3, Room 90-92Q
1:30 - 2
2 - 2:30
2:30 - 3
3 - 3:30
with student emails to get the papers:
The plan is to produce an official
Tech Report with much of this material.
- Josh-1, Product update
for agents with bounded memory,
Dynamic-epistemic product update, firstname.lastname@example.org
- Tomasz' solution of
the Finite Evolution Conjecture,
- Patrick: Segerberg
and doxastic logic applied to belief
- Ian: Action emulation
in the dynamic-epistemic universe, email@example.com
- Kyna: Signalling games
and dynamic update logics,
a first pass, firstname.lastname@example.org
- Audrey: Lying, cheating,
and plausibility updating,
- Tomoyuki: Update logic
for commands and changing
- Itamar: A discussion
of fusion, email@example.com
Homework + a
little project of your own in connection with current research
(10 page paper,
half-hour presentation during the final week).
Test your understanding
on the following!
Due date: the
next Wednesday after.
Hintikka's Lemma which says that a formula phi is true
model under assignment
s IFF Verifier has a winning strategy in the
game GAME(M, s, phi).
1B The method
of Backward Induction in game theory solves finite
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?
) 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'.
) Prove the Pspace upperbound on the sabotaged version of
by translating the problem of determining who wins
into an evaluation
game for a suitable corresponding first-order formula.
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,
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
fixed-point formula. Also, give one other kind of
with game-theoretic content.
) How could you extend your analysis in 2B to describe
of 'backward induction' in game theory?
) Find a representation theorem for properties of players'
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
the soundness of the 'reduction axioms' given in class
for the dynamic-epistemic
logic of public announcement.
) Try to find a similar axiom for common knowledge:
[A!]C-G phi: what
is the difficulty?
the reduction axiom for [A1]K-i phi to the earlier
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"
that formulas of this form do have this property.
up the (program reduction) axioms of propositional
in some textbook, and show that they are sound.
happens in our Muddy Children example when the
"at least one of you is clean"? And what
happens when the
children speak in turn in the rounds?
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.
) Prove that all formulas of the epistemic language
with public announcements
and all three program operations
are still invariant
for epistemic bisimulations between models.
) Muddy Children as originally stated in class really
involves one more
program construction, going beyond standard
Which one, and what about its dynamic logic?
) Find a consistent formula of public update logic
announcements w hich has only infinite models.
suggests some complexity...)
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.
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?
that 1 shows his card to 2 while 3 does not notice.
Then 3 may be
misled. How does this change the framework?
in the cases of product update seen so far
that the new models
MxA remain epistemic S5-models?
) Suppose that we keep repeating product with A,
some initial model M: i.e., M, MxA
, (MxA)xA, ...
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.
gave one example of this in class: now find new ones!
Things are going
well with the homework. We looked at some
in Week 5: e.g., (a) the precise argument for the
sabotage, and (b) the background for the given
producing modal forms: these were the
the universal formulas in first-order logic, which
remain true when
passing to any submodel of the current one.
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
was announced by Tomasz
6A you need three negations: NOT
MUq. NOT phi (NOT q)
6B do not just discuss, but give
The reduction axiom is like that
forordinary update, but
replacing the epistemic modality
<i> on the right-hand
side by a global existential modality
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?
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)
See this LOFT
site for some current interfaces
game theory, and computer science.