SHARE
TWEET

Untitled

a guest Nov 12th, 2019 69 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Theorem “Relationship via 𝕀”: x ⦗ 𝕀 B ⦘ y  ≡  x = y ∈ B
  2. Proof:
  3.     x ⦗ 𝕀 B ⦘ y
  4.   ≡⟨ “Definition of 𝕀” ⟩
  5.     x ⦗ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⦘ y
  6.   ≡⟨ “Infix relationship” ⟩
  7.     ⟨ x , y ⟩ ∈ { z ❙ z ∈ B • ⟨ z , z ⟩ }
  8.   ≡⟨ “Set membership” ⟩
  9.     ∃ z ❙ z ∈ B • ⟨ x , y ⟩ = ⟨ z , z ⟩
  10.   ≡⟨ “Pair equality” ⟩
  11.     ∃ z ❙ z ∈ B • x = z ∧ y = z
  12.   ≡⟨ “Trading for ∃” ⟩
  13.     ∃ z ❙ y = z • x = z ∧ z ∈ B
  14.   ≡⟨ “One-point rule for ∃”, Substitution ⟩
  15.     x = y ∈ B
  16.  
  17. Theorem “Intersection of 𝕀 relations”: 𝕀 B ∩ 𝕀 C = 𝕀 (B ∩ C)
  18. Proof:
  19.     𝕀 B ∩ 𝕀 C = 𝕀 (B ∩ C)
  20.   ≡ ⟨ “Relation extensionality” ⟩
  21.     ∀ x • ∀ y • x ⦗ 𝕀 B ∩ 𝕀 C ⦘ y ≡ x ⦗ 𝕀 (B ∩ C) ⦘ y
  22.   ≡ ⟨ “Relationship via 𝕀” ⟩
  23.     ∀ x • ∀ y • x ⦗ 𝕀 B ∩ 𝕀 C ⦘ y ≡ x = y ∧ y ∈ (B ∩ C)
  24.   ≡ ⟨ “Relation intersection” ⟩
  25.     ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ x ⦗ 𝕀 C ⦘ y ≡ x = y ∈ (B ∩ C)
  26.   ≡ ⟨ “Intersection” ⟩
  27.     ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ x ⦗ 𝕀 C ⦘ y ≡ x = y ∧ (y ∈ B ∧ y ∈ C)
  28.   ≡ ⟨ Subproof:
  29.         For any `x`, `y`:
  30.             x ⦗ 𝕀 B ⦘ y ∧ x ⦗ 𝕀 C ⦘ y
  31.           ≡ ⟨“Relationship via 𝕀”⟩
  32.             x = y ∧ y ∈ B ∧ x = y ∧ y ∈ C
  33.           ≡ ⟨ “Idempotency of ∧” ⟩
  34.              x = y ∧ (y ∈ B ∧ y ∈ C)
  35.     ⟩
  36.     true
  37.            
  38.  
  39. Theorem “Union of 𝕀 relations”: 𝕀 B ∪ 𝕀 C = 𝕀 (B ∪ C)
  40. Proof:
  41.     𝕀 B ∪ 𝕀 C = 𝕀 (B ∪ C)
  42.   ≡ ⟨ “Relation extensionality” ⟩
  43.     ∀ x • ∀ y • x ⦗ 𝕀 B ∪ 𝕀 C ⦘ y ≡ x ⦗ 𝕀 (B ∪ C) ⦘ y
  44.   ≡ ⟨ “Relationship via 𝕀” ⟩
  45.     ∀ x • ∀ y • x ⦗ 𝕀 B ∪ 𝕀 C ⦘ y ≡ x = y ∧ y ∈ (B ∪ C)
  46.   ≡ ⟨ “Relation union” ⟩
  47.     ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∨ x ⦗ 𝕀 C ⦘ y ≡ x = y ∈ (B ∪ C)
  48.   ≡ ⟨ “Union” ⟩
  49.     ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∨ x ⦗ 𝕀 C ⦘ y ≡ x = y ∧ (y ∈ B ∨ y ∈ C)
  50.   ≡ ⟨ Subproof:
  51.         For any `x`, `y`:
  52.             x ⦗ 𝕀 B ⦘ y ∨ x ⦗ 𝕀 C ⦘ y
  53.           ≡ ⟨“Relationship via 𝕀”⟩
  54.             (x = y ∧ y ∈ B) ∨ (x = y ∧ y ∈ C)
  55.           ≡ ⟨ “Distributivity of ∧ over ∨” ⟩
  56.             x = y ∧ (y ∈ B ∨ y ∈ C)
  57.     ⟩
  58.     true
  59.  
  60. Theorem “Difference of 𝕀 relations”: 𝕀 B - 𝕀 C = 𝕀 (B - C)
  61. Proof:
  62.     𝕀 B - 𝕀 C = 𝕀 (B - C)
  63.   ≡ ⟨ “Relation extensionality” ⟩
  64.     ∀ x • ∀ y • x ⦗ 𝕀 B - 𝕀 C ⦘ y ≡ x ⦗ 𝕀 (B - C) ⦘ y
  65.   ≡ ⟨ “Relationship via 𝕀” ⟩
  66.     ∀ x • ∀ y • x ⦗ 𝕀 B - 𝕀 C ⦘ y ≡ x = y ∧ y ∈ (B - C)
  67.   ≡ ⟨ “Relation difference” ⟩
  68.     ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ ¬ ( x ⦗ 𝕀 C ⦘ y ) ≡ x = y ∈ (B - C)
  69.   ≡ ⟨ “Set difference” ⟩
  70.     ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ ¬ ( x ⦗ 𝕀 C ⦘ y ) ≡ x = y ∧ (y ∈ B ∧ ¬ (y ∈ C))
  71.   ≡ ⟨ Subproof:
  72.         For any `x`, `y`:
  73.             x ⦗ 𝕀 B ⦘ y ∧ ¬ ( x ⦗ 𝕀 C ⦘ y )
  74.           ≡ ⟨“Relationship via 𝕀”⟩
  75.             (x = y ∧ y ∈ B) ∧ ¬ (x = y ∧ y ∈ C)
  76.           ≡ ⟨“De Morgan”, “Distributivity of ∧ over ∨”, “Contradiction”, “Identity of ∨” ⟩
  77.             x = y ∧ (y ∈ B ∧ ¬ (y ∈ C))
  78.     ⟩
  79.     true
  80.  
  81. Theorem “Set complement as difference”: ~ B = 𝐔 - B
  82. Proof:
  83.     ~ B = 𝐔 - B
  84.   ≡ ⟨“Set extensionality”⟩
  85.     ∀ e • e ∈ ~ B ≡ e ∈ 𝐔 - B
  86.   ≡ ⟨“Set difference”, “Universal set”, “Identity of ∧”⟩
  87.     ∀ e • e ∈ ~ B ≡ ¬ (e ∈ B)
  88.   ≡ ⟨“Complement”⟩
  89.     ∀ e • true — This is “True ∀ body”
  90.  
  91.  
  92. Theorem “Intersection of 𝕀 and ×”: 𝕀 B ∩ (C × D) = 𝕀 (B ∩ C ∩ D)
  93. Proof:
  94.   Using “Relation extensionality”:
  95.     For any `x`, `y`:
  96.          x ⦗ 𝕀 B ∩ (C × D) ⦘ y
  97.       ≡ ⟨ “Relation intersection” ⟩
  98.          x ⦗ 𝕀 B ⦘ y ∧ x ⦗ (C × D) ⦘ y  
  99.       ≡ ⟨ “Relationship via 𝕀”, “Infix relationship” ⟩
  100.          x = y ∧ y ∈ B ∧ ⟨ x , y ⟩ ∈ (C × D)  
  101.       ≡ ⟨ “Membership in ×” ⟩
  102.          x = y ∧ y ∈ B ∧ x ∈ C ∧ y ∈ D
  103.       ≡ ⟨ Substitution ⟩
  104.          x = y ∧ (y ∈ B ∧ z ∈ C ∧ y ∈ D)[z ≔ x]
  105.       ≡ ⟨ “Replacement”, Substitution ⟩
  106.          x = y ∧ (y ∈ B ∧ y ∈ C ∧ y ∈ D)
  107.       ≡ ⟨ “Intersection” ⟩
  108.          x = y ∧ (y ∈ B ∩ C ∩ D)
  109.       ≡ ⟨ “Relationship via 𝕀” ⟩
  110.          x ⦗ 𝕀 (B ∩ C ∩ D) ⦘ y
  111.  
  112.  
  113. Theorem “Difference of 𝕀 and ×”: 𝕀 B - (C × D) = 𝕀 (B - (C ∩ D))
  114. Proof:
  115.   Using “Relation extensionality”:
  116.     For any `x`, `y`:
  117.         x ⦗ 𝕀 B - (C × D) ⦘ y
  118.       ≡ ⟨“Relation difference”⟩
  119.         (( x ⦗ 𝕀 B ⦘ y ) ∧ ¬ ( x ⦗ (C × D) ⦘ y ))
  120.       ≡ ⟨“Infix relationship”, “Relationship via 𝕀”, “Membership in ×”⟩
  121.          x = y ∧ y ∈ B ∧ ¬ (x ∈ C ∧ y ∈ D)
  122.       ≡ ⟨Substitution⟩
  123.          x = y ∧ (y ∈ B ∧ ¬ (z ∈ C ∧ y ∈ D))[z ≔ x]
  124.       ≡ ⟨“Replacement”, Substitution⟩
  125.          x = y ∧ y ∈ B ∧ ¬ (y ∈ C ∧ y ∈ D)
  126.       ≡ ⟨“Intersection”⟩
  127.          x = y ∧ y ∈ B ∧ ¬ (y ∈ C ∩ D)
  128.       ≡ ⟨“Relationship via 𝕀”, “Set difference”⟩
  129.          x ⦗ 𝕀 (B - (C ∩ D)) ⦘ y
  130.  
  131.  
  132. Theorem “Isotonicity of 𝕀”:  B ⊆ C  ≡  𝕀 B ⊆ 𝕀 C
  133. Proof:
  134.     𝕀 B ⊆ 𝕀 C
  135.   ≡ ⟨ “Set inclusion” ⟩
  136.     ∀ e ❙ e ∈ 𝕀 B • e ∈ 𝕀 C
  137.   ≡ ⟨ “Definition of 𝕀”, “Trading for ∀” ⟩
  138.     ∀ e • e ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⇒ e ∈ { x ❙ x ∈ C • ⟨ x , x ⟩ }
  139.   ≡ ⟨ Subproof for `e ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⇒ e ∈ { x ❙ x ∈ C • ⟨ x , x ⟩ } ≡ ∀ e • e ∈ B ⇒ e ∈ C`:
  140.         e ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⇒ e ∈ { x ❙ x ∈ C • ⟨ x , x ⟩ }
  141.       ≡ ⟨ ? ⟩
  142.         e ∈ B ⇒ e ∈ C
  143.     ⟩
  144.     ∀ e • e ∈ B ⇒ e ∈ C
  145.   ≡ ⟨“Trading for ∀”, “Set inclusion”⟩
  146.     B ⊆ C
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top