逆証明

集合のド・モルガンの法則の証明（順証明、フォワード証明）http://d.hatena.ne.jp/m-hiyama-memo/20170810/1502363526 の最後のほうは、

// SerND
   (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B)
 contract $.1, $.2 by (集合の差)
   (x∈X＼A) ∨ (x∈X＼B)
  contract by (集合の合併)
   x∈(X＼A)∪(X＼B)
  use assumption (ass)
   x∈X＼(A∩B) ⇒ x∈(X＼A)∪(X＼B)
  contract by 集合の包含
   X＼(A∩B) ⊆ (X＼A)∪(X＼B)
 end proof

逆証明"bw-1"を書いてみる。

 X＼(A∩B) ⊆ (X＼A)∪(X＼B)
expand by 集合の包含
 x∈X＼(A∩B) ⇒ x∈(X＼A)∪(X＼B)
register assumption
 x∈(X＼A)∪(X＼B) |[ x∈X＼(A∩B) ]
expand by (集合の合併)
 (x∈X＼A) ∨ (x∈X＼B)
expand by (集合の差)
 (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B)

この逆証明で、次の法則（定理に対するシーケント）"Th-1"が得られる。

for x:object, X, A, B:Set
given
  x∈X＼(A∩B) ⇒ (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B)
holds
   X＼(A∩B) ⊆ (X＼A)∪(X＼B)

次に順証明"fw-1"：

assume
   x∈X＼(A∩B) ---(ass)
expand by (集合の差)
   x∈X ∧ ¬(x∈A∩B)
expand $.2.1 by (集合の共通部分)
   x∈X ∧ ¬(x∈A ∧ x∈B)
rewrite $.2 by (ド・モルガンの法則)
   x∈X ∧ (¬(x∈A) ∨ ¬(x∈B))
rewrite by (論理の分配法則)
   (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B)
use assumption (ass)
   x∈X＼(A∩B) ⇒ (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B)

これから次の法則"Th-2"。

for x:object, X, A, B:Set
holds
 x∈X＼(A∩B) ⇒ (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B)

すると、（以下も順証明"fw-2"）

順証明"fw-1"からの"Th-2"
  x∈X＼(A∩B) ⇒ (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B)
逆証明"bw-1"からの"Th-1"
  (x∈X＼(A∩B) ⇒ (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B)) ⇒ X＼(A∩B) ⊆ (X＼A)∪(X＼B)
apply（モダスポネンス）により
  X＼(A∩B) ⊆ (X＼A)∪(X＼B)

これを法則（定理のシーケント）"Th-3"にすると：

for x:object, X, A, B:Set
holds
  X＼(A∩B) ⊆ (X＼A)∪(X＼B)

まとめると：

• bw-1によりTh-1
• fw-1によりTh-2
• fw-2によりTh-3