Two MSO-compatible operations: Shelah-Stupp's iteration and Muchnik's iteration
- Prelegent(ci)
- Teodor Knapik (joint work with Didier Caucal)
- Afiliacja
- University of New Caledonia
- Termin
- 16 października 2013 14:15
- Pokój
- p. 5870
- Seminarium
- Seminarium „Teoria automatów”
In the early seventies, Shelah proposed a model-theoretic construction,
nowadays called "iteration". This construction is an infinite
replication in a tree-like manner where every vertex possesses its own
copy of the original structure. Stupp proved that the decidability of
the monadic second-order (MSO) theory is transferred from the original
structure onto the iterated one. In its extended version discovered by
Muchnik and introduced by Semenov, the iteration became popular in
computer science logic thanks to a paper by Walukiewicz. Compared to
the basic iteration, Muchnik's iteration has an additional unary
predicate which, in every copy, marks the vertex that is the clone of
the possessor of the copy. There is a widely spread belief that this
extension is crucial. In this talk we attempt to justify this belief.
After a substantial introduction on monadic second-order logic, we
compare two hierarchies of structures built from finite structures
using:
1. MSO interpretations and Shelah-Stupp iteration,
2. MSO interpretations and Muchnik's iteration.
The two hierarchies coincide at the first level (and of course at level
0). While the latter hierarchy is infinite and strict, the former
hierarchy collapses at level 1.