「一階述語論理」の編集履歴（バックアップ）一覧に戻る
一階述語論理 - (2013/03/06 (水) 02:18:52) のソース
&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による定義
*健全性・完全性
古典一階述語論理は健全かつ完全である。
すなわち、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$$
----
#comment()
