I will only give a proof sketch. Take some
T satisfying the preconditions. We want to define an
L-
structure M=M(M,⋅M) which
satisfies T.
Let
C be the collection of
constant symbols guaranteed to exist by the
witness property. And let
∼ relate two
constant symbols c1,
c2 iff the
sentence c1=c2 is in
T (this is an equiv. relation). Then we define our domain to be
M=C/∼. Also, given a
constant symbol c, denote by
c⋆ the
equivalence class [c]∼.
Now we need to define our interpretation
function ⋅M
For
constant symbols c, just let
cM=c⋆.
For
functions, define that
fM(c1⋆,…,cn⋆)=r⋆ exactly when the
sentence f(c1,…,cn)=r is in
T. This makes sense because the
witness prop guarantees that for each
f,c1,…,cn, exists some
c0 such that
(∃v:f(c1,…,cn)=v)→(f(c1,…,cn)=c0) is in
T.
For relations, define that
(c1⋆,…,cn⋆)∈RM exactly when the
sentence R(c1,…,cn) is in
T.
Note that I’m performing these constructions on
equivalence classes ci⋆, meaning that I need to justify that these definitions are in fact well-
defined. I will not do so, but know that it can be done (in some cases using lemma 1).
Now we have to justify that the constructed
model M satisfies T. We will show something stronger; namely, that for every
formula ϕ=ϕ(v1,…,vn) and
constant symbols c1,…,cn we have:
M⊨ϕ(c1⋆,…,cn⋆) iff ϕ(c1,…,cn)∈T
This is stronger than
M⊨T because
M⊨T requires only
satisfiability on
sentences, but here we show a notion of
satisfiability for
formulas with free variables as well.
We can show this essentially by induction on the stucture of
formulas. I will not give the whole proof, but I will spell out two cases:
The case when
ϕ is a conjunction
ψ1(v1,…,vn)∧ψ2(v1,…,vn).
By induction we know that
M⊨ψ1(c1⋆,…,cn⋆) iff ψ1(c1,…,cn)∈Tand that
M⊨ψ2(c1⋆,…,cn⋆) iff ψ2(c1,…,cn)∈T
Now we want to show that
M⊨ψ1(c1⋆,…,cn⋆)∧ψ2(c1⋆,…,cn⋆) iff ψ1(c1,…,cn)∧ψ2(c1,…,cn)∈T
For direction
⇒, note first that if
M⊨ψ1(c1⋆,…,cn⋆)∧ψ2(c1⋆,…,cn⋆) then both
M⊨ψ1(c1⋆,…,cn⋆) and
M⊨ψ2(c1⋆,…,cn⋆). Then due to the inductive hypothesis we have both that
ψ1(c1,…,cn)∈T and that
ψ2(c1,…,cn)∈T. As such for the
finite subset
T0⊆T defined by
T0={ψ1(c1,…,cn),ψ2(c1,…,cn)} we have that
T0⊨ψ1(c1,…,cn)∧ψ2(c1,…,cn); hence by lemma 1
ψ1(c1,…,cn)∧ψ2(c1,…,cn)∈T.
For direction
⇐, assume that
ψ1(c1⋆,…,cn⋆)∧ψ2(c1⋆,…,cn⋆)∈T. By
finite satisfiability, the subtheory
T0={ψ1(c1,…,cn)∧ψ2(c1⋆,…,cn⋆)} is
satisfiable. Note that
T0⊨ψ1(c1⋆,…,cn⋆) and
T0⊨ψ2(c1⋆,…,cn⋆), so by lemma 1
T satsifies both
sentences as well. Then by the inductive hypothesis we get that
M satisfie both
ψ1(c1,…,cn) and
ψ2(c1,…,cn), meaning that it also
satisfies their conjunction; done.
nb. I think I’m messing up
ci⋆ vs
ci in some places. Oops
The case when
ϕ is an exists
∃w:ψ(c1,…,cn)
JK, don’t wanna do this one. Relevant page is starred in notebook if I feel like going back.