Modal
Logic
This course is an introduction
emphasizing major techniques,
and a small tour of modern
application areas for modal logic.
Schedule

Week
1 Basic Language and Expressive Power
This week introduces the
basic modal language, and its
evaluation in possible worlds models. This is a paradigm
for studying the diverse modal languages used in practice.
Expressive power is measured by the modern technique
of bisimulation invariance, also found in computer science.
We can think of bisimulation in terms of playing games,
a topic that will return in this course.

basic language and semantics

bisimulation and expressive power

Week
2 Axiomatization and Complexity
Here we look at the Balance
found in any logical system.
Expressive power comes at a price in terms of complexity
for the basic tasks a logical system is used for, These are
semantical evaluation/model checking, valid reasoning/
SATtesting, and model comparison for language equiva
lence/structural similarity. This involves a brief excursion
into computational complexity, a whole topic by itself.

valid reasoning and axiomatics

complexity of logical tasks

Week
3 Translations and Extensions
We now turn our working analogy between modal operators
and quantifiers into a systematic translation. This puts the
basic modal language inside a spectrum of much stronger
extended modal languages, with the decidable Guarded
Fragment GF
of firstorder logic near the top. The next
workshop on all matters
guarded is this summer. in Nancy
We have also looked at how extended modal languages
fare when we consider all our earlier topics: model checking,
bisimulation, minimal logic, complexity, and ST translation.
Finally, we have explored the border line with undecidability,
noting the non (pairwise)guarded quantification needed to
express the 'grid structure' of the undecidable Tiling Problem.

Week
4 Landscape of modal logics, frame correspondence

Week 5 Recapitulation,
and temporal logic
We first rehearsed earlier material, looking at evaluation games
for modal formulas, inductive decomposition of valid sequents,
and
some further examples of computing frame correspondence.
On Thursday, we looked at tense logic, with the basic language
as proposed by Prior, expressive power on frames (firstorder
properties of linear orders, Dedekind completeness of the reals),
and then the Until/Since extension, explaining Kamp's Theorem
on expressive completeness for this language w.r.t. the full
firstorder language over the reals and related linear orders.
Finally, we looked at modaltemporal models of branching time,
which seemed an appropriate setting for the day's closing event,
viz. the SSP Forum lecture "Is
the Future Unreal?" by John Perry.
Further material on temporal logic: see e.g., this survey
article,
and the references therein, or look at this older monograph
with links to philosophy and linguistics.

Week 6 Modal Logics of Space
Guest speaker Darko Sarenac. See also this seminar
page
and
this Handbook page for
more material on modal logics
of topology and geometry.

Week 7 Epistemic
logics of knowledge and update
We have done the basics on Tuesday and update on Thursday.
See this text,
as well as the following papers (links to follow):
Update in Rotterdam,
One
is a Lonely Number.

Week 8 Dynamic
logics of action
Here is some material about propositional
dynamic logic.
And this is the key monograph
by three founding fathers.

Week 9 Games:
knowledge in action
You can look at the course homepage for Philosophy
298.
On Tuesday, we did some basic modal structures in games:
action modalities, reasonign about strategies in dynamic logic,
Zermelo's Theorem and fixedpoint definition for coloring algorithm,
epistemicdynamic logic of games with imperfect information.
Thursday: special topic, modal
deconstruction of firstorder logic.

Week 10 Student
presentations, two 2hour sessions.
Presentations take 15 minutes, with 5 minutes discussion.
Tuesday June 1st, 11 AM  1:15 PM, room
200305
Thursday June 3d, 10 AM  12:15 PM, room 160326
Titles, and emails ifor people who want to request the paper:
Josh Snyder, Vagueness, Common Knowledge &
Public Announcements, jj@stanford.edu
Govind Persad, The STIT Operator: a modal representation
of agency, gpersad@stanford.edu
Dan Auerbach, Dynamic Doxastic Logic as a Model for
Public Key Protocols, dan06@stanford.edu
Jonathan Lipps, Kripke's World: A Program that Tests
for Bisimulation, jon832@stanford.edu
Renee Trochet, Defaults in Update Semantics,
rtrochet@stanford.edu
Jonathan Frank, Epistemic Reasoning in MultiAgent
Systems, jonfrank@stanford.edu
Kim Diana Ly, FirstOrder and SecondOrder Aspects of
BranchingTime Semantics', kly@stanford.edu
Chris
Gearhart, An Analysis of KnowledgeBased TCP,
cmg33@stanford.edu
Brett Lockspeiser,Possible Worlds,
blocks@stanford.edu
Peter LubellDoughtree, Programming the Evaluation
Game, pld@stanford.edu
Tyler Greene, Plethoric Epistemology,
tylergreene@stanford.edu
Course materials
The book "Manual of Intensional
Logic" provides general philosophical
background. It can be obtained
at CSLI's Publications Office.
But the self
image of modal logicians
is shifting, and the course now takes a more
modern view of what makes
modal logic tick as a family of 'finestructure
formalisms' striking a nice
balance between reasonable expressive
power and often decidable
computational complexity. See the recent
stateoftheart new Textbook
by
Blackburn, de Rijke, and Venema,
or the new Handbook
of Modal Logic, under construction right now.
The following paper in the
volume "Companion to Philosophical Logic"
is a lightning
survey of this course. You may also want to look at some
conference
sites. A nice source of illustrations for topics in the course
is the logic
animations
page of Jan Jaspars in Amsterdam.
Practical things
To be announced. You will
get weekly homework assignments
plus a final paper or presentation
assignment.
Homework
Week
1 This tests your understanding of (a) truth/expressive power
of modal formulas in models, and (b) the workings of bisimulation.
Week
2 Simple formal proofs, arguments about modal validity,
and some impressionistic exercises in
complexity analysis.
Week
3 Working with translations, and firstorder fragments,
and understanding a few useful extended
modal languages.
Week
4 Substitution method for computing firstorder frame
correspondents, and analyzing nonfirstorder
modal axioms.
Week
5 Varia from the survey, and some temporal logic.
Week 6: you got spatial logic homework
from our guest speaker.
Weeks 7, 8, 9: combined
homework on epistemic logic,
dynamic logic & a bit of games: the
final one!
