The complexity of classical theorems on saturated models
Robert Irving Soare, Kenneth D. Harris · 2007
We investigate the computational complexity (as calibrated in computability theory) and the proof-theoretic complexity (as calibrated in reverse mathematics) of Vaught's Theorem on the existence and uniqueness of saturated models for complete theories. We define a saturated bounding degree as a Turing degree which can compute a saturated model for any complete and decidable theory whose types are all computable. We show as an upper-bound that any high degree and any degree of a completion of Peano arithmetic are saturated bounding. We show as a lower-bound that for no n is a low n degree saturated bounding. Our investigation led to a new characterization of the low n hierarchy by means of the difficulty of finding escape functions. By Martin's theorem a degree is non-high if for any function computable in the degree there is a computable function which escapes domination (by infinitely often growing at least as large.) We show that a degree is low if and only if escape functions can be effectively produced. We generalize this property to provide a characterization of the lown degrees. We show that Vaught's Theorem, suitably stated in reverse mathematics, is equivalent to ATR0 over ACA0; and that the statement of the uniqueness of saturated models, as well as the statement that saturated models are universal, are equivalent to ACA0 over RCA0.