11/06/11 08:16:13.89
>>722
> >>719
> > LKの証明図を逆にたどる方法での証明を考えてみよう。
> ん・・・わからんですｗ
> 「式Aがvalid → Aの証明が存在する」を示すことについて言ってるんですよね？
> validであることから証明図へのとっかかりが何なのかわからんです。
完全性定理の証明に選択公理かそれに近い言明が必要な理由を説明してるんだと思う。
（シュッテ流の証明といわれるもの。）
>
> >>720
> > 解析学でコーシーの定理を証明するのと同じことだよ。
> 一瞬戸惑ったｗ
> たとえ話、ですよね？
そうです。
どちらも習慣による数学に基いてるということ。
ZFC、NGB、ニュー・ファンデーション、トポス...何によって
形式化されるかは不明だし、知る必要もないです。
ただし、議論領域がどういった数学に基いているのかとは別の話です。