Stationary logic of ordinals (Q1062974)

The paper presents a new tool for proving primitive recursive decidability results: the neighbourhood systems. A neighbourhood system in a structure A consists of a collection \(N=\{N_ n: n<\omega \}\) of functions where each \(N_ n\) maps finite sequences \(\bar a\) of elements of A to structures \(N_ n(\bar a)\) containing (and possibly expanding) the substructure of A generated by \(\bar a.\) Moreover, extensions of the sequence \(\bar a\) in \(N_ n(\bar a)\) correspond to lower subscripts m in a certain way. To a neighbourhood system N corresponds a ramified notion \(N_ n(\bar a)\vDash^*_ n\phi [\bar a]\) of satifaction of first order formulas. Its definition goes exactly like that of ordinary satisfaction with the exception of existential quantifiers; \(N_ n(\bar a)\vDash^*_ n\exists x\phi [\bar a]\) refers to \(N_{n-1}(\bar a,b)\vDash^*_{n-1}\phi [\bar a,b]\). These definitions are set so that the following results hold: \(A\vDash \phi [\bar a]\), if and only if \(N_ n(\bar a)\vDash^*_ n\phi [\bar a]\) and especially for a sentence \(\phi\), \(A\vDash \phi\), if and only if \(N_ n(\emptyset)\vDash^*_ n\phi\); in both cases the quantifier rank of \(\phi\) is at most n. The notion of a neighbourhood system is first used in the paper to prove primitive recursive decidability and quantifier elimination (in a suitable language) results for the first order theories of \(\omega_ 1\) and On due to \textit{J. E. Doner}, \textit{A. Mostowski} and \textit{A. Tarski} [Logic Colloquium '77 Stud. Logic Found. Math. 96, 1-54 (1978; Zbl 0461.03003)]. In stationary logic L(aa) the notion of a neighbourhood system is applicable to finitely determinate structures, i.e. to those satisfying the scheme: \(aa\bar s \forall \bar x(aat\phi (\bar x,\bar s,t)\vee aat\neg \phi (\bar x,\bar s,t))\). The author gives first a proof to the result of \textit{D. Seese} [Trans. Am. Math. Soc. 263, 111-124 (1981; Zbl 0474.03015)] that all ordinals are finitely determinate. The author then proves that the L(aa)-theories of \(\omega_ 1\), \(\omega^ n_ 1\), \(\omega_ 2\) and On are primitive recursive. Primitive recursive quantifier elimination results (in a suitable language) are given, too. It is shown that every ordinal is L(aa)-equivalent to a unique one of one of the forms \(\omega_ 1^{\omega +1}.a+\omega_ 1^{\omega}.b+\omega^ n_ 1.c_ n+...+c_ 0\) where \(a=0\) or \(b=0\) and \(c_ i<\omega^{\omega}+\omega^{\omega}\) for \(i\leq n\). As a corollary, any set of pairwise non L(aa)-equivalent ordinals is countable. An analogous characterization is given to L(aa)-equivalence types of arbitrary models of the L(aa)-theory of On. Finally, it is shown that the L(aa)-theory of On is axiomatized by the axioms for linear ordering together with the schema \(aa\bar s(\exists x(\phi (\bar s,x)\to \exists y\forall z(\phi (\bar s,y)\wedge (\phi (\bar s,z)\to y\leq z)))\) which says roughly that L(aa)-definable nonempty sets have a least element.