Exercise 8.8

Leaving aside the argument about axioms by definition not requiring proof…

Axiom 3:

(r1 `Intersect` (r2 `Union` r3)) `containsR` p
=> (r1 `containsR` p) && ((r2 `Union` r3) `containsR` p)
=> (r1 `containsR` p) && ((r2 `containsR` p) || (r3 `containsR` p))
=> ((r1 `containsR` p) && (r2 `containsR` p))
  || ((r1 `containsR` p) && (r3 `containsR` p))
=> ((r1 `Intersect` r2) `containsR` p) || ((r1 `Intersect` r3) `containsR` p)
=> ((r1 `Intersect` r2) `Union` (r1 `Intersect` r3)) `containsR` p
 
∴ (r1 `Intersect` (r2 `Union` r3))((r1 `Intersect` r2) `Union` (r1 `Intersect` r3))
 
(r1 `Union` (r2 `Intersect` r3)) `containsR` p
=> (r1 `containsR` p) || ((r2 `Intersect` r3) `containsR` p)
=> (r1 `containsR` p) || ((r2 `containsR` p) && (r3 `containsR` p))
=> ((r1 `containsR` p) || (r2 `containsR` p))
  && ((r1 `containsR` p) || (r3 `containsR` p))
=> ((r1 `Union` r2) `containsR` p) && ((r1 `Union` r3) `containsR` p)
=> ((r1 `Union` r2) `Intersect` (r1 `Union` r3)) `containsR` p
 
∴ (r1 `Union` (r2 `Intersect` r3))((r1 `Union` r2) `Intersect` (r1 `Union` r3))

Axiom 4:

univ = Complement Empty
 
(r `Union` Empty) `containsR` p
=> (r `containsR` p) || (Empty `containsR` p)
=> (r `containsR` p) || False
=> r `containsR` p
 
∴ (r `Union` Empty) ≡ r
 
(r `Intersect` univ) `containsR` p
=> (r `Intersect` Complement Empty) `containsR` p
=> (r `containsR` p) && (Complement Empty `containsR` p)
=> (r `containsR` p) && not (Empty `containsR` p)
=> (r `containsR` p) && not False
=> (r `containsR` p) && True
=> r `containsR` p
 
∴ (r `Intersect` univ) ≡ r

Axiom 5:

(r `Union` Complement r) `containsR` p
=> (r `containsR` p) || (Complement r `containsR` p)
=> (r `containsR` p) || not (r `containsR` p)
=> True
=> not False
=> not (Empty `containsR` p)
=> Complement Empty `containsR` p
=> univ `containsR` p
 
∴ (r `Union` Complement r) ≡ univ
 
(r `Intersect` Complement r) `containsR` p
=> (r `containsR` p) && (Complement r `containsR` p)
=> (r `containsR` p) && not (r `containsR` p)
=> False
=> Empty `containsR` p
 
∴ (r `Intersect` Complement r) ≡ Empty

Leave a Reply