Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Theorem “Relationship via 𝕀”: x ⦗ 𝕀 B ⦘ y ≡ x = y ∈ B
- Proof:
- x ⦗ 𝕀 B ⦘ y
- ≡⟨ “Definition of 𝕀” ⟩
- x ⦗ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⦘ y
- ≡⟨ “Infix relationship” ⟩
- ⟨ x , y ⟩ ∈ { z ❙ z ∈ B • ⟨ z , z ⟩ }
- ≡⟨ “Set membership” ⟩
- ∃ z ❙ z ∈ B • ⟨ x , y ⟩ = ⟨ z , z ⟩
- ≡⟨ “Pair equality” ⟩
- ∃ z ❙ z ∈ B • x = z ∧ y = z
- ≡⟨ “Trading for ∃” ⟩
- ∃ z ❙ y = z • x = z ∧ z ∈ B
- ≡⟨ “One-point rule for ∃”, Substitution ⟩
- x = y ∈ B
- Theorem “Intersection of 𝕀 relations”: 𝕀 B ∩ 𝕀 C = 𝕀 (B ∩ C)
- Proof:
- 𝕀 B ∩ 𝕀 C = 𝕀 (B ∩ C)
- ≡ ⟨ “Relation extensionality” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ∩ 𝕀 C ⦘ y ≡ x ⦗ 𝕀 (B ∩ C) ⦘ y
- ≡ ⟨ “Relationship via 𝕀” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ∩ 𝕀 C ⦘ y ≡ x = y ∧ y ∈ (B ∩ C)
- ≡ ⟨ “Relation intersection” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ x ⦗ 𝕀 C ⦘ y ≡ x = y ∈ (B ∩ C)
- ≡ ⟨ “Intersection” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ x ⦗ 𝕀 C ⦘ y ≡ x = y ∧ (y ∈ B ∧ y ∈ C)
- ≡ ⟨ Subproof:
- For any `x`, `y`:
- x ⦗ 𝕀 B ⦘ y ∧ x ⦗ 𝕀 C ⦘ y
- ≡ ⟨“Relationship via 𝕀”⟩
- x = y ∧ y ∈ B ∧ x = y ∧ y ∈ C
- ≡ ⟨ “Idempotency of ∧” ⟩
- x = y ∧ (y ∈ B ∧ y ∈ C)
- ⟩
- true
- Theorem “Union of 𝕀 relations”: 𝕀 B ∪ 𝕀 C = 𝕀 (B ∪ C)
- Proof:
- 𝕀 B ∪ 𝕀 C = 𝕀 (B ∪ C)
- ≡ ⟨ “Relation extensionality” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ∪ 𝕀 C ⦘ y ≡ x ⦗ 𝕀 (B ∪ C) ⦘ y
- ≡ ⟨ “Relationship via 𝕀” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ∪ 𝕀 C ⦘ y ≡ x = y ∧ y ∈ (B ∪ C)
- ≡ ⟨ “Relation union” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∨ x ⦗ 𝕀 C ⦘ y ≡ x = y ∈ (B ∪ C)
- ≡ ⟨ “Union” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∨ x ⦗ 𝕀 C ⦘ y ≡ x = y ∧ (y ∈ B ∨ y ∈ C)
- ≡ ⟨ Subproof:
- For any `x`, `y`:
- x ⦗ 𝕀 B ⦘ y ∨ x ⦗ 𝕀 C ⦘ y
- ≡ ⟨“Relationship via 𝕀”⟩
- (x = y ∧ y ∈ B) ∨ (x = y ∧ y ∈ C)
- ≡ ⟨ “Distributivity of ∧ over ∨” ⟩
- x = y ∧ (y ∈ B ∨ y ∈ C)
- ⟩
- true
- Theorem “Difference of 𝕀 relations”: 𝕀 B - 𝕀 C = 𝕀 (B - C)
- Proof:
- 𝕀 B - 𝕀 C = 𝕀 (B - C)
- ≡ ⟨ “Relation extensionality” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B - 𝕀 C ⦘ y ≡ x ⦗ 𝕀 (B - C) ⦘ y
- ≡ ⟨ “Relationship via 𝕀” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B - 𝕀 C ⦘ y ≡ x = y ∧ y ∈ (B - C)
- ≡ ⟨ “Relation difference” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ ¬ ( x ⦗ 𝕀 C ⦘ y ) ≡ x = y ∈ (B - C)
- ≡ ⟨ “Set difference” ⟩
- ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ ¬ ( x ⦗ 𝕀 C ⦘ y ) ≡ x = y ∧ (y ∈ B ∧ ¬ (y ∈ C))
- ≡ ⟨ Subproof:
- For any `x`, `y`:
- x ⦗ 𝕀 B ⦘ y ∧ ¬ ( x ⦗ 𝕀 C ⦘ y )
- ≡ ⟨“Relationship via 𝕀”⟩
- (x = y ∧ y ∈ B) ∧ ¬ (x = y ∧ y ∈ C)
- ≡ ⟨“De Morgan”, “Distributivity of ∧ over ∨”, “Contradiction”, “Identity of ∨” ⟩
- x = y ∧ (y ∈ B ∧ ¬ (y ∈ C))
- ⟩
- true
- Theorem “Set complement as difference”: ~ B = 𝐔 - B
- Proof:
- ~ B = 𝐔 - B
- ≡ ⟨“Set extensionality”⟩
- ∀ e • e ∈ ~ B ≡ e ∈ 𝐔 - B
- ≡ ⟨“Set difference”, “Universal set”, “Identity of ∧”⟩
- ∀ e • e ∈ ~ B ≡ ¬ (e ∈ B)
- ≡ ⟨“Complement”⟩
- ∀ e • true — This is “True ∀ body”
- Theorem “Intersection of 𝕀 and ×”: 𝕀 B ∩ (C × D) = 𝕀 (B ∩ C ∩ D)
- Proof:
- Using “Relation extensionality”:
- For any `x`, `y`:
- x ⦗ 𝕀 B ∩ (C × D) ⦘ y
- ≡ ⟨ “Relation intersection” ⟩
- x ⦗ 𝕀 B ⦘ y ∧ x ⦗ (C × D) ⦘ y
- ≡ ⟨ “Relationship via 𝕀”, “Infix relationship” ⟩
- x = y ∧ y ∈ B ∧ ⟨ x , y ⟩ ∈ (C × D)
- ≡ ⟨ “Membership in ×” ⟩
- x = y ∧ y ∈ B ∧ x ∈ C ∧ y ∈ D
- ≡ ⟨ Substitution ⟩
- x = y ∧ (y ∈ B ∧ z ∈ C ∧ y ∈ D)[z ≔ x]
- ≡ ⟨ “Replacement”, Substitution ⟩
- x = y ∧ (y ∈ B ∧ y ∈ C ∧ y ∈ D)
- ≡ ⟨ “Intersection” ⟩
- x = y ∧ (y ∈ B ∩ C ∩ D)
- ≡ ⟨ “Relationship via 𝕀” ⟩
- x ⦗ 𝕀 (B ∩ C ∩ D) ⦘ y
- Theorem “Difference of 𝕀 and ×”: 𝕀 B - (C × D) = 𝕀 (B - (C ∩ D))
- Proof:
- Using “Relation extensionality”:
- For any `x`, `y`:
- x ⦗ 𝕀 B - (C × D) ⦘ y
- ≡ ⟨“Relation difference”⟩
- (( x ⦗ 𝕀 B ⦘ y ) ∧ ¬ ( x ⦗ (C × D) ⦘ y ))
- ≡ ⟨“Infix relationship”, “Relationship via 𝕀”, “Membership in ×”⟩
- x = y ∧ y ∈ B ∧ ¬ (x ∈ C ∧ y ∈ D)
- ≡ ⟨Substitution⟩
- x = y ∧ (y ∈ B ∧ ¬ (z ∈ C ∧ y ∈ D))[z ≔ x]
- ≡ ⟨“Replacement”, Substitution⟩
- x = y ∧ y ∈ B ∧ ¬ (y ∈ C ∧ y ∈ D)
- ≡ ⟨“Intersection”⟩
- x = y ∧ y ∈ B ∧ ¬ (y ∈ C ∩ D)
- ≡ ⟨“Relationship via 𝕀”, “Set difference”⟩
- x ⦗ 𝕀 (B - (C ∩ D)) ⦘ y
- Theorem “Isotonicity of 𝕀”: B ⊆ C ≡ 𝕀 B ⊆ 𝕀 C
- Proof:
- 𝕀 B ⊆ 𝕀 C
- ≡ ⟨ “Set inclusion” ⟩
- ∀ e ❙ e ∈ 𝕀 B • e ∈ 𝕀 C
- ≡ ⟨ “Definition of 𝕀”, “Trading for ∀” ⟩
- ∀ e • e ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⇒ e ∈ { x ❙ x ∈ C • ⟨ x , x ⟩ }
- ≡ ⟨ Subproof for `e ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⇒ e ∈ { x ❙ x ∈ C • ⟨ x , x ⟩ } ≡ ∀ e • e ∈ B ⇒ e ∈ C`:
- e ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⇒ e ∈ { x ❙ x ∈ C • ⟨ x , x ⟩ }
- ≡ ⟨ ? ⟩
- e ∈ B ⇒ e ∈ C
- ⟩
- ∀ e • e ∈ B ⇒ e ∈ C
- ≡ ⟨“Trading for ∀”, “Set inclusion”⟩
- B ⊆ C
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement