[<< wikibooks] Logic for Computer Scientists/Predicate Logic/Equivalence and Normal Forms
== Equivalence and Normal Forms ==
Equivalence of formulae is defined as in the propositional case:

== Definition 6 ==
The formulae

F

{\displaystyle F}
and

G

{\displaystyle G}
are called (semantically)
equivalent, if for all interpretations

I

{\displaystyle {\mathcal {I}}}
for

F

{\displaystyle F}
and

G

{\displaystyle G}
,

I

(
F
)
=

I

(
G
)

{\displaystyle {\mathcal {I}}(F)={\mathcal {I}}(G)}
. We write

F
≡
G

{\displaystyle F\equiv G}
.
The equivalences from  the propositional case in theorem 4
equivalences hold and in addition we have the following
cases for quantifiers.

== Theorem 1 ==
The following equivalences hold:

¬
∀
x
F

{\displaystyle \lnot \forall xF}

≡

{\displaystyle \equiv }

∃
x
¬
F

{\displaystyle \exists x\lnot F}

¬
∃
x
F

{\displaystyle \lnot \exists xF}

≡

{\displaystyle \equiv }

∀
x
¬
F

{\displaystyle \forall x\lnot F}

If

x

{\displaystyle x}
does not occur free in

G

{\displaystyle G}
:

∀
x
F
∧
G

{\displaystyle \forall xF\land G}

≡

{\displaystyle \equiv }

∀
x
(
F
∧
G
)

{\displaystyle \forall x(F\land G)}

∀
x
F
∨
G

{\displaystyle \forall xF\lor G}

≡

{\displaystyle \equiv }

∀
x
(
F
∨
G
)

{\displaystyle \forall x(F\lor G)}

∃
x
F
∧
G

{\displaystyle \exists xF\land G}

≡

{\displaystyle \equiv }

∃
x
(
F
∧
G
)

{\displaystyle \exists x(F\land G)}

∃
x
F
∨
G

{\displaystyle \exists xF\lor G}

≡

{\displaystyle \equiv }

∃
x
(
F
∨
G
)

{\displaystyle \exists x(F\lor G)}

∀
x
F
∧
∀
x
G

{\displaystyle \forall xF\land \forall xG}

≡

{\displaystyle \equiv }

∀
x
(
F
∧
G
)

{\displaystyle \forall x(F\land G)}

∃
x
F
∨
∃
x
G

{\displaystyle \exists xF\lor \exists xG}

≡

{\displaystyle \equiv }

∃
x
(
F
∨
G
)

{\displaystyle \exists x(F\lor G)}

∀
x
∀
y

F

{\displaystyle \forall x\forall y\;F}

≡

{\displaystyle \equiv }

∀
y
∀
x
F

{\displaystyle \forall y\forall xF}

∃
x
∃
y

F

{\displaystyle \exists x\exists y\;F}

≡

{\displaystyle \equiv }

∃
y
∃
x
F

{\displaystyle \exists y\exists xF}

Proof: We will prove only  the equivalence

∀
x
F
∧
G
≡
∀
x
(
F
∧
G
)

{\displaystyle \forall xF\land G\equiv \forall x(F\land G)}

with

x

{\displaystyle x}
has no free occurrence in

G

{\displaystyle G}
, as an example.
Assume an interpretation

I

=
(
U
,

A

)

{\displaystyle {\mathcal {I}}=(U,{\mathcal {A}})}
such that

I

(
∀
x
F
∧
G
)
=
t
r
u
e

{\displaystyle {\mathcal {I}}(\forall xF\land G)=true}

iff

I

(
∀
x
F
)
=
t
r
u
e

and

I

(
G
)
=
t
r
u
e

{\displaystyle {\text{iff }}{\mathcal {I}}(\forall xF)=true{\text{ and }}{\mathcal {I}}(G)=true}

iff

for all

d
∈
U
:

I

[
x

/

d
]

(
F
)
=
t
r
u
e

and

I

(
G
)
=
t
r
u
e

{\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}(G)=true}

iff

for all

d
∈
U
:

I

[
x

/

d
]

(
F
)
=
t
r
u
e

and

I

[
x

/

d
]

(
G
)
=
t
r
u
e

(x = does not occur free in = G)

{\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}_{[x/d]}(G)=true{\text{ (x = does not occur free in = G)}}}

iff

for all

d
∈
U
:

I

[
x

/

d
]

(
(
F
∧
G
)
)
=
t
r
u
e

{\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}((F\land G))=true}

iff

I

(
∀
x
(
F
∧
G
)
)
=
t
r
u
e
.

{\displaystyle {\text{iff }}{\mathcal {I}}(\forall x(F\land G))=true.}

Note that the following symmetric cases do not hold:

∀
x
F
∨
∀
x
G

{\displaystyle \forall xF\lor \forall xG}
is not equivalent to

∀
x
(
F
∨
G
)

{\displaystyle \forall x(F\lor G)}

∃
x
F
∧
∃
x
G

{\displaystyle \exists xF\land \exists xG}
is not equivalent to

∃
x
(
F
∧
G
)

{\displaystyle \exists x(F\land G)}

The theorem for substituitivity holds as in the propositional case.
Example: Let us transform the following formulae by means of
substituitivity and the equivalences from theorem 1:

(
¬
(
∃
x
P
(
x
,
y
)
∨
∀
z
Q
(
z
)
)
∧
∃
w
P
(
f
(
a
,
w
)
)
)

{\displaystyle (\lnot (\exists xP(x,y)\lor \forall zQ(z))\land \exists wP(f(a,w)))}

≡
(
(
¬
∃
x
P
(
x
,
y
)
∧
¬
∀
z
Q
(
z
)
)
∧
∃
w
P
(
f
(
a
,
w
)
)
)

{\displaystyle \equiv ((\lnot \exists xP(x,y)\land \lnot \forall zQ(z))\land \exists wP(f(a,w)))}

≡
(
(
∀
x
¬
P
(
x
,
y
)
∧
∃
z
¬
Q
(
z
)
)
∧
∃
w
P
(
f
(
a
,
w
)
)
)

{\displaystyle \equiv ((\forall x\lnot P(x,y)\land \exists z\lnot Q(z))\land \exists wP(f(a,w)))}

≡
(
∃
w
P
(
f
(
a
,
w
)
)
∧
(
∀
x
¬
P
(
x
,
y
)
∧
∃
z
¬
Q
(
z
)
)
)

{\displaystyle \equiv (\exists wP(f(a,w))\land (\forall x\lnot P(x,y)\land \exists z\lnot Q(z)))}

≡
∃
w
(
P
(
f
(
a
,
w
)
)
∧
∀
x
(
¬
P
(
x
,
y
)
∧
∃
z
¬
Q
(
z
)
)
)

{\displaystyle \equiv \exists w(P(f(a,w))\land \forall x(\lnot P(x,y)\land \exists z\lnot Q(z)))}

≡
∃
w
(
∀
x
(
∃
z
¬
Q
(
z
)
∧
¬
P
(
x
,
y
)
)
∧
P
(
f
(
a
,
w
)
)
)

{\displaystyle \equiv \exists w(\forall x(\exists z\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}

≡
∃
w
(
∀
x
∃
z
(
¬
Q
(
z
)
∧
¬
P
(
x
,
y
)
)
∧
P
(
f
(
a
,
w
)
)
)

{\displaystyle \equiv \exists w(\forall x\exists z(\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}

≡
∃
w
∀
x
∃
z
(
(
¬
Q
(
z
)
∧
¬
P
(
x
,
y
)
)
∧
P
(
f
(
a
,
w
)
)
)

{\displaystyle \equiv \exists w\forall x\exists z((\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}

== Definition 7 ==
Let

F

{\displaystyle F}
be a formula,

x

{\displaystyle x}
a variable and

t

{\displaystyle t}
a term.

F
[
x

/

t
]

{\displaystyle F[x/t]}
is
obtained from

F

{\displaystyle F}
by substituting every free occurrence of

x

{\displaystyle x}
by

t

{\displaystyle t}
.
Note, that this notion can be iterated:

F
[
x

/

t

1

]
[
y

/

t

2

]

{\displaystyle F[x/t_{1}][y/t_{2}]}
and that

t

1

{\displaystyle t_{1}}
may contain free occurrences of

y

{\displaystyle y}
.

== Lemma 1 ==
Let

F

{\displaystyle F}
be a formula,

x

{\displaystyle x}
a variable and

t

{\displaystyle t}
a term.

I

(
F
[
x

/

t
]
)
=

I

[
x

/

I

(
t
)
]

(
F
)

{\displaystyle {\mathcal {I}}(F[x/t])={\mathcal {I}}_{[x/{\mathcal {I}}(t)]}(F)}

== Lemma 2 (Bounded Renaming) ==
Let

F
=
Q
x
G

{\displaystyle F=QxG}
be a formula, where

Q
∈
{
∀
,
∃
}

{\displaystyle Q\in \{\forall ,\exists \}}
and

y

{\displaystyle y}
a variable without an occurrence in

G

{\displaystyle G}
, then

F
≡
Q
y
G
[
x

/

y
]

{\displaystyle F\equiv QyG[x/y]}

== Definition 8 ==
A formula is called proper if there is no variable which
occurs bound and free and after every quantifier there is a distinct
variable.

== Lemma 3 (Proper Formula) ==
For every formula

F

{\displaystyle F}
there is a formula

G

{\displaystyle G}
which is proper and
equivalent to

F

{\displaystyle F}
.
Proof: Follows immediately by bounded renaming.

Example:

F
=
∀
x
∃
y

p
(
x
,
f
(
y
)
)
∧
∀
x
(
q
(
x
,
y
)
∨
r
(
x
)
)

{\displaystyle F=\forall x\exists y\;p(x,f(y))\land \forall x(q(x,y)\lor r(x))}
has the equivalent and proper formula

G
=
∀
x
∃
y

(
p
(
x
,
f
(
y
)
)
)
∧
∀
z
(
q
(
z
,
u
)
∨
r
(
z
)

{\displaystyle G=\forall x\exists y\;(p(x,f(y)))\land \forall z(q(z,u)\lor r(z)}

== Definition 9 ==
A formula is called in prenex form if it has the form

Q

1

⋯

Q

n

F

{\displaystyle Q_{1}\cdots Q_{n}F}
, where

Q

i

∈
{
∀
,
∃
}

{\displaystyle Q_{i}\in \{\forall ,\exists \}}
with no
occurrences of a quantifier in

F

{\displaystyle F}

== Theorem 2 ==
For every formula there is a proper formula in prenex form, which is
equivalent.

Example:

∀
x
∃
y

(
p
(
x
,
g
(
y
,
f
(
x
)
)
)
∨
¬
q
(
z
)
)
∨
¬
∀
x

r
(
x
,
z
)

{\displaystyle \forall x\exists y\;(p(x,g(y,f(x)))\lor \lnot q(z))\lor \lnot \forall x\;r(x,z)}

∀
x
∃
y

(
p
(
x
,
g
(
y
,
f
(
x
)
)
∨
¬
q
(
z
)
)
∨
∃
x

¬
r
(
x
,
z
)

{\displaystyle \forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists x\;\lnot r(x,z)}

∀
x
∃
y

(
p
(
x
,
g
(
y
,
f
(
x
)
)
∨
¬
q
(
z
)
)
∨
∃
v
¬
r
(
v
,
z
)

{\displaystyle \forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists v\lnot r(v,z)}

∀
x
∃
y
∃
v

(
p
(
x
,
g
(
y
,
f
(
x
)
)
∨
¬
q
(
z
)
)
∨
¬
r
(
v
,
z
)

{\displaystyle \forall x\exists y\exists v\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \lnot r(v,z)}

Proof: Induction over the structure of the formula gives us
the theorem for an atomic formula immediately.

F
=
¬

F

0

{\displaystyle F=\lnot F_{0}}
: There is a

G

0

=

Q

1

y

1

⋯

Q

n

y

n

G
′

{\displaystyle G_{0}=Q_{1}y_{1}\cdots Q_{n}y_{n}G'}
with

Q

i

∈
{
∀
,
∃
}

{\displaystyle Q_{i}\in \{\forall ,\exists \}}
, which is equivalent to

F

0

{\displaystyle F_{0}}
. Hence we have

F
≡

Q

1

¯

y

1

⋯

Q

n

¯

y

n

¬

G
′

{\displaystyle F\equiv {\overline {Q_{1}}}y_{1}\cdots {\overline {Q_{n}}}y_{n}\lnot G'}
where

Q

i

¯

=

{

∃

i
f

Q

i

=
∀

∀

i
f

Q

i

=
∃

{\displaystyle {\overline {Q_{i}}}={\begin{cases}\;\;\,\exists &ifQ_{i}=\forall \\\;\;\,\forall &ifQ_{i}=\exists \end{cases}}}

F
=

F

1

∘

F

2

{\displaystyle F=F_{1}\circ F_{2}}
with

∘
∈
{
∧
,
∨
}

{\displaystyle \circ \in \{\land ,\lor \}}
. There exists

G

1

,

G

2

{\displaystyle G_{1},G_{2}}
which are proper and in prenex form and

G

1

≡

F

1

{\displaystyle G_{1}\equiv F_{1}}
and

G

2

≡

F

2

{\displaystyle G_{2}\equiv F_{2}}
. With bounded renaming we can construct

G

1

=

Q

1

y

1

⋯

Q

k

y

k

G

1

′

{\displaystyle G_{1}=Q_{1}y_{1}\cdots Q_{k}y_{k}G_{1}'}

G

2

=

Q

1

′

z

1

⋯

Q

l

′

z

l

G

2

′

{\displaystyle G_{2}=Q_{1}'z_{1}\cdots Q_{l}'z_{l}G_{2}'}

where

{

y

1

,
⋯
,

y

n

}
∩
{

z

1

,
⋯
,

z

l

}
=
∅

{\displaystyle \{y_{1},\cdots ,y_{n}\}\cap \{z_{1},\cdots ,z_{l}\}=\emptyset }
and hence

F
≡

Q

1

y

1

⋯

Q

k

y

k

Q

1

′

z

1

⋯

Q

l

′

z

l

(

G

1

′

∘

G

2

′

)

{\displaystyle F\equiv Q_{1}y_{1}\cdots Q_{k}y_{k}Q_{1}'z_{1}\cdots Q_{l}'z_{l}(G_{1}'\circ G_{2}')}

In the following we call proper formulae in prenex form PP-formulae or PPF’s.

== Definition 10 ==
Let

F

{\displaystyle F}
be a PPF. While

F

{\displaystyle F}
contains a

∃

{\displaystyle \exists }
-Quantifier, do the
following transformation:

F

{\displaystyle F}
has the form

∀

y

1

,
⋯
∀

y

n

∃
z

G

{\displaystyle \forall y_{1},\cdots \forall y_{n}\exists z\;G}

where

G

{\displaystyle G}
is a PPF and

f

{\displaystyle f}
is a

n

{\displaystyle n}
-ary function symbol, which does
not occur in

G

{\displaystyle G}
.
Let

F

{\displaystyle F}
be

∀

y

1

,
⋯
∀

y

n

G
[
z

/

f
(

y

1

,
⋯
,

y

n

)
]

{\displaystyle \forall y_{1},\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})]}

If there exists no more

∃

{\displaystyle \exists }
-quantifier,

F

{\displaystyle F}
is  in
Skolem form.

== Theorem 3 ==
Let

F

{\displaystyle F}
be a PPF.

F

{\displaystyle F}
is satisfiable iff the Skolem form of

F

{\displaystyle F}
is
satisfiable.
Proof: Let

F
=
∀

y

1

⋯
∀

y

n

∃
z

G

{\displaystyle F=\forall y_{1}\cdots \forall y_{n}\exists z\;G}
; after one
transformation according to the while-loop we have

F
′

=
∀

y

1

⋯
∀

y

n

G
[
z

/

f
(

y

1

,
⋯
,

y

n

)

{\displaystyle F'=\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})}
where

f

{\displaystyle f}
is a new function symbol.
We have to prove that this transformation is satisfiability
preserving:
Assume

F
′

{\displaystyle F'}
is satisfiable. than there exists a model

I

{\displaystyle {\mathcal {I}}}
for

F
′

{\displaystyle F'}

I

{\displaystyle {\mathcal {I}}}
is an interpretation for

F

{\displaystyle F}
. From the model
property we have for all

u

1

,
⋯
,

u

n

∈

U

I

{\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}

I

[

y

1

/

u

1

]
⋯
[

y

n

/

u

n

]

(
G
[
z

/

f
(

y

1

,
⋯
,

y

n

)
]
)
=
t
r
u
e

{\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f(y_{1},\cdots ,y_{n})])=true}
From Lemma 1 we conclude

I

[

y

1

/

u

1

]
⋯
[

y

n

/

u

n

]
[
z

/

v
]

(
G
)
=
t
r
u
e

{\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}
where

v
=

I

(
f
(

u

1

,
⋯
,

u

n

)

{\displaystyle v={\mathcal {I}}(f(u_{1},\cdots ,u_{n})}
. Hence we have, that for all

u

1

,
⋯
,

u

n

∈

U

I

{\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}
there is  a

v
∈

U

I

{\displaystyle v\in U_{\mathcal {I}}}
, where

I

[

y

1

/

u

1

]
⋯
[

y

n

/

u

n

]
[
z

/

v
]

(
G
)
=
t
r
u
e

{\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}
and hence we have, that

I

(
∀

y

1

⋯
∀

y

n

∃
z

G
)
=
t
r
u
e

{\displaystyle {\mathcal {I}}(\forall y_{1}\cdots \forall y_{n}\exists z\;G)=true}
, which
means, that

I

{\displaystyle {\mathcal {I}}}
is a model for

F

{\displaystyle F}
.
For the opposite direction of the theorem, assume that

F

{\displaystyle F}
has a
model

I

{\displaystyle {\mathcal {I}}}
. Then we have, that for all

u

1

,
⋯
,

u

n

∈

U

I

{\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}
,
there is  a

v
∈

U

I

{\displaystyle v\in U_{\mathcal {I}}}
, where

I

[

y

1

/

u

1

]
⋯
[

y

n

/

u

n

]
[
z

/

v
]

(
G
)
=
t
r
u
e

{\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}
Let

I
′

{\displaystyle {\mathcal {I'}}}
be an interpretation, which deviates from

I

{\displaystyle {\mathcal {I}}}
only, by the
fact that it is defined for the function symbol

f

{\displaystyle f}
, where

I

{\displaystyle {\mathcal {I}}}
is
not defined. We assume that

f

I

′

(

u

1

,
⋯
,

u

n

)
=
v

{\displaystyle f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})=v}
, where

v

{\displaystyle v}

is chosen according to the above equation.
Hence we have that for all

u

1

,
⋯
,

u

n

∈

U

I

′

{\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}'}

I

[

y

1

/

u

1

]
⋯
[

y

n

/

u

n

]
[
z

/

f

I

′

(

u

1

,
⋯
,

u

n

)
]

′

(
G
)
=
t
r
u
e

{\displaystyle {\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})]}(G)=true}
and from Lemma 1 we conclude that for all

u

1

,
⋯
,

u

n

∈

U

I

{\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}

I

[

y

1

/

u

1

]
⋯
[

y

n

/

u

n

]

′

(
G
[
z

/

f

(

y

1

,
⋯
,

y

n

)
]
)
=
t
r
u
e

{\displaystyle {\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f^{(}y_{1},\cdots ,y_{n})])=true}
which means, that

I

′

(
∀

y

1

⋯
∀

y

n

G
[
z

/

f
(

y

1

,
⋯
,

y

n

)
]
)
=
t
r
u
e

{\displaystyle {\mathcal {I}}'(\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})])=true}
, and hence

I

′

{\displaystyle {\mathcal {I}}'}
is a model for

F
′

{\displaystyle F'}
.

The above results can be used to transform a Formula into a set of
clauses, its clause normal form:

== Problems ==

==== Problem 6 (Predicate) ====
Let

F

{\displaystyle F}
be  a formula,

x

{\displaystyle x}
a variable and

t

{\displaystyle t}
a term. Then

F
[
x

/

t
]

{\displaystyle F[x/t]}
denotes the formula which results from

F

{\displaystyle F}
by replacing  every free
occurrence of

x

{\displaystyle x}
by

t

{\displaystyle t}
. Give a formal definition of this three argument function

F
[
x

/

t
]

{\displaystyle F[x/t]}
,  by induction over  the structure of
the formula

F

{\displaystyle F}
.

◻

{\displaystyle \Box }

==== Problem 7 (Predicate) ====
Show the following semantic equivalences:

∀
x
(
p
(
x
)
→
(
q
(
x
)
∧
r
(
x
)
)
)
≡
∀
x
(
p
(
x
)
→
q
(
x
)
)
∧
∀
x
(
p
(
x
)
→
r
(
x
)
)

{\displaystyle \forall x(p(x)\to (q(x)\land r(x)))\equiv \forall x(p(x)\to q(x))\land \forall x(p(x)\to r(x))}

∀
x
(
p
(
x
)
→
(
q
(
x
)
∨
r
(
x
)
)
)
≢
∀
x
(
p
(
x
)
→
q
(
x
)
)
∨
∀
x
(
p
(
x
)
→
r
(
x
)
)

{\displaystyle \forall x(p(x)\to (q(x)\lor r(x)))\not \equiv \forall x(p(x)\to q(x))\lor \forall x(p(x)\to r(x))}

◻

{\displaystyle \Box }

==== Problem 8 (Predicate) ====
Show the following semantic equivalences:

(
∀
x
p
(
x
)
)
→
q
(
b
)
≡
∃
x
(
p
(
x
)
→
q
(
b
)
)

{\displaystyle (\forall xp(x))\to q(b)\equiv \exists x(p(x)\to q(b))}

(
∀
x
r
(
x
)
)
∨
(
∃
y
¬
r
(
y
)
)
≡
(
∀
x
r
(
x
)
)
→
(
∃
y
r
(
y
)
)

{\displaystyle (\forall xr(x))\lor (\exists y\lnot r(y))\equiv (\forall xr(x))\to (\exists yr(y))}

◻

{\displaystyle \Box }

==== Problem 9 (Predicate) ====
Show that for arbitrary formulae

F

{\displaystyle F}
and

G

{\displaystyle G}
, the following holds:

∀
x
(
F
∨
G
)
≢
∀
x
F
∨
∀
x
G

{\displaystyle \forall x(F\lor G)\not \equiv \forall xF\lor \forall xG}

If

G
=
F
[
x

/

t
]

{\displaystyle G=F[x/t]}
, than

G
⊨
∃
x
F

{\displaystyle G\models \exists xF}
.

◻

{\displaystyle \Box }