Decidability and Definability Results Concerning Well‐Orderings and Some Extensions of First Order Logic

This quantifier binds one variable in each formula of the pair of formulas. L”(“) for a natural n or n = co denotes the (first order) expansion of L obtained by adding to L two predicate symbols 7 and E. By a structure appropriate for L‘(“) is meant any structure = (A“, . . .) defined as follows : 1) ?( = ( A , , . . .) is a structure appropriate for L in the ordinary sense, 2) for a natural n, the universe of %@+l) is the set A,,+1 = {x: z E A,, or x is a finite subset of A,)} and A , = U A f , . new 3) &P) k ~ ( a ) iff a E A , (for a E A,,) .