Math 1090 A Homework 5 Math 1090 A Homework 5
SOLUTIONS

1. Fill in correct REASONS and complete the following to a proof that
 |-  (("x|:Ax) Ù(AyÞ By)) Þ By  .

 (("x|:Ax) Ù(AyÞ By)) Þ By = á        REASONS        ñ (("x|:Ax)Ùtrue Ù(AyÞ By)) Þ By = á        REASONS         ñ (("x|:Ax)Ù(("x |: Ax)Þ Ay) Ù(AyÞ By)) Þ By

Answer:

 (("x|:Ax) Ù(Ay Þ By)) Þ By = á    (3.39)     ñ (("x|:Ax)Ùtrue Ù(Ay Þ By)) Þ By = á    (9.13)     ñ (("x|:Ax)Ù(("x |: Ax)Þ Ay) Ù(Ay Þ By)) Þ By

This is a theorem as
 |- (P Ù(PÞ Q) Ù(Q Þ R)) Þ R .
A proof can be seen below:

 (P Ù(PÞ Q) Ù(Q Þ R)) Þ R = á    (3.66)     ñ (PÙQ) Ù (Q Þ R) = á    (3.37)     ñ PÙ(Q Ù (Q Þ R) = á    (3.66)     ñ PÙ(Q Ù R) = á    (3.37)     ñ (PÙQ) Ù R Þ á    (3.76)(b)     ñ R

2. Prove (8.18) where * is Ù, i.e.,
 |-  ("x | R ÚS : P) = ("x | R : P) Ù("x | S : P).

Hint: Use (9.2), (3.78), (8.15) for " with R being ``true'', and finally (9.2) again.
Answer:

 ("x | RÚS:P) = á    (9.2)     ñ ("x |:RÚS Þ P) = á    (3.78), Leibniz (8.12)     ñ ("x |:(RÞ P)  Ù(S Þ P)) = á    (8.15)     ñ ("x |:RÞ P)  Ù("x |:SÞ P) = á    (9.2)     ñ ("x | R : P) Ù("x | S : P)

1. Prove
 |- (\$x |:true) = true .
Answer: Start with (9.28) with P being true.

 true Þ (\$x |:true) = á    (3.57)     ñ true Ú(\$x |:true)    º   (\$x |:true) = á    (3.24), (3.29)     ñ true    º   (\$x |:true)

2. Prove
 |- (\$x |: P Þ ("x |:P) ) .
Answer:

 (\$x |: P Þ ("x |:P) ) = á    (3.59)     ñ (\$x |: ØP Ú("x |:P) ) = á    (8.15)     ñ (\$x |: ØP ) Ú(\$x |:("x |:P)) = á    (3.39)     ñ (\$x |: ØP ) Ú(\$x |:("x |:P)Ùtrue) = á    (9.21), Øoccurs(¢x¢,¢("x|:P)¢)     ñ (\$x |: ØP ) Ú( ("x |:P) Ù(\$x |:true )) = á    Part (a)     ñ (\$x |: ØP ) Ú(("x |:P)Ùtrue ) = á    (3.39), (9.18)(c)     ñ Ø("x |:P) Ú("x |:P)

3. Prove
 |- ("x|:Ax) Ú ("x|:Bx)    º   ("x|:("x|:Ax) Ú Bx)
and use to prove
 |- ("x|:Ax) Ú ("x|:Bx)    º   ("x|:("y|:Ay  Ú Bx) ) .
Answer: The proof of the first result is incorporated in the proof of the second.

 ("x|:Ax) Ú ("x|:Bx) = á    (9.5), Øoccurs(¢x¢,¢("x|:Ax)¢)     ñ ("x|:("x|:Ax) Ú Bx) = á    (8.22), Øoccurs(¢y¢,¢Ax¢)     ñ ("x|:("y|:Ay) Ú Bx) = á    (3.36), (9.5), Øoccurs(¢y¢,¢Bx¢)     ñ ("x|:("y|:Ay  Ú Bx)

4. Prove without using (9.13),
 ("x|:P)   º   (" x|:P) Ù  P[x: = a] .
Hint: Use (8.17) and (8.14).
Answer: Note that the symbol a is a constant symbol so that Øoccurs(¢x¢,¢a¢).

 ("x |:P) = á    (3.39)     ñ ("x |x = a  Ú true :P) = á    (8.18)     ñ ("x |x = a : P) Ù("x |true: P) = á    (8.14), Øoccurs(¢x¢,¢a¢)     ñ P[x: = a] Ù("x |:P)

File translated from TEX by TTH, version 2.60.
On 30 Nov 2000, 19:50.