一階述語論理と完全性

一階述語論理は、対象と関係に関する量化された命題の形式言語であり、ゲーデルの完全性定理は、その証明体系がすべての解釈において真となる命題を正確に捉えていることを示しています。

Definition

一階述語論理は、対象の領域にわたる量化子と、関係、関数、定数記号を用いて命題論理を拡張したものです。完全性定理は、ある命題がその証明体系において導出可能であるのは、それが仮定された公理の論理的帰結である場合に限る、と述べています。

Scope

このトピックでは、一階述語論理の言語、項、論理式、および命題の構文、構造と充足のセマンティクス、妥当性と論理的帰結の概念、一階述語論理の演繹体系、および証明可能性と真理を結びつける健全性定理と完全性定理について扱います。

Core questions

• 一階述語論理の正確な構文と意味論は何ですか？
• ある命題が理論の論理的帰結であるとはどういう意味ですか？
• なぜすべての妥当な命題は形式的に証明可能なのですか？
• 完全性はいかにして証明体系とすべてのモデルのクラスを結びつけるのですか？

Key theories

健全性定理

証明体系において導出可能なすべての命題は、前提のすべてのモデルにおいて真であるため、演繹体系は決して誤った帰結を証明することはありません。

ゲーデルの完全性定理

逆に、ある理論のすべてのモデルで成り立つすべての命題は、その理論から導出可能であるため、一階述語論理においては証明可能性と論理的帰結が一致します。

ヘンキン構成

完全性は、存在命題の証人を持つ極大無矛盾な命題の集合から直接モデルを構築することによって証明され、モデルを構築するための構文的な手順を提供します。

Clinical relevance

一階述語論理は、数学的理論を形式化するための標準的な枠組みであり、完全性は、すべてのモデルに共通する任意の意味論的真理が原理的には証明可能であることを保証し、自動定理証明と公理的体系の基礎的妥当性を支えています。

History

一階述語論理はフレーゲの『概念記法』から生まれ、ヒルベルトとアッカーマンによって独立した体系として確立されました。ゲーデルは1929年の博士論文で完全性を証明し、ヘンキンは1949年の構成法で、今日標準となっている、極大無矛盾集合を用いた簡潔な証明を与えました。

Key figures

• Gottlob Frege
• Kurt Goedel
• Leon Henkin
• Alfred Tarski

Seminal works

• enderton2001
• marker2002
• shoenfield1967

Frequently asked questions

完全性定理はゲーデルの不完全性定理とどう異なりますか？

完全性定理は論理的帰結に関するものであり、ある理論のすべてのモデルで真であるすべての命題は証明可能である、と述べます。不完全性定理は特定の理論に関するものであり、十分に強力な無矛盾な理論には、その意図されたモデルで真であるが証明できない命題が存在する、と述べます。これら二つは異なる概念に関わるものであり、矛盾するものではありません。

なぜ一階述語論理が標準的な選択肢なのですか？

それは、ほとんどの数学を形式化するのに十分な表現力を持つ一方で、完全性とコンパクト性を享受しており、これらは二階述語論理のようなより強力な論理では成り立ちません。この表現力と良好なメタ理論的特性のバランスが、それをデフォルトの論理的枠組みにしています。