30 MICHAEL D. FRIED, DAN HARAN, AND HELMUT VOLKLEIN
with conjugacy classes of involutory substructures of G(
Cd
Ai) (
cf. [HL,
Sec-
tions 8 and 9]).
This includes the definition of Galois stratification and Galois formulas [F
J,
p. 410]. Thus, a real Galois stratification
is a partition of the affine space
An
over
K
as a finite disjoint union
An
=
UiEI
Ai
of nonsingular K-basic sets, each of them equipped with a real Galois cover
Cd
Ai
and a conjugacy domain Con(Ai) in Sub[Ci/Ai, P
0].
The corresponding real
Galois formula is a formal expression
Ar(A,
X)
~
Con(A) with the following
interpretation. For be an extension
M
of Kanda
E
Mn
write
M
f=
Ar(A,
a)
~
Con(A) if
Ar(Ai,
a)
~
Con(Ai) for the unique i such that a
E
Ai(M).
If K is a presented field with elimination theory [F
J,
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
parameters from
K
is equivaler1t to a real Galois formula
(cf.
[FJ, Remark 25.8]).
The corresponding real Galois stratification may satisfy
Ci
=
K[Ai][AJ, for
each i
E
I.
Conclude the following.
PROPOSITION 9.4
[HL,
Theorem 9.2(a)J.
Let K be
a
presented field with
elimination
theory,
and
let
'13
be
a
sentence
in .C(K).
We
can
effectively find
a
finite Galois
extension
L of K with
A
E
L,
a
finite
family
1t
2
Sub[L/ K]
of
(isomorphism types of) finite involutory structures,
and
for
each
S
~
1t
a con-
jugacy
domain
Con(S) in Sub[L/ K]
contained
inS
with the following property.
For every real Frobenius field M that contains K
and
satisfies
ImG(M)
n1t
=
S
we have M
f=
'13
if
and
only ifresLG(M)
E
Con(S).
In particular, Proposition 9.4 holds for K
=
IQ.
10. Model theoretic results.
Let
K'
be a given finite extension of IQ, say as
K'
=
IQ[X]/(f), where
f
E
Z[X] is a given monic irreducible polynomial. Then
K'
is formally real (resp.
K'
~
!Qtr) if and only if
f
has a root in IR (resp.
f
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
n
!Qtr and the involutory structure G(L/ L
n
!Qtr).
Let
.C(K)
denote the elementary language of fields with parameters from
K.
THEOREM 10 .1.
The elementary theory of
!Qtr is
effectively
decidable.
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
IH
=/=
0
is a conjugacy domain in H and H
=
(IH)
(Lemma 7.3(b)). Furthermore, if
L/IQ
is a finite Galois extension and
K'
=
Previous Page Next Page