証明図シリアル化構文 キーワードの現状
| キーワード | 意味 | 備考 |
|---|---|---|
| target | 目標は…である。 | |
| proof end | （これから）証明しよう。 | |
| set | …と置く。 | |
| by the way | ところで | リーフの開始 |
| remark | …であることを注意しておく。 | |
| concat | …との連言を作る。 | ∧導入 |
| select | …を抜き出すと、 | ∧除去 |
| add | …との選言を作る。 | ∨導入 |
| cases end | （これから）場合分けをしよう。 | ∨除去ブロック |
| contradict end | （これから）背理法で証明しよう。 | ¬導入ブロック |
| conflict | 矛盾が生じる。 | ¬除去、⊥導入 |
| produce | 何でも言えるので、 | ⊥除去 |
| assume | …を仮定する。 | ⇒導入疑似ブロック |
| use assumption | 仮定を使って、 | ⇒導入 |
| apply | …を適用すれば、 | ⇒除去 |
| for end | …について考えよう。 | ∀導入ブロック |
| fix（forと同義） | …を任意に固定しよう。 | ∀導入ブロック |
| introduce universal | 全称化すれば、 | ∀導入 |
| instantiate | …で具体化すれば、 | ∀除去 |
| introduce existential | 特称化すれば、 | ∃導入 |
| choice end | 適当な…を選ぶ。 | ∃除去ブロック |
- set vs. let ：letだと局所束縛の感じがするのでsetを選ぶ。defとsetは同じ。
- remark ： assertもあるが、assertは温存。
- conflict ： contradict（動詞）からconflict（動詞）に変更。contradiction（名詞）と紛らわしいから。
- produce ： あまり良くない。cause（動詞）もあるか？
- use assumption ： assumeと対になることを強調。ほぼブロックなのだが、ブロックにするのは辛い。
- for vs. fix ： fixはIsarで使っている。forもイマイチ。
- choice ： takeもあるが、ブロックだとお尻がend take、これ変じゃない？
カントールの対角線論法により、カントールの単射非存在定理を証明してみる。次の補題は仮定する。f_*はfの順像を作る関数。
次は、より簡単な補題。
- ∀X, Y:Set.∀f.[f:X→Y ∧ A⊆X ∧ a∈A) ⇒ f(a)∈f_*(A)] ---(値と像の補題)
// SerND カントールの定理
target
∀A:Set.¬∃f.(f:Pow(A)→A ∧ fは単射)
proof
for A:Set
target
¬∃f.(f:Pow(A)→A ∧ fは単射)
contradiction
∃f.(f:Pow(A)→A ∧ fは単射)
choice f
f:Pow(A)→A ∧ fは単射 ---(hyp)
set Ψ := {B∈Pow(A) | ¬(f(B)∈B) }
remark Ψ⊆Pow(A) ---(Ψは部分集合)
remark ∀S:Set.(S∈Ψ ⇔ ¬(f(S)∈S)) ---(Ψメンバー)
remark ∀S:Set.(¬(S∈Ψ) ⇔ f(S)∈S) ---(Ψ非メンバー)
set C := f_*(Ψ) ---(C定義)
remark C⊆A
remark C∈Pow(A)
by the way
logical axiom (排中律)
_A ∨ ¬_A
logically instantiage with f(C)∈C
f(C)∈C ∨ ¬(f(C)∈C)
cases
case 1
f(C)∈C ---(case1hyp)
apply (Ψ非メンバー)
¬(C∈Ψ) ---(CはΨ非メンバー)
cite (hyp)
f:Pow(A)→A ∧ fは単射
concat with (Ψは部分集合)
f:Pow(A)→A ∧ fは単射 ∧ Ψ⊆Pow(A)
concat with (CはΨ非メンバー)
f:Pow(A)→A ∧ fは単射 ∧ Ψ⊆Pow(A) ∧ ¬(C∈Ψ)
apply (単射補題)
¬(f(C)∈f_*(Ψ))
contract term $.1.2 by (C定義)
¬(f(C)∈C)
concat with (case1hyp)
¬(f(C)∈C) ∧ f(C)∈C
conflict
thus False
case 2
¬(f(C)∈C) ---(case2hyp)
apply (Ψメンバー)
C∈Ψ
concat with (hyp)$.1
C∈Ψ ∧ f:Pow(A)→A
concat with (Ψは部分集合)
C∈Ψ ∧ f:Pow(A)→A ∧ Ψ⊆Pow(A)
rewrite by (連言可換律)
f:Pow(A)→A ∧ Ψ⊆Pow(A) ∧ C∈Ψ
apply (値と像の補題)
f(C)∈f_*(Ψ)
contract $.2 by (C定義)
f(C)∈C
concat with (case2hyp)
f(C)∈C ∧ ¬(f(C)∈C)
conflict
thsu False
end cases
False
end contradiction
¬∃f.(f:Pow(A)→A ∧ fは単射)
introduce unversal
∀A:Set.¬∃f.(f:Pow(A)→A ∧ fは単射)
end for
∀A:Set.¬∃f.(f:Pow(A)→A ∧ fは単射)
end proof
∀A:Set.¬∃f.(f:Pow(A)→A ∧ fは単射) ---(カントールの定理)
