自然数の順序
x ≦ x
準備
Γ |-? ∀x∈N.(x ≦ x) ---------------------------------- Γ |-? ∀x∈N.∃z∈N.( x + z = x) ---------------------------------- Γ, x∈N |-? ∃z∈N.( x + z = x)
証明
証明要求： Γ, x∈N |-? ∃z∈N.(x + z = x) x + 0 = x ---(1) -----------------[●∃導入 z :← 0] ∃z.(x + z = x)
x≦y, y≦x ⇒ x = y
準備
Γ |-? ∀x, y, z∈N.((x ≦ y ∧ y≦x) ⇒ x = y) --------------------------------------------- Γ, x, y, z∈N |-? (x ≦ y ∧ y≦x) ⇒ x = y --------------------------------------------- Γ, x, y, z∈N, x ≦ y ∧ y≦x |-? x = y --------------------------------------------- Γ, x, y, z∈N, x ≦ y, y≦x |-? x = y ------------------------------------------------------------- Γ, x, y, z∈N, ∃z.(x + z = y), ∃z.(y + z = x) |-? x = y
証明
証明要求： Γ, x, y, z∈N, ∃z.(x + z = y), ∃z.(y + z = x) |-? x = y
●∃z.(x + z = y)
BEGIN ∃-BOX A
var a
x + a = y
●∃z(y + z = x)
BEGIN ∃-BOX B
var b
y + b = x
(x + a) + b = x
x + (a + b) = x
--[消約律から]
a + b = 0
--[ゼロ和自由性から]
a = 0 ∧ b = 0
x = y
END
x = y
END
x = y
x≦y, y≦z ⇒ x≦z
準備
Γ |-? ∀x, y, z∈N.((x≦y ∧y≦z) ⇒ x≦z) --------------------------------------------- Γ, (x, y, z∈N) |-? (x≦y ∧y≦z) ⇒ x≦z --------------------------------------------- Γ, (x, y, z∈N), (x≦y ∧ y≦z) |-? x≦z --------------------------------------------- Γ, (x, y, z∈N), x≦y, y≦z |-? x≦z --------------------------------------------- Γ, (x, y, z∈N), ∃z.(x + z = y), ∃w.(y + w = z) |-? ∃w.(x + w = z)
証明
証明要求： Γ, (x, y, z∈N), ∃z.(x + z = y), ∃w.(y + w = z) |-? ∃w.(x + w = z)
●∃z.(x + z = y)
BEGIN ∃-BOX A
var a
x + a = y
●∃w.(y + w = z)
BEGIN ∃-BOX B
var b
y + b = z
(x + a) + b = z
x + (a + b) = z
--[●∃導入 w :← (a + b)]
∃w.(x + w = z)
END
∃w.(x + w = z)
END
∃w.(x + w = z)[追記]矢田部さん資料、eigenvariable
- 基礎演習 I 論理学・授業要約（10）// ∀ と ∃ の eigenvariable 条件
- 4p
- https://researchmap.jp/mu99zdvyy-21099/?action=multidatabase_action_main_filedownload&download_flag=1&upload_id=29795&metadata_id=12105
- スライド： 基礎演習 I 論理学 第10回
- 37枚
- https://researchmap.jp/mu0vndp9g-21099/?action=multidatabase_action_main_filedownload&download_flag=1&upload_id=49595&metadata_id=12105
[/追記]
