【検証論】5 ホーア論理の数学 （その5）

*** 5.2.2 完全性
 - 完全性：
   正しいものは全て、証明可能。
 - 完全性の定義をそのままホーア論理PHLに適用する。
   - PHL(PV,AV,S)が解釈Iに対して完全であるとは、
     I |= {A}P{B}であれば必ずPHL(PV,AV,S) |- {A}P{B}
     となることをいう。
 - あたりまえだが、これではゲーテルの不完全性定理の
   対象となり、ホーア論理は完全では無い、というこ
   とになる。
 - その様子
   - {True}skip{B}という表明付きプログラムについて
     考える。
     - これが正しいということ
       - I |= {True}skip{B}ということは、
         
         - 表明付きプログラムの意味論。
         - I |= True。
         - skipは状態を変えない、ということだけ。
           
         の3つから、I |= B と同値である。
     - これが証明可能であるということ
       - 次に{True}skip{B}がPHL(PV,AV,S)で証明可能
         であるとする。するとその証明は一般的に、証
         明アウトラインにて次の形で書くことができる。

         {True}{A1}...{An}skip{An}...{A2n-1}{B}

       - これが形式的に証明できるということは、
         
          - 表明付きプログラムの意味論
          - skip文の実行関係の特徴付け
          - 帰結規則の定義
            
         という3つから、次の論理式が真であることと
         同値である。

         True => A1, ... ,Ai => Ai+1, ... ,A2n-1 => B
         
       - ポイントは、これは表明に関する論理式なの
         で、PHL(PV,AV,S)全体を使って証明するので
         はなく、Sを非論理的公理とする一階述語論理
         (T(S)と書く)で証明するということだ。
       - すると、
      
         PHL(PV,AV,S) |- {True}{A1}...{An}skip{An}...{A2n-1}{B}

         は、

         T(S) |- True => A1, ... ,Ai => Ai+1, ... ,A2n-1 => B

         と同値であるということになる。

         ここで、先頭のTrueはトートロジなので常に
         真だから、さらには、

         T(S) |- B

         と同値であると言える。
    - まとめると、PHL(PV,AV,S)の完全性の定義が先の
      ようであるということは、

      PHL(PV,AV,S) |= {True}skip{B}
      ならば
      PHL(PV,AV,S) |- {True}skip{B}

      ということであり、これは上で調査したところ、

      I |= B
      ならば
      T(S) |- B

      と同値である。
      これは、ホーア論理の先の完全性の定義が、一階
      述語論理の完全性とリンクしていることを示して
      いる(ゲーデルの不完全性定理を考えるにあたっ
      て)。

 - やはりポイントは、T(S)というか表明の完全性の話
   題であるということ。
 - では、PHL(PV,AV,S)全体ではなくPHL(PV,AV,I)に限っ
   て考えたらどうか。
 - そうしても完全性は無条件には成り立たない。この
   点が健全性と違う。健全性はPHL(PV,AV,I)であれば
   無条件に成立した。
 - 無条件に成立しない様子
   - AVが極端に貧弱な場合、完全にならない。その様
     子を。
   - 例えば、整数の加減算のプログラムにおいて、AVの
     語彙として、add1/1とsub1/1の関数記号(関数)が
     与えられているとする。
   - すると、プログラム全体の前条件と後条件はこの
     語彙で表現できたとしても、プログラムの内部の
     中間表明がAVの語彙で表現できないことがある。
   - 例えば、
     x := x + y;
     x := x - y;
     とすると、xは結局xであるがこういことをadd1/1、
     sub1/1だけでは表現できない。表明にはwhileがな
     いからだ。なので、add/2やsub/2が必要になる。
   - というわけで、表明の語彙が貧弱だと、完全性だな
     んだかんだと言う前な感じで「形式的証明を原理的
     に記述不能」という状態になる。
 - では、貧弱じゃない語彙ってどういうものなの？と
   いうのが次項の話題。

刻んでるなぁ。。。
しかし一日一文字以上進む限り、いつかは終わる。

こつこつ。