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)     
    (PQ)  (Q R)
    =    (3.37)     
    P(Q  (Q R)
    =    (3.66)     
    P(Q  R)
    =    (3.37)     
    (PQ)  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:

    ("| RS:P)
    =    (9.2)     
    ("|:RS P)
    =    (3.78), Leibniz (8.12)     
    ("|:(R P)  (S P))
    =    (8.15)     
    ("|:R P)  ("|:S P)
    =    (9.2)     
    ("x | R : P) ("x | S : P)

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

      true ($|:true)
      =    (3.57)     
      true ($|:true)      ($|:true)
      =    (3.24), (3.29)     
      true      ($|:true)

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

      ($|: P ("x |:P) )
      =    (3.59)     
      ($|: P ("x |:P) )
      =    (8.15)     
      ($|: P ) ($|:("x |:P))
      =    (3.39)     
      ($|: P ) ($|:("x |:P)true)
      =    (9.21), occurs(x,("x|:P))     
      ($|: P ) ( ("x |:P) ($|:true ))
      =    Part (a)     
      ($|: 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).

    ("|:P)
    =    (3.39)     
    ("|x = a   true :P)
    =    (8.18)     
    ("|x = a : P) ("|true: P)
    =    (8.14), occurs(x,a)     
    P[x: = a] ("|:P)


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