パスワードを忘れた? アカウント作成
10232046 journal
日記

iidaの日記: 選択公理と排中律 5

日記 by iida

書店で論理学の本を買った。ラムダ計算についても書いてあり、よさげに思ったからだ。第3章にとある定理が掲載されていた。いわく

選択公理が成立すれば、排中律が成立する。

そして、しかつめらしい証明が長々と書いてある。しかし、古典論理では常に排中律が成立するので、

常に排中律が成立する。ゆえに、「選択公理が成立すれば、排中律が成立する」は正しい。

で証明は終わりなのだ。

となると、著者は古典論理を前提としていないのだろうと読むべきであろう。ところが、どういう論理なのか、まるっきり書いていない。なまじ理解できるだけに、すっきりしない。

この議論は、iida (8060)によって テキとトモのテキ禁止として作成されたが、今となっては 新たにコメントを付けることはできません。
  • by tagga (31268) on 2013年11月19日 20時58分 (#2497930) 日記

    たぶん http://plato.stanford.edu/entries/axiom-choice/#AxiChoLog [stanford.edu] の話だと思います。

    注意が必要なのは、 証明に使うメタ論理体系と証明の対象である論理体系の区別です。 メタ論理体系の古典論理で排中律が公理であっても、 証明対象の体系では直観論理とZFCが公理なので、排中律は定理です。

    喩えてみると、 Common Lispで Scheme を実装したばあいに、 Common Lispで出来ることが Schemeで出来るとは単純には言えないという話です。

    • ご指摘ありがとうございます。このページは初見なので後日、拝見しようと思います。

      「証明対象の体系では直観論理」のとき、二重否定の除去を使っていない、ということがよくわかるような証明(図)であるべきだと思うのだが、そうなっていません。

      ふつう「(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
      親コメント
      • by superbaystars (46157) on 2013年11月20日 21時17分 (#2498455)
        じぶんのいたらなさってやつをうたがえよw
        親コメント
      • by tagga (31268) on 2013年11月21日 16時38分 (#2498871) 日記

        そういう直接的な手段をとれないので、工夫が要ります。

        リンク先のものでは、選択関数(リンク先の K)を適用する先を 工夫することで次のような展開をしています(述語を集合に直しています)。

        U = {x∈{0,1}|A∨x=0}, V = {x∈{0,1}|A∨x=1}とおく (ただし、0≠1)。 選択関数f があって f(U)∈U, f(V)∈V. 内包表示の式のxにそれぞれ代入して A∨f(U)=0, A∨f(V)=1.

        • 「A∨f(U)=0, A∨f(V)=1」 なので、A∨[f(U)=0∧f(V)=1]. さらに 0≠1 なので、A∨¬[f(U) = f(V)].
        • 「A を真と仮定すると U = V なので、f(U)=f(V)」から A→[f(U) = f(V)].
          • 『¬[f(U) = f(V)]を真と仮定したとき、「Aを真と仮定すると、f(U)=f(V) となり矛盾する」ので、¬A』なので¬[f(U) = f(V)]→¬A
        • この2つから、A∨¬A.

        拝察するに、上の展開ではなく、場合分けをしているようです。 いくつかの場合に A∨(矛盾)から A を示し、 残りの場合に、A を真と仮定すると矛盾することから、¬A を示している 論理展開だと思います。

        なお、直観論理では、 背理法「¬Aを真と仮定すると、矛盾するので、A」は言えませんが、 否定の導入「Aを真と仮定すると、矛盾するので、¬A」は言えます。 また、無限個では場合分けできる保証はありませんが、 有限個では網羅すればいいので場合分けができます。

        親コメント
typodupeerror

ナニゲにアレゲなのは、ナニゲなアレゲ -- アレゲ研究家

読み込み中...