論理学的背景
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/05/28 07:09 UTC 版)
論理学の起源はアリストテレスまで遡るが、現代的数理論理学は19世紀末から20世紀初頭に発展した。フレーゲの『概念記法』(1879) が完全な命題論理と一階述語論理の基本的なものを導入。同じくフレーゲの『算術の基礎』(1884)でも、形式論理の数学（の一部）を説明している。この流れを受け継いだのがラッセルとホワイトヘッドの『プリンキピア・マテマティカ』で、初版は1910年から1913年に出版され、1927年に第2版が出ている。ラッセルとホワイトヘッドは、公理と形式論理の推論規則からあらゆる数学的真理が導き出せると考え、証明自動化への道を拓いた。1920年、トアルフ・スコーレムはレオポールト・レーヴェンハイム（英語版）の成果を単純化したレーヴェンハイム-スコーレムの定理をもたらし、1930年にはエルブラン領域とエルブラン解釈により、一階の論理式の充足（不）可能性（および定理の妥当性）を命題論理の充足可能性問題に還元できることが示された。 1929年、Mojżesz Presburger はプレスブルガー算術（加法と等号のある自然数の理論）が決定可能であり、その言語内の任意の文の真偽を判定できるアルゴリズムを示した。しかしその直後、クルト・ゲーデルが Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I (1931) を発表し、十分に強力な公理系はその体系内で証明も反証もできない文を含みうることを示した。1930年代にこの課題を研究したのがアロンゾ・チャーチとアラン・チューリングで、それぞれ独自に等価な計算可能性の定義を与え、決定不能な具体例も示した。
※この「論理学的背景」の解説は、「自動定理証明」の解説の一部です。
「論理学的背景」を含む「自動定理証明」の記事については、「自動定理証明」の概要を参照ください。
- 論理学的背景のページへのリンク
