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'

=