一階述語論理


※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。



言語L

言語LにおけるL項、L論理式を定義しておく。

L項
t := x | f(t_1,...,t_n)

L論理式
\varphi, \psi := p(t_1,...,t_n) | \top | \bot | (\varphi \wedge \psi) | (\varphi \vee \psi) | (\varphi \rightarrow \psi) | \forall x.\varphi | \exists x.\varphi

こうして定義された言語Lによって記述される論理を一階述語論理と呼ぶ。
形式的証明を定義するためにいくつかの公理と推論規則を定めるが、これらの定め方はいくつかあることが知られている。


Hilbertによる定義

Gentzenによる定義


モデル

\SigmaをL論理式の集合とする。このとき
\boldsymbol{A}\Sigmaのモデル  \:\: \Leftrightarrow \:\: \forall \psi \in \Sigma. \:\: \boldsymbol{A} \vDash \psi

完全性定理

古典一階述語論理は健全かつ完全である。
すなわち、Lを言語、\SigmaをL文の集合、\varphiをL文とすると
\Sigma \vDash \varphi \: \Leftrightarrow \: \Sigma \vdash \varphi
が成り立つ。

健全性 \Sigma \vdash \varphi \:\: \Rightarrow \:\: \Sigma \vDash \varphi
完全性 \Sigma \vDash \varphi \:\: \Rightarrow \:\: \Sigma \vdash \varphi

また、以下は完全性定理と同値な命題である。
\Sigmaが無矛盾(i.e. \Sigma \nvdash \bot) \:\: \Leftrightarrow \:\: \Sigmaはモデルを持つ。


Gödelの不完全性定理


  • 第1不完全性定理
Tを\mathbf{Q}の再帰的拡大とする。Tがω無矛盾であれば、不完全である。
  • 第2不完全性定理
Tを\mathbf{PA}の再帰的拡大とする。Tが無矛盾であれば、TではTの無矛盾性を証明できない。


なお、第2不完全性定理について、局所的にはTは無矛盾性を証明することができることが分かっている。


名前:
コメント: