On decidability of monadic logic of order over the naturals extended by monadic predicates

A fundamental result of Buchi states that the set of monadic second-order formulas true in the structure (Nat, <) is decidable. A natural question is: what monadic predicates (sets) can be added to (Nat, <) while preserving decidability? Elgot and Rabin found many interesting predicates P for which the monadic theory of is decidable. The Elgot and Rabin automata theoretical method has been generalized and sharpened over the years and their results were extended to a variety of unary predicates. We give a sufficient and necessary model-theoretical condition for the decidability of the monadic theory of (Nat,<,P"1,...,P"n).We reformulate this condition in an algebraic framework and show that a sufficient condition proposed previously by O. Carton and W.Thomas is actually necessary. A crucial argument in the proof is that monadic second-order logic has the selection and the uniformization properties over the extensions of (Nat,<) by monadic predicates. We provide a self-contained proof of this result.

Related papers:

title: Restricted set-theoretical definitions in arithmetic
abstract: Notice that sets of ordered pairs of natural numbers are used in this definition. Here and throughout this paper the logical symbols A (and), v (or), -* (if * * * then * * * ), -+ (if and only if), A (for every), and V (there exists) are used; negation does not occur explicitly. The concepts just mentioned, together with identity, are considered as the logical notions. On the other hand, it is known that it is not possible to give an explicit arithmetical definition of addition in terms of successor, that is, a definition using only the concepts of logic, and excluding the concepts of set theory. In fact, from a formula containing (besides parentheses and variables ranging over the natural numbers) only logical symbols and the symbol for successor, we can eliminate all quantifiers, if we allow the symbol 0 to be introduced.' From this, it follows that the only sets of natural numbers which are definable are the finite sets and their complements. In particular, the set of even numbers is not definable. It is then clear that addition also is not definable in this way. Alfred Tarski has proposed (in lectures) consideration of an intermediate type of definition, in which sets of natural numbers but no other sets are allowed. Thus we will have variables a, b, c, * * * which represent natural numbers, and variables A, B, C, * * * which repre-

title: Decidability and Undecidability of Extensions of Second (First) Order Theory of (Generalized) Successor
abstract: We study certain first and second order theories which are semantically defined as the sets of all sentences true in certain given structures. Let be a structure where A is a non-empty set, λ is an ordinal, and P α is an n ( α )-ary relation or function 4 on A . With we associate a language L appropriate for which may be a first or higher order calculus. L has an n ( α )-place predicate or function constant P for each α A ; (3) restricted (weak) second-order calculi which contain monadic predicate variables ranging over finite subsets of A .

title: LOGICAL THEORIES OF ONE-PLACE FUNCTIONS ON THE SET OF NATURAL NUMBERS
abstract: In this paper the author studies the decision problem for logical languages intended to describe the properties of one-place functions on the set of natural numbers. For functions taking a finite number of values a criterion for decidability of the monadic theory of the structure is obtained. For a large class of monotone functions , conditions are found under which the elementary theory of the structure is decidable; corresponding conditions are also found for structures of the form .Bibliography: 20 titles.

title: The Monadic Theory of Morphic Infinite Words and Generalizations
abstract: We present new examples of infinite words which have a decidable monadic theory. Formally, we consider structures ?N, <, P? which expand the ordering ?N, <? of the natural numbers by a unary predicate P; the corresponding infinite word is the characteristic 0-1-sequence xP of P. We show that for a morphic predicate P the associated monadic second-order theory MTh?N, <, P? is decidable, thus extending results of Elgot and Rabin (1966) and Maes (1999). The solution is obtained in the framework of semigroup theory, which is then connected to the known automata theoretic approach of Elgot and Rabin. Finally, a large class of predicates P is exhibited such that the monadic theory MTh?N, <, P? is decidable, which unifies and extends the previously known examples.

title: 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 model-theoretic 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.

title: Uniformization and Skolem Functions in the Class of Trees
abstract: The monadic second-order theory of trees allows quantification over elements and over arbitrary subsets. We classify the class of trees with respect to the question: does a tree T have definable Skolem functions (by a monadic formula with parameters)? This continues [LiSh539] where the question was asked only with respect to choice functions. Here we define a subclass of the class of tame trees (trees with a definable choice function) and prove that this is exactly the class (actually set) of trees with definable Skolem functions.

title: The monadic theory of order
abstract: We deal with the monadic (second-order) theory of order. We prove all known results in a unified way, show a general way of reduction, prove more results and show the limitation on extending them. We prove (CH) that the monadic theory of the real order is undecidable. Our methods are modeltheoretic, and we do not use automaton theory.

title: Monadic Second-Order Theories
abstract: In the present chapter we will make a case for the monadic second-order logic (that is to say, for the extension of first-order logic allowing quantification over monadic predicates) as a good source of theories that are both expressive and manageable. We will illustrate two powerful decidability techniques here—the one makes use of automata and games while the other uses generalized products a la Feferman-Vaught. The latter is, of course, particularly relevant, since monadic logic definitely appears to be the proper framework for examining generalized products. Undecidability proofs must be thought out anew in this area; for, whereas true first-order arithmetic is reducible to the monadic theory of the real line R, it is nevertheless not interpretable in the monadic theory of R. Thus, the examination of a quite unusual undecidability method is another subject that will be explained in this chapter. In the last section we will briefly review the history of the methods thus far developed and give a description of some further results. Monadic (second-order) logic is the extension of the first-order logic that allows quantification over monadic (unary) predicates. Thus, although binary, ternary, and other predicates, as well as functions, may appear in monadic (second-order) languages, they may nevertheless not be quantified over. 1.1.  We are interested less in monadic (second-order) logic itself than in the applications of this logic to mathematical theories. We are interested in the monadic formalization of the language of a mathematical theory and in monadic theories of corresponding mathematical objects. Before we explore this line of thought in more detail, let us argue that formalizing a mathematical language—not necessarily in monadic logic, but rather in first-order logic or in any other formal logic for that matter—can be useful.

title: Solving sequential conditions by finite-state strategies
abstract: Our main purpose is to present an algorithm which decides whether or not a condition 𝕮(X, Y) stated in sequential calculus admits a finite automata solution, and produces one if it exists. This solves a problem stated in  and contains, as a very special case, the answer to Case 4 left open in . In an equally appealing form the result can be restated in the terminology of [7], ,  Every ω-game definable in sequential calculus is determined. Moreover the player who has a winning strategy, in fact, has a winning finite-state strategy, that is one which can effectively be played in a strong sense. The main proof, that of the central Theorem 1, will be presented at the end. We begin with a discussion of its consequences.