大小関係、最小限と足し算との協調性 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 を再掲。
証明要求： Γ |-? ∃a.∀x.a≦x BEGIN ∀-BOX var u 0 + u = u --[●∃導入 t:←左辺のu] ∃t.0 + t = u 0 ≦ u --[●∀導入 x:←u] ∀x.(0 ≦ x) END ∀x.(0 ≦ x) --[●∃導入 a:←0] ∃a.∀x.(a ≦ x)
「足し算と協調」とタイトルが付いている次の命題。⇒は含意でシーケントではないようだ。
- a≦b, c≦d ⇒ a + c ≦ b + d
準備として、証明要求を変形する。
Γ |-? ∀a, b, c, d.(a≦b ∧ c≦d ⇒ a + c ≦ b + d)
--------------------------------------------------------
Γ, (a, b, c, d∈Nat) |-? a≦b ∧ c≦d ⇒ a + c ≦ b + d
--------------------------------------------------------
Γ, (a, b, c, d∈Nat), (a≦b ∧ c≦d) |-? a + c ≦ b + d
--------------------------------------------------------
Γ, (a, b, c, d∈Nat), a≦b, c≦d |-? a + c ≦ b + d
--------------------------------------------------------
Γ, (a, b, c, d∈Nat), ∃z.(a + z = b), ∃z.(c + z = d) |-?
∃z.(a + c + z = b + d)実際の証明は：
証明要求： Γ, (a, b, c, d∈Nat), ∃z.(a + z = b), ∃z.(c + z = d) |-?
∃z.((a + c) + z = b + d)
●∃z.(a + z = b)
BEGIN ∃-BOX
var x
a + x = b
●∃z.(c + z = d)
BEGIN ∃-BOX
var y
c + y = d
(a + x) + (c + y) = b + d
(a + c) + (x + y) = b + d
--[●∃導入 z:← x + y]
∃z.((a + c) + z = b + d)
END
∃z.((a + c) + z = b + d)
END
∃z.((a + c) + z = b + d)
