(1 ⇒ 2) Assume
ϕ QE and take
M,N,A,a.
Assume
M⊨ϕ(a). Then
M⊨ψ(a) for
ψ the guaranteed quantifier-elimination of
ϕ. So
A⊨ψ(a) since
A is a
substructure of
M and
ψ is
qf. Likewise,
N⊨ψ(a). Then
N⊨ϕ(a). (The other direction proceeds similarly)
(2 ⇒ 1) Assume
T meets the preconditions.
Take some
formula ϕ=ϕ(v). We want to eliminate the quantifiers of
ϕ.
Given some tuple
x of
terms, let
Γ(x) be all those
qf sentences ψ(x) implied by
ϕ(x); ie,
Γ(x):={ψ(x):ψ qf. and T⊨(∀y:ϕ(y)→ψ(x))}
Let
c be a tuple of new
constant symbols of the same length as
v. I claim (proven below) that
T∪Γ(c)⊨ϕ(c). Hence by
compactness there is some
finite subset of
T∪Γ(c) implying
ϕ(c). Thus for some
ψ1 … ψn∈Γ(c) we know
T⊨(n⋀ψn(c)→ϕ(c))
Note that we know nothing about these
constant symbols; ie, no assumptions are made about them. So by a metatheorem of
first-order logic we can strengthen this to:
T⊨∀x(n⋀ψn(x)→ϕ(x))
And we already know that
ϕ implies each
ψ, so we can make the implication a biconditional and conclude:
T⊨∀x(n⋀ψn(x)⟷ϕ(x))
So the conjunction
⋀nψn is a quantifier elimination for
ϕ. Done!
Just kidding. We still need to show the claim.
Claim. T∪Γ(c)⊨ϕ(c). Well, suppose for contradiction that this isn’t the case. Then
T∪Γ(c)∪{¬ϕ(c)} is
satisfiable; let
M be a
model, and let
A be the
substructure of
M whose domain consists only of interpretations for
c.
Let
Σ=T∪Diag(A)∪{ϕ(c)}. Assume for contradiction that
Σ is unsatisfiable. Then
T∪Diag(A)⊨¬ϕ(c), so by
compactness exists
ψ1 … ψn∈Diag(A) for which
T⊨n⋀ψn→¬ϕ(c)
Recall that domain of
A includes only interpretations of
constant symbols in
c. Let us reconsider each
sentence ψn∈Diag(A) as a
formula ψn′=ψn′(b) where
ψn′ is
ψ but with
constant symbols replaced by free variables. Then we have:
T⊨n⋀ψn′(c)→¬ϕ(c)
And by the same metatheorem as above we can strengthen this to
T⊨∀x(n⋀ψ′(x)→¬ϕ(x))
So by contrapositive
T⊨∀x(ϕ(x)→n⋁¬ψ′(x))
Hence for any
x we have that
Γ(x) contains
⋁n¬ψ′(x). Since
A⊆M⊨Γ(c), we conclude that
A⊨n⋁¬ψ′(c)
Which is not true. Contradiction. Discharging the contradiction, we conclude that
Σ is satsifiable.
Let
N be a
model of
Σ. Then
N⊨Diag(A), so by a theorem of
diagrams A injects into
N. But
N⊨ϕ(c) and
A⊆M⊨¬ϕ(c). Hence
N⊨(ϕ(c)∧¬ϕ(c)), contradiction!
Discharge the contradiction and we are done.