数学のエキスパートシステムは作れるか?決定問題

与えられた命題の真偽や証明可能性を判定する有限の手続きを求める問題。古くは17世紀の哲学者ライプニッツも普遍機械という形で決定問題の解決を夢みたと言われている。ヒルベルトは「1階論理の決定問題は数理論理学の主問題である」と述べた。ゲーデルが不完全性定理により初等算術の決定手続きがないことを示した後、チャーチ【チャーチ】米国の数学者。計算可能性の概念が計算モデルに依存しないことを主張する「チャーチ=チューリングの提唱」が有名。1936年に「記号論理学会」を設立し、専門誌を発行するなどして、学問としての現代論理学の基礎を築いた。チューリング、ロッサー、ヘンキン、スマリヤンらの博士指導教官。 とチューリングが純粋1階論理の決定問題を否定的に解いた。 他方、ラムジー【ラムジー】 ラムジーは経済学者ケインズの弟子。ラッセルの型理論を改良。26歳で夭折。 は組合せ的急増加関数を考案し、特殊な形の1階論理式の決定手続きを示し、後にパリスとハーリントンはそれから新種の決定不能命題を作った。