Advanced Modal Logic
Philosophy 269, Spring 2003, Stanford,
T 1112, Th 1112:30, 2022K
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 secondorder 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,
GoldblattThomason theorem
Week 8
Modal fixedpoint logics, dynamic
logic, mcalculus
Week 9
Modal logic and coalgebra of nonwellfounded
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, 167247.
(Reprint with addenda in D. Gabbay,
ed., 2001, Handbook
of Philosophical Logic,
vol. III., Kluwer, Dordrecht, 325408.)
[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. 8789.
The main result this week is the
Modal Invariance Theorem:
A firstorder 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 firstorder 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 wsaturated models,
existence result: every model
has an wsaturated elementary extension
5.6 if wsaturated models
are modally equivalent,
then they have a bisimulation
5.7 chasing the final diagram
M, s
modeq N,
t=f
elext
elext
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 higherorder version:
MSOL and mcalculus (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 firstorder formulas!
Week 2
Decidability of fragments of firstorder
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, 217274.
The hybrid logic
homepage.
Week 3
Undecidability of tiling problems
and firstorder/modal encodings:
see the "Modal Logic" book by Blackburn,
de Rijke & Venema.
Warmup examples, first and secondorder
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
secondorder and fixedpoint logics.
Undefinability examples showing
the limits of the Theorem.
Week 5
Background in monadic secondorder
logic: e.g., complexity of the
correspondence problem, characterizations
firstorder definability.
Basic modal frame operations:
generated subframes, disjoint unions,
pmorphic images, ultrafilter
extensions. Preservation properties:
examples of nonmodal 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
Fixedpoint extensions of modal
languages:
Propositional dynamic logic,
double set up propositions/programs,
bisimulation invariance and safety
theorems, decidability.
MuCalculus:
general fixedpoint theory, language
and semantics,
reading stacked fixedpoint formulas,
local translation
into MLinfinity: 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
memoryfree strategies.
Brief discussion of connections
with earlier topics:
(a) Fixedpoint 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
'firstorder implication from Ppositive
formula to Patom'.
(b) Extensions of invariance theorem
for models: e.g.,
is the MuCalculus precisely the
bisimulationinvariant
fragment of FOL with fixedpoints?
(c) Frame correspondence theory
with fixedpoint languages.
(d) versions of MuCalculus with
fixedpoints defining relations.
Final topic: more on MLinfinity.
Modal logic with arbitrary
set conjunctions and disjunctions
in relation to its firstorder
counterpart Linfinityomega. Generalized
interpolation,
bisimulation invariance theorem,
proved in the absence
of compactness and other firstorder
techniques. See
J. Barwise & J. van Benthem,
1999, 'Interpolation, Preservation,
and Pebble Games', Journal of
Symbolic Logic 64:2, 881903.
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 firstorder
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 firstorder definability in
general secondorder logic.
(Prove the assertions in class
about fixedpoint extensions.)
Week 5 (preliminary version)
Formulate and prove a preservation
theorem for one of the
modal frame operations, using the
modeltheoretic techniques
of the first week: e.g., that for
generated subframes (due to
Feferman & Kreisel originally).
Modern variant in hybrid logic:
characterize those firstorder
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
pmorphism etc. that are
used in the proof of the GoldblattThomason
Theorem.
Final
Small project on how these topics
work for extended modal languages.
Advertisement
Check out
the Second NorthAmerican Summer
School in Logic,
Language and Information, Bloomington,
June 2430 of this year.
