A = B-(B-A) ⇔ A⊆B
人と人とのコミュニケーションを目的にするので、機械可読ではない。特に、新しい変数(fresh variable)が登場したら、適当な変域の自由変数(または全称束縛変数)と解釈する。
前提
次は前提(既に知っているもの)とする。':⇔' は '⇔' と同じだが、定義していることを示すために':'を付けている。
論理の法則
使いそうなものだけ。
- (⇔定義) (P⇔Q) :⇔ (P⇒Q)∧(Q⇒P) // '⇔'の定義に'⇔'を使っているというツッコミはあるだろうが、、、
- (ド・モルガン) ¬(P∧Q) ⇔ ¬P∨¬Q, ¬(P∨Q) ⇔ ¬P∧¬Q
- (二重否定) ¬¬P ⇔ P
- (分配) P∧(Q∨R) ⇔ (P∧Q)∨(P∧Q), P∨(Q∧R) ⇔ (P∨Q)∧(P∨Q)
- (矛盾) P∧¬P ⇔ false
- (∧単位) true∧P ⇔ P
- (∧交換) P∧Q ⇔ Q∧P
- (∨単位) false∨P ⇔ P
- (∨交換) P∨Q ⇔ P∨Q
「'⇔'の定義に'⇔'を使っている」は、定義用のメタ記号(例えば':≡')を導入すれば回避できる。ただし、演繹定理があるので、ここらへんはあまり気にしなくてよい。
集合に対する定義と定理
使いそうなものだけ。
- (集合⊆) A⊆B :⇔ (x∈A ⇒ x∈B)
- (集合=) A = B :⇔ (A⊆B ∧ B⊆A)
- (集合∩) x∈A∩B :⇔ (x∈A ∧ x∈B)
- (集合∪) x∈A∪B :⇔ (x∈A ∨ x∈B)
- (集合-) x∈A-B :⇔ (x∈A ∧ ¬(x∈B))
- (∩と⊆) A∩B⊆A, A∩B⊆B
- (∪と⊆) A⊆A∪B, B⊆A∪B
- (∩は単調) A⊆B ⇒ A∩C⊆B∩C
- (∪は単調) A⊆B ⇒ A∪C⊆B∪C
- (∩はベキ等) A∩A = A
- (∪はベキ等) A∪A = A
- (∩は可換) A∩B = B∩A
- (∪は可換) A∪B = B∪A
補題
B-(B-A) = A∩B
target // 目標 B-(B-A) = A∩B proof // ここから証明開始 equivalence // ここから同値性の証明 // 各行が同値な命題、行頭の'⇔'は省略、'by'で根拠を示す x∈B-(B-A) x∈B ∧ ¬(x∈B-A) by (集合-) x∈B ∧ ¬(x∈B ∧ ¬(x∈A)) by (集合-) x∈B ∧ (¬(x∈B) ∨ (x∈A)) by (ド・モルガン), (二重否定) (x∈B ∧ ¬(x∈B)) ∨ (x∈B ∧ x∈A) by (分配) false ∨ (x∈B ∧ x∈A) by (矛盾) x∈B ∧ x∈A by (∨単位) x∈B∩A by (集合∩) end equivalence // 同値性の証明 終わり thus x∈B-(B-A) ⇔ x∈B∩A // 'thus'は「念のために言うならば」 B-(B-A) = B∩A by (集合=) end proof // 証明終わり thus B-(B-A) = B∩A
これより
- (補題1) B-(B-A) = A∩B
A = A∩B ⇔ A⊆B
target // 最終的な目標 A = A∩B ⇔ A⊆B proof target // 入れ子は補助的な目標 A = A∩B ⇒ A⊆B proof assume A = A∩B ---(1) // これは仮定 by the way // 一旦話題を変えるけど A∩B ⊆ B by (∩と⊆) // いつだって成立している命題 A ⊆ B by (1) use assumption (1) // 仮定を使う、自然演繹の含意導入 A = A∩B ⇒ A ⊆ B end proof thus A = A∩B ⇒ A⊆B ---(2) target A⊆B ⇒ A = A∩B proof assume A⊆B ---(3) A∩A ⊆ B∩A by (∩は単調) A ⊆ B∩A by (∩はベキ等) A ⊆ A∩B by (∩は可換) use assumptin (3) A⊆B ⇒ A ⊆ A∩B end proof thus A⊆B ⇒ A ⊆ A∩B ---(4) A = A∩B ⇔ A⊆B by (2), (4), (⇔定義) end proof thus A = A∩B ⇔ A⊆B
これより
- (補題2) A = A∩B ⇔ A⊆B
定理
target A = B-(B-A) ⇔ A⊆B proof assume A = B-(B-A) ---(1) A = A∩B by (補題1: B-(B-A) = A∩B) A⊆B by (補題2: A = A∩B ⇔ A⊆B) use assumption (1) A = B-(B-A) ⇒ A⊆B ---(2) assume A⊆B ---(3) by the way A∩B ⊆ A by (∩と⊆) ---(4) B-(B-A) ⊆ A by (補題1: B-(B-A) = A∩B) use assumption (3) A⊆B ⇒ B-(B-A) ⊆ A ---(5) A = B-(B-A) ⇔ A⊆B by (2), (5), (⇔定義) end proof thus A = B-(B-A) ⇔ A⊆B