iidaの日記: 選択公理と排中律 5
日記 by
iida
書店で論理学の本を買った。ラムダ計算についても書いてあり、よさげに思ったからだ。第3章にとある定理が掲載されていた。いわく
選択公理が成立すれば、排中律が成立する。
そして、しかつめらしい証明が長々と書いてある。しかし、古典論理では常に排中律が成立するので、
常に排中律が成立する。ゆえに、「選択公理が成立すれば、排中律が成立する」は正しい。
で証明は終わりなのだ。
となると、著者は古典論理を前提としていないのだろうと読むべきであろう。ところが、どういう論理なのか、まるっきり書いていない。なまじ理解できるだけに、すっきりしない。
論理とメタ論理 (スコア:1)
たぶん http://plato.stanford.edu/entries/axiom-choice/#AxiChoLog [stanford.edu] の話だと思います。
注意が必要なのは、 証明に使うメタ論理体系と証明の対象である論理体系の区別です。 メタ論理体系の古典論理で排中律が公理であっても、 証明対象の体系では直観論理とZFCが公理なので、排中律は定理です。
喩えてみると、 Common Lispで Scheme を実装したばあいに、 Common Lispで出来ることが Schemeで出来るとは単純には言えないという話です。
Re:論理とメタ論理 (スコア:1)
「証明対象の体系では直観論理」のとき、二重否定の除去を使っていない、ということがよくわかるような証明(図)であるべきだと思うのだが、そうなっていません。
ふつう「(A)∨(¬A)」を証明するには、
a.もし「A」が証明できれば∨入れするところだが、今回は無理。
b.もし「¬A」が証明できても∨入れするところだが、当然これも無理。
c.もし適当な命題Pについて「P⊃((A)∨(¬A))」と「P」の両方が証明できれば、⊃とりすればよい。
d.もし適当な命題Pについて「P∨((A)∨(¬A))」と「¬P」の両方が証明できれば、∨とりすればよい(Pが右側でも同様)。
あたりでしょう。
したがってa.以外の証明であれば、必ず「¬A」の真偽が問題になるはず。
しかし、この本の証明に「A」の真偽は登場するのだが、「¬A」の真偽については一言も出てこないので、どういう論理展開をしたかったのかがさっぱり読めない。
おまけに真と偽が誤植されている箇所が1つある。幸い、証明全体には波及していないが。
完全に邪推だが、もし学才があって文才のない学者が、学才がなく文才のある学生に書かせて、査読抜きで刊行したとしたら、こんな本になるのかなあ。
iida
Re:論理とメタ論理 (スコア:1)
Re:論理とメタ論理 (スコア:1)
そういう直接的な手段をとれないので、工夫が要ります。
リンク先のものでは、選択関数(リンク先の K)を適用する先を 工夫することで次のような展開をしています(述語を集合に直しています)。
拝察するに、上の展開ではなく、場合分けをしているようです。 いくつかの場合に A∨(矛盾)から A を示し、 残りの場合に、A を真と仮定すると矛盾することから、¬A を示している 論理展開だと思います。
なお、直観論理では、 背理法「¬Aを真と仮定すると、矛盾するので、A」は言えませんが、 否定の導入「Aを真と仮定すると、矛盾するので、¬A」は言えます。 また、無限個では場合分けできる保証はありませんが、 有限個では網羅すればいいので場合分けができます。
Re:論理とメタ論理 (スコア:1)
iida