整数の問題の一部解答

• Even(n) :⇔ ∃p.(n = 2p)

のもとで、

• ∀n.(n%2 = 1 ⇔ ¬∃p.(n = 2p))

を示す。

  Γ |-? ∀n.(n%2 = 1 ⇔ ¬∃p.(n = 2p))
 --------------------------------------------------
  Γ, n∈<b>Z</b> |-? n%2 = 1 ⇔ ¬∃p.(n = 2p)
 --------------------------------------------------
  Γ, n∈<b>Z</b> |-? n%2 = 1 ⇒ ¬∃p.(n = 2p)
  Γ, n∈<b>Z</b> |-? ¬∃p.(n = 2p) ⇒ n%2 = 1
 --------------------------------------------------
  Γ, n∈<b>Z</b>, n%2 = 1 |-?  ¬∃p.(n = 2p)
  Γ, n∈<b>Z</b>, ¬∃p.(n = 2p) |-? n%2 = 1

  Γ, n∈<b>Z</b>, n%2 = 1 |-?  ¬∃p.(n = 2p)
 ---------------------------------------------
 ↓             [n%2 = 1 ⇔ ∃q.(n = 2q + 1)]
 ---------------------------------------------
  Γ, n∈<b>Z</b>, ∃q.(n = 2q + 1) |-?  ¬∃p.(n = 2p)
 ---------------------------------------------
  Γ, n∈<b>Z</b>, ∃q.(n = 2q + 1), ∃p.(n = 2p) |-? ⊥

次は公理

• ∀n, m.∃!q, r.(n = qm + r ∧ 0≦ r ＜m)

前提の ∃q.(n = 2q + 1), ∃p.(n = 2p) から

• q = p, 1 = 0

1 = 0 と 1 ≠ 0 となり矛盾。

以上で、

• Γ, n∈Z, ∃q.(n = 2q + 1), ∃p.(n = 2p) |- ⊥

逆向きの証明に移る。

  Γ, n∈<b>Z</b>, ¬∃p.(n = 2p) |-? n%2 = 1
 ---------------------------------------------
 ↓             [n%2 = 1 ⇔ ∃q.(n = 2q + 1)]
 ---------------------------------------------
  Γ, n∈<b>Z</b>, ¬∃p.(n = 2p) |-? ∃q.(n = 2q + 1)

公理から、

• ∃!q, r.(n = 2q + r ∧ 0≦ r ＜2)

これより、

• ∃!q,[(n = 2q + 0) ∨ (n = 2q + 1)]
• ∃!q,(n = 2q + 0) ∨ ∃!q.(n = 2q + 1)
• 仮定から、∃!q,(n = 2q + 0) が落ちて
• ∃q.(n = 2q + 1)

ターゲットが示せた。