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/                  SAT-testing, 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 first-order 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 (first-order
         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
         first-order language over the reals and related linear orders.
         Finally, we looked at modal-temporal 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 fixed-point definition for coloring algorithm,
         epistemic-dynamic logic of games with imperfect information.

         Thursday: special topic, modal deconstruction of first-order logic.

  • Week 10   Student presentations, two 2-hour sessions.
         Presentations take 15 minutes, with 5 minutes discussion.

       Tuesday June 1st,     11 AM - 1:15 PM, room 200-305
         Thursday June 3d,     10 AM - 12:15 PM, room 160-326

       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 Multi-Agent 
                                  Systems, jonfrank@stanford.edu
       Kim Diana Ly, First-Order and Second-Order Aspects of 
                                  Branching-Time Semantics', kly@stanford.edu
       Chris Gearhart, An Analysis of Knowledge-Based TCP, 
                                  cmg33@stanford.edu
       Brett Lockspeiser,Possible Worlds, 
                                 blocks@stanford.edu
       Peter Lubell-Doughtree, 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 'fine-structure
formalisms' striking a nice balance between reasonable expressive 
power and often decidable computational complexity. See the recent 
state-of-the-art 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 first-order fragments,
and understanding a few useful extended modal languages.

Week 4  Substitution method for computing first-order frame 
correspondents, and analyzing non-first-order 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!

 

Logic in Action ILLC