Philosophy 359, Spring 2005, Stanford, T 3:30 - 5:30, 50-51P

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

We did not get to the counterpoint: undecidability of tiling
problems, and the sort of non-guarded quantifier syntax 
which typically leads to undecidability. For this, cf. e.g.,
Exploring Logical Dynamics, pp. 135-136.

Week 3

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

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

Look ahead: extensions of the algorithm to fixed-point logics.

Week 4

More connections with second-order logic, undefinability result
for the McKinsey Axiom via a Loewenheim-Skolem argument.

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

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

Weeks 5, 6 

Modal algebras, equational languages for arbitrary algebras,
basic operations: Homomorphisms, Subalgebras, Products

Universal algebra, Birkhoff characterization of equational varieties.

Duality: Stone/Jónsson-Tarski ultrafilter representation, 
general frames, and the frame operations generalized.

Application: proof of the Goldblatt-Thomason Theorem.

Model-theoretic versus universal-algebraic proofs.

Analogies in first-order logic, role of ultraproducts.

Some modern algebraic developments.

A note has been mailed to you with some additional information.
 

Week 7 Propositional Dynamic Logic

Motivations. Two-level language, models, axioms, proofs.
Embeds Hoare logic of sequential programs (though not
exactly the Dijkstra variant: cf. Master's thesis Marc Pauly),
as well as algebra of regular expressions/finite automata.

The axioms are natural because they fix the meaning of the 
program constructions, in terms of frame correspondence.

Completeness: a survey of the basic steps. For details,
see Blackburn, de Rijke & Venema. Decidability follows.
Issue: how general can this 'filtration' argument be made?
Do we perhaps need new notions from automata theory?

Definability: tests add expressive power to basic PDL.
Construction of suitable 'clock model' to separate the two.
Arguments mix model theory with bit of automata theory.

Difficulty: basic model-theoretic properties still open for PDL, 
such as Interpolation. The usual proofs do not work here!

   I did not get to the rest in any detail, but anyway:

Ehrenfeucht games? Bisimulation invariance, and safety.
Semantic characterization of safety in first-order language.
Proof along the lines of Exploring Logical Dynamics, p.114.

Week 8   Mu-Calculus and  LFP(FO)

Playing with PDL: reformulating well-known model axioms;
generalized correspondence theory; and open questions:
e.g., what would be the best possible Sahlqvist Theorem?
'Modal Correspondences Generalized', Studia Logica, t.a.

Modal m-calculus, language, models, evaluation games,
valid principles. See introductory paper by Stirling in Logic
Journal of the IGLP, 1999, and draft chapter by Bradfield &
Stirling in Handbook of Modal Logic (on reserve in Tanner):

(a) Monotone set functions, Tarski-Knaster Theorem, 
      ordinal approximations for LFP and GFP.
(b) Language and models, examples of single fixed-
      point formulas, and iterated cases ('NU MU') .
(c)  Decidability: e.g., via translation into MSOL:
     (monadic second-order logic over orderings),
      invariance w.r.t. trees, and Rabin's Theorem.
(d)  Completeness: rules for smallest fixed-point:
       sample derivation of 'MUp. MU q interchange'.
(e) Bisimulation invariance and Janin-Walukiewicz:
      MSOL & BIS-INV = MU-calculus.
(f)  General landscape of fixed-point extensions,
      all the way up to having inflationary fixed-points:

      ML    -------   PDL    ---------   MU    ----------  IF(MU)

      GF    ------    ??   -----------   LFP(GF)   ------   ??

     FOL  ------  TC(FO)    ------- LFP(FO)  -----  IF(FO)

IF(MU) no longer decidable (Dawar, Graedel & Kreutzer),
LFP(GF) decidable (Graedel), LFP(FO) = IF(FO) (Kreutzer).

Issue: determine PDL as fragment of the modal m-calculus.
Here are  Amsterdam notes from a course by Yde Venema.

Week 9   More Fixed-Point Logic, and Infinitary Logic

Continuing with last week's diagram, we look at two ways 
of extending the basic modal logic -- or on the classical 
side, its 'companion language' of first-order logic. 

• One route adds explicit fixed-point operators:

Some model theory of LFP(FO):

1. invariance for potential isomorphism (Karp Property)
2. Loewenheim-Skolem theorem (Flum 1995)

Many further results in finite model theory (0-1 Laws, etc.).

Still open: model-theoretic characterization of LFP(FO);
or just versions of the major semantic meta-theorems.

At least, one application of what we do know so far:

Generalized modal correspondence theory w.r.t. LFP(FO):
Loeb's Axiom revisited, McKinsey not LFP(FO)-definable,
using the Loewenheim-Skole frame argument given earlier. 

Further results on fixed-point logic and predicate minimization:
J. van Benthem, 2005, 'Minimal Predicates, Fixed-Points, and
Definability', ILLC - to appear in the Journal of Symbolic Logic.

• The second route adds infinite con-/dis-junctions:

Famous system in abstract model theory: L-infinity-omega: 
first-order logic with arbitrary set conjunctions/disjunctions. 
Potential isomorphism again, and two basic features:

1. Karp Property (invariance for potential isomorphism), 
2. Boundedness Theorem: well-foundedness not                                                  even SIGMA-1-1 definable in this language

Classical model-theoretic results often lift thanks to this,
with the strong undefinability in this language of well-foun-
dedness of orderings substituting for f.o. compactness.

Other basic techniques: Scott-sentences defining models
up to potential isomorphism via iterated object description.

Modal Invariance Theorem holds for L-infinity-omega!
The modal fragment is the bisimulation-invariant case.

• Comparison between the two routes:

Locally in given models, formulas of LFP(FO) can be 
translated into infinitary ones, by 'unrolling' their fixed-
point approximations 'far enough'. But the point is that
there is no uniform definition - except for cases with
a uniform bound on approximations, such as <a*>q.

• Abstract model theory: some further background

Recent thesis combining these viewpoints: Marta Garcia-
Matos, 2005, Abstract Model Theory without Negation,
department of mathematics, University of Helsinki.

Excursion: what are the right meta-properties?

Failures of classical meta-properties: often interesting 
generalized formulations. J. Barwise & J. van Benthem
1999, 'Interpolation, Preservation, and Pebble Games',
Journal of Symbolic Logic 64:2, 881-903. 

Indistinguishable for first-order logic from the usual
formulation of the interpolation theorem is this version: 

          TFAE:
          (a) A and B have interpolant in their joint language L
          (b) A implies B along potential isomorphism w.r.t. L

Idea of entailment along a relation: generalize inference to 
include informational 'jumping from one situation to another'. 

Intuitively, entailment along p.i. is stronger than ordinary
consequence, and it corresponds more closely to what 
an interpolant really tells you. Still, for FOL, the difference 
collapses thanks to an easy argument using the Loewen-
heim-Skolem Theorem and the Cantor Theorem (potential 
isomorphism implies isomorphism on countable models).

Ordinary interpolation fails for L-infinity-omega. But this 
second version holds! Proof in the B&B paper combines 
a lot of the earlier ideas. Issue then: when classical meta-
properties are said to 'fail' in some new logic,  what does 
that really mean? Perhaps only one formulation fails, while 
other equally plasuible versions of the property still hold?

In any case, style for neat reformulations of earlier results:

The following are equivalent for all first-order formulas:

1. A entails B along L-bisimulation
2. there is a modal L-formula C with A |=C|= B

This closes the circle of topics in this course.
 

Week 10  Student paper presentations!

Here are the working titles that I gathered from your emails:

Jesse Alama, substitution-based correspondence algorithms
Dan Auerbach, undecidability via tiling and guarded syntax
Tyler Greene, AFA set theory and infinitary modal logic
Tomohiro Hoshi, bounded fragment and modal model theory
Dan Long, Goldblatt-Thomason theorems for hybrid languages
Tomasz Sadzik, interpolation in modal fixed-point logics
Conor Wilson, evaluation games for the MU-calculus
Audrey Yap, interpolation theorems in hybrid languages
 

At least an advertisement for some topics I did not get to:

Some recent results in hybrid logics and other extended 
modal languages: Bounded Fragment, Second-Order 
Propositional Quantifiers. Balder ten Cate, 2005, Model 
Theory for Extended Modal Languages, ILLC Amsterdam.

Alternative semantics: topological, neighbourhood models:
how does the preceding theory generalize? Translations
from neighbourhood modal logic back into bimodal logic.
For modern instances of neighborhood semantics, cf. the 
forthcoming Stanford dissertation of Darko Sarenac on
spatial reasoning, and the 2001 ILLC dissertation by
Marc Pauly, Logic for Social Software, on neighborhood
models for games, and powers of agents in group action.

Modal logic and co-algebra of non-well-founded phenomena.
Cf. the home pages of Larry Moss (CS Indiana Bloomington),
Jan Rutten (CWI & VU Amsterdam) and Yde Venema (ILLC).
 

Some background reading

To brush up: electronic course notes for Philosophy 169. 

Best-seller: P. Blackburn, M. de Rijke & Y. Venema, 2001, 
Modal Logic, Cambridge UP (on reserve in Tanner).

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.

[some more recent nineties topics;] J. van Benthem, 1995, 
Exploring Logical Dynamics, CSLI Publications, Stanford.

Plus other material as we proceed.

See also the Handbook of Modal Logic, to appear with
Elsevier, edited by Patrick Blackburn, Johan van Benthem 
& Frank Wolter. This has chapters across the whole range.

Credit

Homework set and/or special project.

Support

Patrick Girard (pgirard@stanford.edu) will grade your homeworks,
and be available for questions. Please contact him for details.

Week 1

Material: see Exploring Logical Dynamics, p. 87-89, for a proof

of the main result for this week: 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!

6.6  more sophisticated modern version (J. Barwise & J. van 
       Benthem, 1999, 'Interpolation, Preservation, and Pebble 
       Games', Journal of Symbolic Logic 64:2, 881?903). The
       following are equivalent  for all first-order formulas f(x), y(x):

      (a) f entails y along bisimulation: i.e., if E is a bisimulation
              between M, s and N, t, and M, s |=f, then N, t |=y
       (b)  there exists a modal interpolant as.t. f |= a|= y

Coda
We also did a little excursion on why the basic modal language
behaves so much like the full language of first-order logic. One
part is the 'potential isomorphism'/'bisimulation' transfer explored
in de Rijke's 1993 ILLC dissertation Extending Modal Logic. But
this is still heuristic. Perhaps the language of modal logic is an
elementary submodel of the appropriate 'meta-model' for FOL
= <FORM, PREDSYMBOL, imply, occur> --- 'reflecting' all true 
existential first-order properties of its objects. Mason 1985 (JSL)
shows that this complete theory is equivalent to True Arithmetic!

Week 2

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

Readings: for general background and motivation, look at

       Erich Graedels' dialogue on guarded languages

The original source is 

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

Here is a recent paper with proofs and addenda, to appear in
a forthcoming issue of the Journal of Logic, Language and
Information on '10 Years of the Guarded Fragment'.

For a general view of extended modal logics, 
see the hybrid logic homepage.

Week 3

An early reference for frame correspondence theory is the
chapter on 'Correspondence Theory' in the Handbook of
Philosophical Logic, 1984, and revised reprint 1997.

You can also look at Blackburn, de Rijke & Venema.

Here is a recent paper, to appear in Studia Logica, 
which also looks at extensions beyond first-order.

Week 4

The Correspondence Theory chapter, and also the book
Modal Logic and Classical Logic have the original proofs
in terms of the duality with modal algebras, representation
methods, and an appeal to the Birkhoff Theorems charac-
terizing equational varieties in universal algebra.

Here we present a newer purely model-theoretic analysis.

Homework

Weeks 1 + 2    (with apologies for the strange rotation)

Week 3

Week 4

Week 5

Week 6:

(a)      State and prove the duality results for H, S, P on modal 
           algebras and the corresponding operations on general 
           frames that were used in the proof of the GT Theorem.

(b)      Explain the version of GT given at the end of the notes 
           involving an added universal modality ("true in all worlds').

(c)*     Look up and explain the purely model-theoretic proof of GT.

Week 7:

(a)      Derive the law that (a + b)* = (a* ; b*)* in its PDL version.

(b)      How does the completeness proof for PDL in 'B, dR & V',
           simplify for a language in which all the programs only 
           have non-iterated *-operators? 

(c)     Supply details of the proof involving 'clock models' showing
          that PDL with test is more expressive than PDL without test.

(d)*    Devise a characteristic Ehrenfeucht-Fraisse game 
           of model comparison for the language of PDL.

(e)*    Look up and explain the proof of the Modal Safety Theorem
           for bisimulation. See Exploring Logical Dynamics, Ch. .5

Week 7: preliminary version.