Inessential features, ineliminable features, and modal logics for model theoretic syntax (Q1006492)

This paper further develops the theory of model-theoretic syntax. The author looks at various modal logics for trees with the aim to reach a better understanding of what is a good logic for the formalisation of grammatical theories. The focus of the paper lies on the notion of an \textit{inessential feature}, that has been introduced by \textit{M. Kracht} [Lect. Notes Comput. Sci. 1328, 43--62 (1997; Zbl 0896.03023)]. The main result is a generalization of a theorem by Kracht [loc. cit.]: Any tree language that can be defined in a stronger logic, but not in some weaker logic, can be defined in the weaker logic with inessential features (assumption: all logics involved are weaker than MSO). The theorem is a consequence of a theorem by \textit{J. W. Thatcher} [J. Comput. Syst. Sci. 1, 317--322 (1967; Zbl 0155.01802)]. This shows that the various modal logics for trees differ precisely with respect to which inessential features of trees are eliminable or not. Furthermore, the author argues that the logic MSO might be too strong as a logic for formalizing grammatical theories, because it allows for the elimination of all inessential features.