引き算の定義

参考：

• 引き算と無限個の足し算は両立しない - 檜山正幸のキマイラ飼育記
• モノイドや半環は、群や環とはかけ離れている - 檜山正幸のキマイラ飼育記

定義

集合Lの定義

• L := {(x, y)∈N² | x≦y }
• (x, y)∈L ⇔ ∃z.(x + z = y)

関数subtの定義

• function subt := λ(x, y)∈L.εz.(x + z = y)

関数subtの正当性（well-defined）

• 値の存在：(x, y)∈L ⇒ ∃z.(x + z = y)
• 値の一意性：(x, y)∈L ⇒ (x + z = y)∧(x + z' = y) ⇒ z = z'

値の存在

準備

 Γ |-? ∀x, y, z∈N.(x, y)∈<b>L</b> ⇒ ∃z.(x + z = y)
 --------------------------------------------------------
 Γ, x, y, z∈N |-? (x, y)∈<b>L</b> ⇒ ∃z.(x + z = y)
 --------------------------------------------------------
 Γ, x, y, z∈N, (x, y)∈<b>L</b> |-? ∃z.(x + z = y)
 --------------------------------------------------------
 Γ, x, y, z∈N, ∃z.(x + z = y) |-? ∃z.(x + z = y)

証明不要。

値の一意性

準備

 Γ |-?
   ∀x, y, z∈N.(x, y)∈<b>L</b> ⇒ (x + z = y)∧(x + z' = y) ⇒ z = z'
 ---------------------------------------------------------------
 Γ, (x, y, z∈N) |-?
   (x, y)∈<b>L</b> ⇒ (x + z = y)∧(x + z' = y) ⇒ z = z'
 ---------------------------------------------------------------
 Γ, (x, y, z∈N) |-?
   (∃z.x + z = y) ⇒ ((x + z = y)∧(x + z' = y) ⇒ z = z')
 ---------------------------------------------------------------
 Γ, (x, y, z∈N), (∃z.x + z = y) |-?
   (x + z = y)∧(x + z' = y) ⇒ z = z'

証明

証明要求： Γ, (x, y, z∈N), (∃z.x + z = y) |-?
   (x + z = y)∧(x + z' = y) ⇒ z = z'

 x + z = y
 x + z' = y
 x + z = x + z'
  --[消約律から]
 z = z'