30 MICHAEL D. FRIED, DAN HARAN, AND HELMUT VOLKLEIN
with conjugacy classes of involutory substructures of G(
tions 8 and 9]).
This includes the definition of Galois stratification and Galois formulas [F
p. 410]. Thus, a real Galois stratification
is a partition of the affine space
as a finite disjoint union
of nonsingular K-basic sets, each of them equipped with a real Galois cover
and a conjugacy domain Con(Ai) in Sub[Ci/Ai, P
The corresponding real
Galois formula is a formal expression
Con(A) with the following
interpretation. For be an extension
Con(Ai) for the unique i such that a
If K is a presented field with elimination theory [F
Definition 17.9], we
get an effective elimination of quantifiers for the theory of real Frobenius fields
in this language. Moreover, every formula in the language .C(K) of rings with
is equivaler1t to a real Galois formula
[FJ, Remark 25.8]).
The corresponding real Galois stratification may satisfy
Conclude the following.
Let K be
presented field with
L of K with
(isomorphism types of) finite involutory structures,
Con(S) in Sub[L/ K]
with the following property.
For every real Frobenius field M that contains K
we have M
In particular, Proposition 9.4 holds for K
10. Model theoretic results.
be a given finite extension of IQ, say as
Z[X] is a given monic irreducible polynomial. Then
is formally real (resp.
!Qtr) if and only if
has a root in IR (resp.
splits over IR). We can
effectively decide whether this condition holds [L, p. 276].
In particular, given a finite Galois extension L of IQ, we can effectively find
the field L
!Qtr and the involutory structure G(L/ L
denote the elementary language of fields with parameters from
THEOREM 10 .1.
The elementary theory of
PROOF. Apply Proposition 9.4. The field !Qtr is real Frobenius (Corollary
8.3) and lmG(!Qtr)
lmD (Corollary 7.7) is the family of finite involutory
structures H in which
is a conjugacy domain in H and H
(Lemma 7.3(b)). Furthermore, if
is a finite Galois extension and