このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

A = B-(B-A) ⇔ A⊆B

人と人とのコミュニケーションを目的にするので、機械可読ではない。特に、新しい変数(fresh variable)が登場したら、適当な変域の自由変数(または全称束縛変数)と解釈する。

前提

次は前提(既に知っているもの)とする。':⇔' は '⇔' と同じだが、定義していることを示すために':'を付けている。

論理の法則

使いそうなものだけ。

  1. (⇔定義) (P⇔Q) :⇔ (P⇒Q)∧(Q⇒P) // '⇔'の定義に'⇔'を使っているというツッコミはあるだろうが、、、
  2. (ド・モルガン) ¬(P∧Q) ⇔ ¬P∨¬Q,  ¬(P∨Q) ⇔ ¬P∧¬Q
  3. (二重否定) ¬¬P ⇔ P
  4. (分配) P∧(Q∨R) ⇔ (P∧Q)∨(P∧Q),  P∨(Q∧R) ⇔ (P∨Q)∧(P∨Q)
  5. (矛盾) P∧¬P ⇔ false
  6. (∧単位) true∧P ⇔ P
  7. (∧交換) P∧Q ⇔ Q∧P
  8. (∨単位) false∨P ⇔ P
  9. (∨交換) P∨Q ⇔ P∨Q

「'⇔'の定義に'⇔'を使っている」は、定義用のメタ記号(例えば':≡')を導入すれば回避できる。ただし、演繹定理があるので、ここらへんはあまり気にしなくてよい。

集合に対する定義と定理

使いそうなものだけ。

  1. (集合⊆) A⊆B :⇔ (x∈A ⇒ x∈B)
  2. (集合=) A = B :⇔ (A⊆B ∧ B⊆A)
  3. (集合∩) x∈A∩B :⇔ (x∈A ∧ x∈B)
  4. (集合∪) x∈A∪B :⇔ (x∈A ∨ x∈B)
  5. (集合-) x∈A-B :⇔ (x∈A ∧ ¬(x∈B))
  6. (∩と⊆) A∩B⊆A,  A∩B⊆B
  7. (∪と⊆) A⊆A∪B,  B⊆A∪B
  8. (∩は単調) A⊆B ⇒ A∩C⊆B∩C
  9. (∪は単調) A⊆B ⇒ A∪C⊆B∪C
  10. (∩はベキ等) A∩A = A
  11. (∪はベキ等) A∪A = A
  12. (∩は可換) A∩B = B∩A
  13. (∪は可換) 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

これより

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