|Advanced Modal Logic
Philosophy 269, Spring 2003, Stanford,
T 11-12, Th 11-12:30, 20-22K
This course is
a sequel to Philosophy 169, which was basically
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.)
Basic modal language, translation,
characterization theorem for the
modal fragment of FOL
Guarded fragment and hybrid logics:
and decidability of suitable extended
The counterpoint: undecidability
of tiling problems, and
the sort of quantifier syntax which
leads to undecidability.
Frame correspondence theory, Sahlqvist
Connections with second-order logic,
Basic completeness results and
Modal algebras and frame representations,
connections with universal algebra
Definability of frame classes,
Modal fixed-point logics, dynamic
Modal logic and co-algebra of non-well-founded
Some background reading
To brush up: electronic course
notes for Philosophy 169
P. Blackburn, M. de Rijke &
Y. Venema, 2001, Modal Logic,
J. van Benthem, 1984, 'Correspondence
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,
J. van Benthem, 1995, Exploring
CSLI Publications, Stanford.
Plus other material as we proceed.
Homework set, and/or special
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
1 Modal propositional logic:
language, models, truth definition
2 Bisimulation between models
of modal formulas for bisimulation
3 Translation into a fragment
of first-order logic
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
bis N*, t
6 Further comments on the
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!
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
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
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.
Background in monadic second-order
logic: e.g., complexity of the
correspondence problem, characterizations
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
Birkhoff characterization of equational
Goldblatt & Thomason's characterization
modally definable (elementary)
Weeks 8 & 9
Fixed-point extensions of modal
Propositional dynamic logic,
double set up propositions/programs,
bisimulation invariance and safety
general fixed-point theory, language
reading stacked fixed-point formulas,
into ML-infinity: unrolling up
to an ordinal: bisimulation
invariance, translation into MSOL:
tree model property,
decidability via Rabin's Tree Theorem,
adequacy of the games, role of
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
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
bisimulation invariance theorem,
proved in the absence
of compactness and other first-order
J. Barwise & J. van Benthem,
1999, 'Interpolation, Preservation,
and Pebble Games', Journal of
Symbolic Logic 64:2, 881903.
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
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
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.)
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
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.
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
Small project on how these topics
work for extended modal languages.
the Second North-American Summer
School in Logic,
Language and Information, Bloomington,
June 24-30 of this year.