Decision Procedure
決定手続き（Decision Procedure）
『真 理・証明・計算』のまえがきでも述べたように、この教科書の一つのねらいは「機械的手続き」でいったい何ができるか、という問いに立ち入ることである。す でに話を終えた「分析的推論」の一つの大きな特徴は、推論やトートロジーかどうかの判定が一定の機械的手続きでできる（簡単に言えば、確実に答えを出せる コンピュータのプログラムとして書ける）ようにすることであった。
自然演繹とヒルベルト流の公理系を眺めて、諸君らにもようやくわかってきたように、公理 的方法あるいは証明論の厳密さも、一つには種々の判定に同様な機械的方法が適用でき、曖昧さや不確定性を徹底的に排除できることから生じる。たとえば、与 えられた記号列がきちんとした論理式になっているかどうか、式の与えられた系列が証明になっているかどうかなどは、機械的手続きのみによって判定できるよ うになっている。このような手続きは「決定手続き」とよばれ、ヒルベルトが求めた本質的な条件の一つに他ならない。 では、少しおさらいをし、今後の展望にも立ち入ってみよう。
以上の疑問文に答えるのにフラフラ迷うようでは困るデ！しっかり復習せい！では、次の問題はどうじゃ？
- （７）一般に、すべての数学の問題には、決定手続きが存在するか？
- （８）そこまでいかなくとも、われわれがもうじきやる第５章の（一階）述語論理について、与えられた式が妥当（トートロジーよりは複雑だが、同じように反証不可能であること）かどうかを判定する決定手続きは存在するか？
- （９）おなじく、述語論理について適当な公理系を作れば、与えられた式が定理であるかどうかを判定する決定手続きは存在するか？
これらに対する答えはもう（わかる人には）わかっているが、それほど簡単にわかったわけではない。
Uchii, S. (1989) 『真理・証明・計算』ミネルヴァ書房、1989。