Quantifier elimination in separably closed fields of finite imperfectness degree
Dan Haran · Journal of Symbolic Logic · 1988
The theory of separably closed fields of a fixed characteristic and a fixed imperfectness degree is clearly recursively axiomatizable. Ershov [1] showed that it is complete, and therefore decidable. Later it became clear that this theory also has the prime extension property in a suitable language (cf. [4, Proposition 1]); hence it admits quantifier elimination. The purpose of this work is to give an explicit, primitive recursive procedure for such quantifier elimination in the case of a finite imperfectness degree. To be precise, the language ∧ that we have in mind is the first order language of fields enriched with (m + 1)-place function symbols , where m = 0,1,2,… and 1 ≤ j ≤ pm. To interpret in a field M of characteristic p, consider the p-adic expansion of j – 1, and for x1,…,xm Є M let . If x1, …, xm) are p-independent and y Є M is p-dependent on them, then are linearly independent over Mp and y is linearly dependent on them. In this case there are unique such that define . Set otherwise. Denote by SCF(p,e) the theory of separably closed fields of characteristic p and finite imperfectness degree e, containing the above interpretation of the functions .