【シプサ】6 計算可能性の理論における先進的な話題 (その4)

休日にもう少しすすめたらうれしい。

• "AN UNDECIDABLE THEORY"
  
  
• この節は、詳細な証明(確認)をするのでなく、考え方をざくっとしめすもののようだ。それにそって進みたい。
  
  
• THEOREM 6.13
  Th(N,+,x) is undecidable.
  
• これがこの節のひとつめのお題。
  
• 確認の方針は、A[TM]をTh(N,+,x)に帰着させる、ということ。手法には計算履歴を使う。
  
  
  
  • LEMMA 6.14
    TM Mと入力wがあるとする。これらから、とある論理式をつくることができる。それをΦ[M,w]と呼ぶ。どんな論理式かというと、Mがwを受理するときに限り∃xΦ[M,w]がモデル(N,+,x)にてtrueとなる、すなわちthe language of Th(N,+,x)となるような論理式である。
    
  • これの証明というか、このような機構を構築することはかなり面倒。
    
  • ここでは、これが構築できる、ということにしておく。
    
  
  
• LENNMA 6.14は写像帰着であるから、A[TM] <=m Th(N,+,x) である。よって、A[TM]は判定不可能性により、Th(N,+,x)は判定不可能であるといえる。■
  
  
• 次のお題は、ゲーデルの不完全性定理。
  
• 完全な証明ではなく、そのスケッチをみてみる。
  
• ゲーデルの不完全性定理を簡単に言うと
  「数論において、証明形式や方式についていかなるものを採用したとしても、それをつかって証明不能な数学的言明が存在する」
  ということ。
  
• 証明(proof)の正確な定義を構成する余裕はこの本ではない。
  
• そこで簡単に言うと、
  
  
  
  • 言明Φに対する形式的証明πとは、言明の列である。
    
  • その列をS1, S2, ..., Slと表すとする。
    
  • SlはΦである。
    
  • Siは、Siより前の言明と数に関する基本的な公理とをもとにして、形式化された含意ルール(implication)によって導かれる。
    
  
  
• さて、話しを進めるために次の2つが成り立つと仮定しちゃおう。
  
  
  
  • 1. {<Φ,π> | π is a proof of Φ } は 判定可能。
    
  • 2. ここで採用する証明システムは健全である。すなわち、ある言明の証明が存在するならば、その言明はtrueである。
    
  
  
  
• THEOREM 6.15
  Th(N,+,x)をもとにして証明可能な言明を集めた部分集合をつくると、それはTuring認識可能である。
  
• これの証明は簡単。上記1を使えばよい。
  
  
• THEOREM 6.16 (不完全性定理 Th(N,+,x)版)
  Th(N,+,x)の一部の言明は、証明不可能である。
  
  
  
  • 背理法で確認していく。
    
  • 「Th(N,+,x)の全ての言明(すなわちtrueとなる言明)は証明可能である」とする。
    
  • この仮定を利用してアルゴリズムDを構成する。
    
  • さて、THEOREM6.15の認識可能ということを実現するアルゴリズムをPとする。
    
  • 言明入力Φから、Φと¬Φをつくり、双方についてアルゴリズムPを適用させる。
    
  • Φと¬Φのどちらかはtrueだから、仮定によると、そのtrueな方は証明可能である。
    
  • これはまさにTHEOREM6.15によって認識可能ということだから、先のアルゴリズムPの適用はどちらかが受理し停止する。
    
  • さて、どちらで受理したとしても、受理した方がtrueである。これは上の2によって保証されている。すなわち、Φで受理すれば、Φはtrue。¬Φで受理すれば、Φはfalse。
    
  • このアルゴリズムDは、Th(N,+,x)を判定している。これはTHEOREM6.13に反している。よって仮定は間違いである。■
    
  
  
  
• うわ、次、再帰定理を使うのか。。。
  
  
• 再帰定理を使って、(N,+,x)に関する言明で証明不可能なものを作ってみる、ということ。
  
  
• 次のようにTM Sを構成する。
  
  
  
  • あらゆる入力に対して次のように動作する。
    
  • 1. 再帰定理を使って、自分自身の記述<S>を得る。
    
  • 2. LEMMA 6.14をつかって、言明ψ = ¬∃c [Φ[S,0]] を構成する。
    
  • 3. THEOREM6.15のアルゴリズムPを、入力ψにて動作させる。
    
  • 4. 3で受理すれば受理、拒否すれば拒否。
    
  
  
• 実はこのψが、trueだがunprovableな言明である。それを確かめる。
  
  
• 入力を(どうせ無視するが)0としておこう。
  
• TM Sは受理するか拒否するか、である。
  
  
• TM Sが受理するのは、3.でPが受理したとき。
  
• Pが受理するということは、言明ψが証明可能ということ。
  
• 一方、TM Sは受理するんだから、∃c [Φ[S,0]] はtrue。
  
• ということは、¬∃c [Φ[S,0]] = ψ がfalse。
  
• あり、このケースは、falseなものが証明可能となっている、というケースであることがわかった。
  
• これは証明システムの事実2.に反している。
  
• よってこのケースは発生しえない。
  
  
• というわけで、次のケースが発生することがわかった。
  
  
• TM Sが拒否するのは、3.でPが拒否したとき。
  
• Pが受理するということは、言明ψが証明不可能ということ。
  
• 一方、TM Sは拒否するんだから、∃c [Φ[S,0]] はfalse。
  
• ということは、¬∃c [Φ[S,0]] = ψ がtrue。
  
  
• ψは、証明不可能かつtrueである。■
  

こつこつ。次回は「Turing帰着性」。