November 22, 2000 November 22, 2000

We prove (9.12)
 |- ("x|R:QÞ P)    Þ    ((" x|R:Q) Þ ("x|R:P)) .
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))
 =

 (3.65)

 (("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) .

 ("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)
I understand (9.13),
 |- ("x|:P) Þ P[x: = E]
to mean (semantically) that if something holds in general then it holds in particular. Note that there is no restriction on E.
If it happens that there are no free occurrences of x in E then there is a simple proof based on (8.14).
 ("x|:P)
 =

 (3.29)

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

 (9.10)

 ("x|x = E:P)
 =

 (8.14)

 P[x: = E]
The proof without restrictions on x proceeds in a similar fashion but note the subtle difference.
 ("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]
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].
(9.16) says
 P is a theorem if and only if ("x|:P) is a theorem.
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 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
 ("x|:P)
 =

 Metatheorem

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

File translated from TEX by TTH, version 2.60.
On 21 Nov 2000, 18:42.