比較的最近、述語論理の全称記号・存在記号について書きました。
特定分野の予備知識を仮定しないことにすると、例題は自然数や整数の話になりがちですが、集合と写像をネタに例題を探してみました。
f:X→Y は写像として、S⊆X, T⊆Y とします。
- s∈S ⇒ f(s)∈T
が成立しているとします。これは、
- f*(S)⊆T
と書けますね。ここで、f*(S)は、fによるSの像〈image〉を表します。
- f*(S) := {y∈Y | ∃x∈X.(x∈S ∧ f(x) = y)}
f*(S) を単に f(S) と書くことがありますが、好ましくないです。なぜなら、f:X→Y, f*:Pow(X)→Pow(Y) であり、fとf*は異なる写像だからです。
さて、f*(S)⊆T は、
- ∀y∈Y.(y∈f*(S) ⇒ y∈T)
であり、f*(S) をその定義により書き換えると：
- ∀y∈Y.(y∈{y∈Y | ∃x∈X.(x∈S ∧ f(x) = y)} ⇒ y∈T)
集合の内包的記法が冗長なので（ウザいだけなので）落として、
- ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T)
これは f*(S)⊆T の書き換えに過ぎないので、最初に挙げた命題 s∈S ⇒ f(s)∈T に全称記号を付けた命題と同値のはずです。
- ∀s∈X.(s∈S ⇒ f(s)∈T)
同値であることを述べると：
- ∀s∈X.(s∈S ⇒ f(s)∈T) ⇔ ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T)
この命題は、今述べた背景から考えれば明らかに成立します。が、背景は忘れて、単なる論理的命題の証明だと思って淡々と証明してみます。
同値性を主張する命題を2つの含意命題に分けます。
- ∀s∈X.(s∈S ⇒ f(s)∈T) ⇒ ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T)
- ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T) ⇒ ∀s∈X.(s∈S ⇒ f(s)∈T)
それぞれの証明要求を書きます。
- Γ |-? ∀s∈X.(s∈S ⇒ f(s)∈T) ⇒ ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T)
- Γ |-? ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T) ⇒ ∀s∈X.(s∈S ⇒ f(s)∈T)
Γ（文脈、予備知識）のなかには、「X, Yは集合である」とか「f:X→Y, S⊆X, T⊆Y」なんかが入っています。
それぞれの証明要求を変形（お膳立て）します。
Γ |-? ∀s∈X.(s∈S ⇒ f(s)∈T) ⇒ ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T) ---------------------------------------------------------------------- Γ, ∀s∈X.(s∈S ⇒ f(s)∈T) |-? ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T) ---------------------------------------------------------------------- Γ, ∀s∈X.(s∈S ⇒ f(s)∈T), y∈Y |-? ∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T ---------------------------------------------------------------------- Γ, ∀s∈X.(s∈S ⇒ f(s)∈T), y∈Y, ∃x∈X.(x∈S ∧ f(x) = y) |-? y∈T
Γ |-?
∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T) ⇒ ∀s∈X.(s∈S ⇒ f(s)∈T)
----------------------------------------------------------------------
Γ, ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T) |-?
∀s∈X.(s∈S ⇒ f(s)∈T)
----------------------------------------------------------------------
Γ, ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T), s∈X |-?
s∈S ⇒ f(s)∈T
----------------------------------------------------------------------
Γ, ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T), s∈X, s∈S |-?
f(s)∈T
証明をします。∀と∃の推論規則を使った場所には、目立つように'●'を付けておきます。
証明要求： Γ, ∀s∈X.(s∈S ⇒ f(s)∈T), y∈Y, ∃x∈X.(x∈S ∧ f(x) = y)
|-? y∈T
// 前提より
∃x∈X.(x∈S ∧ f(x) = y)
BEGIN ●∃除去
a∈X
a∈S ∧ f(a) = y ---(1)
// 前提より
∀s∈X.(s∈S ⇒ f(s)∈T),
--[●∀除去 s:=a]
a∈S ⇒ f(a)∈T ---(2)
// (1)から
a∈S ---(3)
// (2), (3)から
f(a)∈T ---(4)
// (1)から
f(a) = y ---(5)
// (4), (5)から
y ∈T
END
y∈T
証明要求： Γ, ∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T), s∈X, s∈S
|-? f(s)∈T
// 前提より
∀y∈Y.(∃x∈X.(x∈S ∧ f(x) = y) ⇒ y∈T)
--[●∀除去 y:=f(s)]
∃x∈X.(x∈S ∧ f(x) = f(s)) ⇒ f(s)∈T ---(1)
// 前提より
s∈S
// 等号の反射律から
f(s) = f(s)
// 上の2つの命題から
s∈S ∧ f(s) = f(s)
--[●∃導入 一番左のs:←x, 二番目のs:←x]
∃x∈X.(x∈S ∧ f(x) = f(s)) ---(2)
// (1), (2)から
f(s)∈T
