記号論理

ウィキペディア小見出し辞書

記号論理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/06/12 02:07 UTC 版)

「数理論理学」の記事における「記号論理」の解説

レオポルト・レーヴェンハイム（1915）とトアルフ・スコーレム（1920）はレーヴェンハイム-スコーレムの定理を得た。これは一階述語論理は無限構造の濃度を制御できないことを述べる。スコーレムは、この定理を一階で形式化された集合論へ適用でき、そのいかなる形式化も可算モデルを持つことが導かれる、ということに気付いた。この直観に反する結果はスコーレムのパラドックスとして知られることになった。 ゲーデルは自身の博士論文（1929）において完全性定理を示した。これは一階論理における構文論と意味論の間の対応を確立する。ゲーデルは完全性定理をコンパクト性定理の証明に用いた。これは一階の論理的帰結の有限性を立証する。これらの結果は一階論理を数学者にとって支配的な論理として確立することを助けた。 1931年、ゲーデルはプリンキピア・マテマティカとそれに関連する体系において形式的に決定不可能な命題について（英語版）を出版した。ここでは、十分に強く、実効的な一階理論が不完全（完全性定理のそれとは異なる意味である）であることを示されている。この結果はゲーデルの不完全性定理として知られ、数学の公理的基礎の厳密な限界を示すものであり、ヒルベルト・プログラムに大きな打撃を与えた。これは算術の無矛盾性をいかなる算術の形式理論においても証明できないことを示している。しかしながら、ヒルベルトは、不完全性定理の重要性を、あるときまで認めなかった。 ゲーデルの定理は、十分に強く、実効的な公理系の無矛盾性の証明は、それが無矛盾である限り、それ自身からも、それよりも弱い体系からも、得られないことを示す。これはいま考えている体系で形式化できないような無矛盾性証明の可能性については未解決のまま残す。ゲンツェン（1936）は算術の無矛盾性を超限帰納法の原理を持つ有限的な体系を用いて証明した。ゲンツェンの結果はカット除去と証明論的順序数の概念を生み出し、これらは証明論における主要な道具となった。ゲーデル（1958）は別の無矛盾性証明を与えた。これは古典算術の無矛盾性を高階直観主義算術の無矛盾性に還元することで為された。