Galois Stratification

Zusammenfassung

Chapter 25 extends the constructive field theory and algebraic geometry of Chapter 17, in contrast to Chapter 18, to give effective decision procedures through elimination of quantifiers. Such an elimination of quantifiers requires formulas outside of the theory ℰ (ring). We call these more general formulas Galois formulas. These formulas include data for a stratification of the affine space 𝔸ⁿ into K-normal basic sets A; and each coordinate ring K[A] is equipped with a Galois ring cover C and a collection of conjugacy classes Con of subgroups of the Galois group ℰ(K(C)/K(A)) Each successive elimination of a quantifier contributes to the subgroups that appear in Con. In particular, this leads to the primitive recursiveness of the theory of all Frobenius fields which contain a given field K with elimination theory (Theorem 25.11).