PRIMITIVE RECURSIVE DECIDABILITY FOR LARGE RINGS OF ALGEBRAIC INTEGERS

Source abstract

Lou v. d. Dries proves in [Dri88] that the elementary theory Th(ℤ˜) of the ring ℤ˜ of all algebraic integers is decidable. For a prime number p, let 𝔽p(t)˜ be the algebraic closure of 𝔽p(t) and denote the integral closure of 𝔽p[t] in 𝔽p(t)˜ by 𝔽p[t]˜. Lou v. d. Dries and Angus Macintyre prove in [DrM90] that Th(𝔽p[t]˜) is decidable. One of the main results of this work states that both Th(ℤ˜) and Th(𝔽p[t]˜) are primitive recursive. Moreover, let ℚ˜ be the field of all algebraic numbers and let Gal(ℚ)=Gal(ℚ˜/ℚ) be the absolute Galois group of ℚ. For each positive integer e we equip the group Gal(ℚ)e with its unique normalized Haar measure. For each σ=(σ1,…,σe)∈Gal(ℚ)e let ℚ˜(σ) be the fixed field of σ1,…,σe in ℚ˜ and let ℤ˜(σ) be the ring of integers of ℚ˜(σ). Given a sentence θ in the language of rings, we let α be the Haar measure of the set of all σ∈Gal(ℚ)e for which θ holds in ℤ˜(σ). We prove that α is a rational number which can be effectively computed in a primitive recursive way. We prove a similar result also in the function field case.