Logic Seminar

Decision Procedure


決定手続き(Decision Procedure)

『真 理・証明・計算』のまえがきでも述べたように、この教科書の一つのねらいは「機械的手続き」でいったい何ができるか、という問いに立ち入ることである。す でに話を終えた「分析的推論」の一つの大きな特徴は、推論やトートロジーかどうかの判定が一定の機械的手続きでできる(簡単に言えば、確実に答えを出せる コンピュータのプログラムとして書ける)ようにすることであった。

自然演繹とヒルベルト流の公理系を眺めて、諸君らにもようやくわかってきたように、公理 的方法あるいは証明論の厳密さも、一つには種々の判定に同様な機械的方法が適用でき、曖昧さや不確定性を徹底的に排除できることから生じる。たとえば、与 えられた記号列がきちんとした論理式になっているかどうか、式の与えられた系列が証明になっているかどうかなどは、機械的手続きのみによって判定できるよ うになっている。このような手続きは「決定手続き」とよばれ、ヒルベルトが求めた本質的な条件の一つに他ならない。 では、少しおさらいをし、今後の展望にも立ち入ってみよう。

以上の疑問文に答えるのにフラフラ迷うようでは困るデ!しっかり復習せい!では、次の問題はどうじゃ?

これらに対する答えはもう(わかる人には)わかっているが、それほど簡単にわかったわけではない。

 

Uchii, S. (1989) 『真理・証明・計算』ミネルヴァ書房、1989。


Last modified May 27, 2008. (c) Soshichi Uchii