「一階述語論理」の編集履歴（バックアップ）一覧はこちら
「一階述語論理」(2013/03/07 (木) 03:19:02) の最新版変更点
追加された行は緑色になります。
削除された行は赤色になります。
&tags()
----
#contents()
*言語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$$はモデルを持つ。
----
#comment()
&tags()
----
#contents()
*言語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は無矛盾性を証明することができることが分かっている。
----
#comment()
