Undecidability and 1-types in the recursively enumerable degrees (Q688787)

The authors present a new coding method which enables them to establish the results of \textit{L. Harrington} and \textit{S. Shelah} [Bull. Am. Math. Soc., New Ser. 6, 79-80 (1982; Zbl 0518.03016)]: the recursively enumerable degrees have an undecidable first-order theory, and \textit{K. Ambos-Spies} and \textit{R. I. Soare} [Ann. Pure Appl. Logic 44, 1-23 (1989; Zbl 0682.03024)]: the recursively enumerable degrees realise infinitely many one types. Each of the original proofs of the above theorems, as well as other known proofs of the undecidability of the first-order theory of the recursively enumerable degrees, involved very complex \({\mathbf O}'''\) methods. The principal novelty of the current paper is that it only uses a fairly straightforward \({\mathbf O}''\) argument involving the coding of finite partial orderings. One then appeals to the Ershov- Taitslin result that the theory of finite partial orderings is strongly undecidable. Three additional remarks seem in order. First, the technique might be much more widely applicable to, for intance, one type in intervals. Secondly, at the time of the writing of this review, this is the only published account of the undecidability of \(\text{Th} ({\mathbf R})\). Finally, as the authors themselves point out, the encoding has apparent limitations in that while it gives undecidability earlier techniques such as Harrington-Slaman and Slaman-Woolin (both unpublished) also enable one to calculate the degree of the theory which seems beyond the scope of the Ambos-Spies Shore method. The paper is very well written.