Decidable Theories of the Ordering of Natural Numbers with Unary Predicates

Abstract. Expansions of the natural number ordering by unary predicates are studied, using logics which in expressive power are located between first-order and monadic second-order logic. Building on the modeltheoretic composition method of Shelah, we give two characterizations of the decidable theories of this form, in terms of effectiveness conditions on two types of "homogeneous sets". We discuss the significance of these characterizations, show that the first-order theory of successor with extra predicates is not covered by this approach, and indicate how analogous results are obtained in the semigroup theoretic and the automata theoretic framework.

• Type: Conference
• Year: 2006
• Where: CSL
• Authors: Alexander Moshe Rabinovich, Wolfgang Thomas
• Keywords: Automated Reasoning, CSL 2006, Modeltheoretic Composition Method, Monadic Second-order Logic, Unary Predicates