We prove (9.12)

Note that the primary connective is Þ. If it happens that
|- ("x|R:QÞ P), then by Modus Ponens we can
conclude that |- (" x|R:Q) Þ ("x|R:P).
|- ("x|R:QÞ P) Þ ((" x|R:Q) Þ ("x|R:P)) .

so it suffices to prove
("x|R:QÞ P) Þ ((" x|R:Q) Þ ("x|R:P))
=

(3.65)

(("x|R:QÞ P)Ù(" x|R:Q)) Þ ("x|R:P)
|- (("x|R:QÞ P)Ù(" x|R:Q)) Þ ("x|R:P) .

I understand (9.13),
("x|R:QÞ P)Ù(" x|R:Q)
=

(8.15)

("x |R:(Q Þ P) ÙQ)
=

(3.66)

("x |R:Q ÙP)
=

(3.36)

("x |R:PÙQ)
Þ

(9.11)

("x |R:P)

to mean (semantically) that if something holds in general then it
holds in particular. Note that there is no restriction on E.
|- ("x|:P) Þ P[x: = E]

If
it happens that there are no free occurrences of x in E then there
is a simple proof based on (8.14).

The proof without restrictions on x proceeds in a similar fashion
but note the subtle difference.
("x|:P)
=

(3.29)

("x|x = E Útrue:P)
Þ

(9.10)

("x|x = E:P)
=

(8.14)

P[x: = E]

Now what is P[x: = w][w: = E]? w is fresh so P[x: = w] is obtained
simply by replacing all free occurrences of x in P by w. Since
the only w's in P[x: = w] are those which replaced the free
occurrences of x, P[x: = w][w: = E] is the identical expression to
P[x: = E].
("x|:P)
=

w fresh, (8.21)

("w|:P[x: = w])
=

(3.29)

("w|w = E Útrue:P[x: = w])
Þ

(9.10)

("w|w = E :P[x: = w])
=

w d.n.o.f. in E

P[x: = w][w = E]

(9.16) says

It does not make any assertion as to the syntactic equivalence of P
and ("x|:P). By (9.13), keeping in mind that P is just
P[x: = x], we have |- ("x|:P)Þ P. The converse
P Þ ("x|:P) is
P is a theorem if and only if ("x|:P) is a theorem. **not** a theorem as can be
seen by taking the UD to be {0,1}, P to be ``x = 0'' and the
free occurrence of x in P to have value 0.

Assume |- P. Then

Conversely, assume |- ("x |:P). Then as |- ("x|:P) Þ P, by Modus Ponens, |- P.
("x|:P)
=

Metatheorem

("x|:true)

File translated from T

On 21 Nov 2000, 18:42.