Philosophy 269, Spring 2003, Stanford, T 11-12, Th 11-12:30, 20-22K

Abstract

This course is a sequel to Philosophy 169, which was basically
an introduction to modal logic emphasizing major techniques, 
plus a small tour of modern application areas. This time, we 
present the mathematical theory behind modal logic. You need 
some basic model theory for the results to be proved, but this 
will be explained as we proceed. (And please ask questions.)

Preliminary schedule

Week 1 
Basic modal language, translation, bisimulation invariance, 
characterization theorem for the modal fragment of FOL

Week 2 
Guarded fragment and hybrid logics: expressive power 
and decidability of suitable extended modal languages

The counterpoint: undecidability of tiling problems, and
the sort of quantifier syntax which leads to undecidability.

Week 3 
Frame correspondence theory, Sahlqvist theorems

Week 4 
Connections with second-order logic, undefinability results

Week 5 
Basic completeness results and modal algebras

Week 6 
Modal algebras and frame representations,
connections with universal algebra

Week 7 
Definability of frame classes, Goldblatt-Thomason theorem

Week 8 
Modal fixed-point logics, dynamic logic, m-calculus

Week 9 
Modal logic and co-algebra of non-well-founded phenomena

Some background reading

To brush up: electronic course notes for Philosophy 169

P. Blackburn, M. de Rijke & Y. Venema, 2001, Modal Logic, 
Cambridge UP.

J. van Benthem, 1984, 'Correspondence Theory', in
D. Gabbay and F. Guenthner, eds., 1984, Handbook of 
Philosophical Logic, Vol. II., Reidel, Dordrecht, 167-247.
(Reprint with addenda in D. Gabbay, ed., 2001, Handbook
of Philosophical Logic, vol. III., Kluwer, Dordrecht, 325-408.)

[the original, more extensive source:] J. van Benthem, 1983, 
Modal Logic and Classical Logic, Bibliopolis, Napoli.

J. van Benthem, 1995, Exploring Logical Dynamics, 
CSLI Publications, Stanford.

Plus other material as we proceed.

Credit

Homework  set, and/or special project.

Week 1

Material: copies from 'Exploring Logical Dynamics', p. 87-89.

The main result this week is the Modal Invariance Theorem:

       A first-order formula f(x) is definable by a 
       modal one iff it is invariant for bisimulation

This is the key semantic characteristic of modal languages.

Here are the main points that were covered:

1  Modal propositional logic: language, models, truth definition
2  Bisimulation between models
     invariance of modal formulas for bisimulation
3  Translation into a fragment of first-order logic
     good balance of expressiveness and decidability
4  Statement of the MIT
5  Proof of the MIT, in a number of modules

5.1  one direction is just bisimulation invariance for modal formulas
5.2  to be proved: mod(f)|=f, 
        and then done by compactness
5.3  if (M, s)|= mod(f), then there is a model (N, t)|=f 
        which is modally equivalent to (M, s)
5.4  elementary submodel, limits of elementary chains
5.5  w-saturated models, existence result: every model 
        has an w-saturated elementary extension
5.6  if w-saturated models are modally equivalent, 
        then they have a bisimulation
5.7  chasing the final diagram

          M, s           mod-eq           N, t|=f

               el-ext                                    el-ext

        M*, s            bis N*, t

6  Further comments on the MIT

6.1  proof extends to many further results: e.g., total bisimulation
6.2  higher-order version: MSOL and m-calculus (Janin & Walukiewicz)
6.3  different proofs: e.g., via ABN Lemma: 'modally equivalent 
        models have elementarily equivalent tree unravelings'; 
6.4  more constructive version for finite models (Rosen)
6.5  modal definability is undecidable inside first-order formulas!

Week 2

Decidability of fragments of first-order logic with suitably guarded 
patterns of quantification. Use of quasimodels and representation.

Readings: parts of

Erich Graedels' dialogue on guarded languages

H. Andreka, J. van Benthem, & I. Nemeti, 1998, 'Modal Logics and 
Bounded Fragments of Predicate Logic', Journal of Philosophical 
Logic 27:3, 217-274. 

The hybrid logic homepage.

Week 3

Undecidability of tiling problems and  first-order/modal encodings:
see the "Modal Logic" book by Blackburn, de Rijke & Venema.

Warm-up examples, first- and second-order frame correspondence.

Week 4

Proof of the Sahlqvist Theorem in its correspondence version: 
the basic minimal substitution algorithm and its correctness.

Extensions of the algorithm to second-order and fixed-point logics.

Undefinability examples showing the limits of the Theorem.

Week 5

Background in monadic second-order logic: e.g., complexity of the
correspondence problem, characterizations first-order definability.

Basic modal frame operations: generated subframes, disjoint unions, 
p-morphic images, ultrafilter extensions. Preservation properties:
examples of non-modal definability, syntax for preservation classes.

Weeks 6 & 7

Modal algebras, Stone ultrafilter representation,

Birkhoff characterization of equational varieties,
Goldblatt & Thomason's characterization of the
modally definable (elementary) frame classes.

Weeks 8 & 9

Fixed-point extensions of modal languages:

Propositional dynamic logic, double set up propositions/programs,
bisimulation invariance and safety theorems, decidability.

Mu-Calculus: 
general fixed-point theory, language and semantics,
reading stacked fixed-point formulas, local translation 
into ML-infinity: unrolling up to an ordinal: bisimulation 
invariance, translation into MSOL: tree model property,
decidability via Rabin's Tree Theorem, evaluation games,
adequacy of the games, role of memory-free strategies.

Brief discussion of connections with earlier topics:

(a) Fixed-point languages for defining minimal valuations of
antecedents in Sahlqvist Theorem (this covers most known
axioms, including Loeb's). Key feature: a minimal valuation
exists if the antecedent set transformation has the complete
Intersection property, and CIP is guaranteed by the syntax 
'first-order implication from P-positive formula to P-atom'.

(b) Extensions of invariance theorem for models: e.g., 
is the Mu-Calculus precisely the bisimulation-invariant 
fragment of FOL with fixed-points?

(c) Frame correspondence theory with fixed-point languages.

(d) versions of Mu-Calculus with fixed-points defining relations.

Final topic: more on ML-infinity. Modal logic with arbitrary
set conjunctions and disjunctions in relation to its first-order
counterpart L-infinity-omega. Generalized interpolation, 
bisimulation invariance theorem, proved in the absence
of compactness and other first-order techniques. See

J. Barwise & J. van Benthem, 1999, 'Interpolation, Preservation, 
and Pebble Games', Journal of Symbolic Logic 64:2, 881­903. 

Homework

Week 1

Extend the invariance theorem to an extended modal  language 
with an unbounded universal and existential modality over worlds,
characterizing it in terms of invariance for total bisimulations,
whose domain and range are the whole models involved.
Which parts of the proof go through unchanged?

Week 2

Extend the proof of decidability for the guarded fragment to one
for the loosely guarded fragment. Which steps remain the same,
what needs to be changed? Which parts of the proof would
go through even for general first-order formulas?

Week 3

Try to find a formula encoding the tiling property for the plane
which has as large a guarded part as possible. (This may
require some syntactic tricks.) Where must you go beyond GF? 

(Explore decidable tiling problems using guarded versions.)

Week 4

Find a most general formulation of the Sahlqvist Theorem 
for first-order definability in general second-order logic.

(Prove the assertions in class about fixed-point extensions.)

Week 5 (preliminary version)

Formulate and prove a preservation theorem for one of the 
modal frame operations, using the model-theoretic techniques
of the first week: e.g., that for generated subframes (due to
Feferman & Kreisel originally). Modern variant in hybrid logic: 
characterize those first-order formulas that are invariant for 
generated submodels. This combines two of the operations.

Discuss how the results of this week fare for extended modal 
languages, with operators such as the universal modality.

Week 6

Prove all results connecting H, S, P on modal algebras and 
operations on general frames like p-morphism etc. that are 
used in the proof of the Goldblatt-Thomason Theorem.

Final 

Small project on how these topics work for extended modal languages.
 

Advertisement

Check out  the Second North-American Summer School in Logic, 
Language and Information, Bloomington, June 24-30 of this year.