Advertisement
Guest User

Untitled

a guest
Nov 18th, 2019
52
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 8.96 KB | None | 0 0
  1. Theorem “`Id` is reflexive”: is-reflexive Id
  2. Proof:
  3. is-reflexive Id
  4. ≡⟨ “Definition of reflexivity” ⟩
  5. ∀ x • x ⦗ Id ⦘ x
  6. ≡⟨ Subproof:
  7. For any `x`:
  8. x ⦗ Id ⦘ x
  9. ≡⟨ “Relationship via `Id`” ⟩
  10. x = x — This is 【 “Reflexivity of =” 】
  11. true
  12.  
  13. Theorem “`Id` is reflexive”: is-reflexive Id
  14. Proof:
  15. Using “Definition of reflexivity”:
  16. Subproof for `∀ x • x ⦗ Id ⦘ x`:
  17. For any `x`:
  18. x ⦗ Id ⦘ x
  19. ≡⟨ “Relationship via `Id`” ⟩
  20. x = x — This is “Reflexivity of =”
  21.  
  22. Theorem “`Id` is reflexive”: is-reflexive Id
  23. Proof:
  24. Using “Definition of reflexivity”:
  25. Subproof:
  26. For any `x`:
  27. x ⦗ Id ⦘ x
  28. ≡⟨ “Relationship via `Id`” ⟩
  29. x = x — This is “Reflexivity of =”
  30.  
  31. Theorem “`Id` is reflexive”: is-reflexive Id
  32. Proof:
  33. Using “Definition of reflexivity”:
  34. For any `x`:
  35. x ⦗ Id ⦘ x
  36. ≡⟨ “Relationship via `Id`” ⟩
  37. x = x — This is “Reflexivity of =”
  38.  
  39. Theorem “Reflexivity”: is-reflexive R ≡ Id ⊆ R
  40. Proof:
  41. Id ⊆ R
  42. ≡⟨ “Relation inclusion” ⟩
  43. ∀ x • ∀ y ❙ x ⦗ Id ⦘ y • x ⦗ R ⦘ y
  44. ≡⟨ “Relationship via `Id`” ⟩
  45. ∀ x • ∀ y ❙ x = y • x ⦗ R ⦘ y
  46. ≡⟨ “One-point rule for ∀” ⟩
  47. ∀ x • (x ⦗ R ⦘ y)[y ≔ x]
  48. ≡⟨ Substitution ⟩
  49. ∀ x • (x ⦗ R ⦘ x)
  50. ≡⟨ “Definition of reflexivity” ⟩
  51. is-reflexive R
  52.  
  53. Theorem “Composition of reflexive relations”:
  54. is-reflexive R ⇒ is-reflexive S ⇒ is-reflexive (R ⨾ S)
  55. Proof:
  56. Assuming `is-reflexive R`:
  57. Assuming `is-reflexive S`:
  58. Using “Definition of reflexivity”:
  59. For any `x`:
  60. x ⦗ R ⨾ S ⦘ x
  61. ≡⟨ “Relation composition” ⟩
  62. ∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x
  63. ⇐⟨ “∃-Introduction” ⟩
  64. (x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x)[b ≔ x]
  65. ≡⟨ Substitution ⟩
  66. (x ⦗ R ⦘ x ∧ x ⦗ S ⦘ x)
  67. ≡⟨ Assumption `is-reflexive R` with “Definition of reflexivity” ⟩
  68. true ∧ x ⦗ S ⦘ x
  69. ≡⟨ Assumption `is-reflexive S` with “Definition of reflexivity” ⟩
  70. true ∧ true
  71. ≡⟨ “Idempotency of ∧” ⟩
  72. true
  73.  
  74. Theorem “Composition of reflexive relations”:
  75. is-reflexive R ⇒ is-reflexive S ⇒ is-reflexive (R ⨾ S)
  76. Proof:
  77. Assuming `is-reflexive R` and using with “Definition of reflexivity”:
  78. Assuming `is-reflexive S` and using with “Definition of reflexivity”:
  79. Using “Definition of reflexivity”:
  80. For any `x`:
  81. x ⦗ R ⨾ S ⦘ x
  82. ≡⟨ “Relation composition” ⟩
  83. ∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x
  84. ⇐⟨ “∃-Introduction” ⟩
  85. (x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x)[b ≔ x]
  86. ≡⟨ Substitution ⟩
  87. (x ⦗ R ⦘ x ∧ x ⦗ S ⦘ x)
  88. ≡⟨ Assumption `is-reflexive R` ⟩
  89. true ∧ x ⦗ S ⦘ x
  90. ≡⟨ Assumption `is-reflexive S` ⟩
  91. true ∧ true
  92. ≡⟨ “Idempotency of ∧” ⟩
  93. true
  94.  
  95. Theorem “Converse of reflexive relations”:
  96. is-reflexive R ⇒ is-reflexive (R ˘)
  97. Proof:
  98. Assuming `is-reflexive R` and using with “Definition of reflexivity”:
  99. Using “Definition of reflexivity”:
  100. For any `x`:
  101. x ⦗ R ˘ ⦘ x
  102. ≡⟨ “Relation converse” ⟩
  103. x ⦗ R ⦘ x
  104. ≡⟨ Assumption `is-reflexive R` ⟩
  105. true
  106.  
  107. Theorem “Converse reflects reflectivity”:
  108. is-reflexive (R ˘) ⇒ is-reflexive R
  109. Proof:
  110. Assuming `is-reflexive (R ˘)` and using with “Definition of reflexivity”:
  111. Using “Definition of reflexivity”:
  112. For any `x`:
  113. x ⦗ R ⦘ x
  114. ≡⟨ “Relation converse” ⟩
  115. x ⦗ R ˘ ⦘ x
  116. ≡⟨ Assumption `is-reflexive (R ˘)` ⟩
  117. true
  118.  
  119. Theorem “Converse of transitive relations”:
  120. is-transitive R ⇒ is-transitive (R ˘)
  121. Proof:
  122. Assuming `is-transitive R` and using with “Definition of transitivity”:
  123. Using “Definition of transitivity”:
  124. For any `x`:
  125. For any `y`:
  126. For any `z`:
  127. x ⦗ R ˘ ⦘ y ⦗ R ˘ ⦘ z ⇒ x ⦗ R ˘ ⦘ z
  128. ≡⟨ “Relation converse” ⟩
  129. x ⦗ R ˘ ⦘ y ⦗ R ˘ ⦘ z ⇒ z ⦗ R ⦘ x
  130. ≡⟨ “Reflexivity of ⊆” ⟩
  131. x ⦗ R ˘ ⦘ y ∧ y ⦗ R ˘ ⦘ z ⇒ z ⦗ R ⦘ x
  132. ≡⟨ “Relation converse” ⟩
  133. (y ⦗ R ⦘ x) ∧ (z ⦗ R ⦘ y) ⇒ z ⦗ R ⦘ x
  134. ≡⟨ “Reflexivity of ⊆” ⟩
  135. (z ⦗ R ⦘ y) ∧ (y ⦗ R ⦘ x) ⇒ z ⦗ R ⦘ x
  136. ≡⟨ Assumption `is-transitive R` ⟩
  137. true
  138.  
  139. Theorem “Transitivity”:
  140. is-transitive R ≡ R ⨾ R ⊆ R
  141. Proof:
  142. R ⨾ R ⊆ R
  143. ≡⟨ “Relation inclusion” ⟩
  144. (∀ x • ∀ y • x ⦗ R ⨾ R ⦘ y ⇒ x ⦗ R ⦘ y )
  145. ≡⟨ “Relation composition” ⟩
  146. (∀ x • ∀ y • (∃ z • x ⦗ R ⦘ z ∧ z ⦗ R ⦘ y) ⇒ x ⦗ R ⦘ y )
  147. ≡⟨ “Definition of ⇒” ⟩
  148. (∀ x • ∀ y • ¬ (∃ z • x ⦗ R ⦘ z ∧ z ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y )
  149. ≡⟨ “Trading for ∃” ⟩
  150. (∀ x • ∀ y • ¬ (∃ z ❙ x ⦗ R ⦘ z • z ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y )
  151. ≡⟨ “Generalised De Morgan” ⟩
  152. (∀ x • ∀ y • (∀ z ❙ x ⦗ R ⦘ z • ¬ (z ⦗ R ⦘ y)) ∨ x ⦗ R ⦘ y )
  153. ≡⟨ “Distributivity of ∨ over ∀” ⟩
  154. (∀ x • ∀ y • (∀ z ❙ x ⦗ R ⦘ z • ¬ (z ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y))
  155. ≡⟨ “Definition of ⇒” ⟩
  156. (∀ x • ∀ y • (∀ z ❙ x ⦗ R ⦘ z • (z ⦗ R ⦘ y) ⇒ x ⦗ R ⦘ y))
  157. ≡⟨ “Trading for ∀” ⟩
  158. (∀ x • ∀ y • (∀ z • ¬ (x ⦗ R ⦘ z) ∨ ((z ⦗ R ⦘ y) ⇒ x ⦗ R ⦘ y)))
  159. ≡⟨ “Definition of ⇒” ⟩
  160. (∀ x • ∀ y • (∀ z • ¬ (x ⦗ R ⦘ z) ∨ (¬ (z ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y)))
  161. ≡⟨ “Distributivity of ∨ over ∨”, “De Morgan” ⟩
  162. (∀ x • ∀ y • (∀ z • (¬ (x ⦗ R ⦘ z ⦗ R ⦘ y) ∨ ¬ (x ⦗ R ⦘ z) ∨ x ⦗ R ⦘ y)))
  163. ≡⟨ “De Morgan” ⟩
  164. ∀ x • ∀ y • ∀ z • ¬ ((x ⦗ R ⦘ z ⦗ R ⦘ y) ∧ (x ⦗ R ⦘ z)) ∨ x ⦗ R ⦘ y
  165. ≡⟨ “Idempotency of ∧”, “Definition of ⇒” ⟩
  166. ∀ x • ∀ y • ∀ z • ((x ⦗ R ⦘ z ⦗ R ⦘ y)) ⇒ x ⦗ R ⦘ y
  167. ≡⟨ “Interchange of dummies for ∀” ⟩
  168. ∀ x • ∀ z • ∀ y • ((x ⦗ R ⦘ z ⦗ R ⦘ y)) ⇒ x ⦗ R ⦘ y
  169. ≡⟨ “Definition of transitivity” ⟩
  170. is-transitive R
  171.  
  172. Theorem (R1): ∀ b : B • ∀ c : C • (∀ a : A ❙ a ⦗ R ⦘ b • a ⦗ S ⦘ c) ≡ b ⦗ ~ (R ˘ ⨾ ~ S) ⦘ c
  173. Proof:
  174. For any `b`, `c`:
  175. b ⦗ ~ (R ˘ ⨾ ~ S) ⦘ c
  176. ≡⟨ “Relation complement” ⟩
  177. ¬ (b ⦗ (R ˘ ⨾ ~ S) ⦘ c)
  178. ≡⟨ “Relation composition” ⟩
  179. ¬ (∃ a • b ⦗ R ˘ ⦘ a ∧ a ⦗ ~ S ⦘ c)
  180. ≡⟨ “Relation converse” ⟩
  181. ¬ (∃ a • a ⦗ R ⦘ b ∧ a ⦗ ~ S ⦘ c)
  182. ≡⟨ “Relation complement” ⟩
  183. ¬ (∃ a • a ⦗ R ⦘ b ∧ ¬ (a ⦗ S ⦘ c))
  184. ≡⟨ “Generalised De Morgan”, “De Morgan”, “Double negation”, “Definition of ⇒” ⟩
  185. (∀ a • ((a ⦗ R ⦘ b) ⇒ (a ⦗ S ⦘ c)))
  186. ≡⟨ “Trading for ∀” ⟩
  187. (∀ a ❙ a ⦗ R ⦘ b • a ⦗ S ⦘ c)
  188.  
  189. Theorem (R2): R ⨾ ~ (R ˘ ⨾ ~ S) ⊆ S
  190. Proof:
  191. Using “Relation inclusion”:
  192. For any `a`, `c`:
  193. a ⦗ R ⨾ ~ (R ˘ ⨾ ~ S) ⦘ c
  194. ≡⟨ “Relation composition” ⟩
  195. (∃ b • a ⦗ R ⦘ b ∧ b ⦗ ~ (R ˘ ⨾ ~ S) ⦘ c )
  196. ≡⟨ “Relation complement” ⟩
  197. (∃ b • a ⦗ R ⦘ b ∧ ¬ (b ⦗ (R ˘ ⨾ ~ S) ⦘ c) )
  198. ≡⟨ “Relation composition” ⟩
  199. (∃ b • a ⦗ R ⦘ b ∧ ¬ (∃ a • b ⦗ (R ˘) ⦘ a ∧ a ⦗ ~ S ⦘ c ))
  200. ≡⟨ “Relation complement”, “Relation converse” ⟩
  201. (∃ b • a ⦗ R ⦘ b ∧ ¬ (∃ a • a ⦗ R ⦘ b ∧ ¬ (a ⦗ S ⦘ c) ))
  202. ≡⟨ “Trading for ∃” ⟩
  203. (∃ b ❙ a ⦗ R ⦘ b • ¬ (∃ a ❙ a ⦗ R ⦘ b • ¬ (a ⦗ S ⦘ c) ))
  204. ≡⟨ “Generalised De Morgan” ⟩
  205. ¬ (∀ b ❙ a ⦗ R ⦘ b • (∃ a ❙ a ⦗ R ⦘ b • ¬ (a ⦗ S ⦘ c) ))
  206. ≡⟨ “Trading for ∀” ⟩
  207. ¬ (∀ b • a ⦗ R ⦘ b ⇒ (∃ a ❙ a ⦗ R ⦘ b • ¬ (a ⦗ S ⦘ c)))
  208. ⇒⟨ “Instantiation” ⟩
  209. ¬ (∀ b • a ⦗ R ⦘ b ⇒ (∃ a ❙ a ⦗ R ⦘ b • ¬ (a ⦗ S ⦘ c)))
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement