Decidability and undecidability of extensions of second (first) order theory of (generalized) successor

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 α < λ. We shall study three types of languages: (1) first-order calculi with equality; (2) second-order monadic calculi which contain monadic predicate (set) variables ranging over subsets of A ; (3) restricted (weak) second-order calculi which contain monadic predicate variables ranging over finite subsets of A .