Vol. 15 No. 1, © The Author, 2005. Published by Oxford University Press. All rights reserved.
An Extension of Muchnik's Theorem
1 Université Bordeaux-1, LaBRI, 351, Cours de la Liberation, 33405, Talence Cedex, France. E-mail: blume{at}labri.fr, 2 Humboldt-Universität zu Berlin, Institut für Informatik, Unter den Linden 6, 10099 Berlin, Germany. E-mail: Kreutzer{at}informatik.hu-berlin.de
One of the strongest decidability results in logic is the theorem of Muchnik which allows one to transfer the decidability of the monadic second-order theory of a structure to the decidability of the MSO-theory of its iteration, a tree built of disjoint copies of the original structure. We present a generalization of Muchnik's result to stronger logics, namely guarded second-order logic and its extensions by counting quantifiers. We also establish a strong equivalence result between monadic least fixed-point logic (M-LFP) and MSO on trees by showing that whenever M-LFP and MSO coincide on a structure they also coincide on its iteration.
Keywords: Monadic second-order logic, Muchnik's theorem, tree automata, fixed-point logics
Received 11 September 2003.