「一階述語論理」の版間の差分
削除された内容 追加された内容
編集の要約なし |
編集の要約なし |
||
124行目:
=== 論理公理 ===
以下の形の
*トートロジー（命題論理におけるトートロジーの命題記号を一階の論理式で置き換えて得られる論理式）
*量化記号に関する公理
144行目:
==== 全称化 (GEN) ====
全称化規則とは、''x'' が
:GEN = { (
(φ<sub>1</sub>, φ<sub>2</sub>) ∈ GEN であるとき、φ<sub>2</sub> は φ<sub>1</sub> からの全称化による導出であるという。
166行目:
:#''c'' 定数記号ならば、''c''<sub>''x''</sub> [ ''t'' ] = ''c'' 。
:#''t''<sub>1</sub> , ..., ''t''<sub>''n''</sub> が項で、''f'' がアリティ ''n'' の関数記号ならば、(''f t''<sub>1</sub> … ''t''<sub>''n''</sub>)<sub>''x''</sub> [ ''t'' ] = ''f'' (''t''<sub>1</sub>)<sub>''x''</sub> [ ''t'' ] … (''t''<sub>''n''</sub>)<sub>''x''</sub> [ ''t'' ] 。
:そして、φ<sub>''x''</sub> [ ''t'' ] を次のように再帰的に定義する：
:#原子論理式 ''P t''<sub>1</sub> … ''t''<sub>''n''</sub> に対しては、(''P t''<sub>1</sub> … ''t''<sub>''n''</sub>)<sub>''x''</sub> [ ''t'' ] = ''P'' (''t''<sub>1</sub>)<sub>''x''</sub> [ ''t'' ] … (''t''<sub>''n''</sub>)<sub>''x''</sub> [ ''t'' ] 。
:#'''('''¬ φ''')'''<sub>''x''</sub> [ ''t'' ] = '''('''¬ φ<sub>''x''</sub> [ ''t'' ]''')'''
200行目:
== 健全性と完全性 ==
:<math>\Sigma\vdash\varphi \Longrightarrow \Sigma \vDash \varphi</math>
:<math>\Sigma\vDash\varphi \Longrightarrow \Sigma \vdash \varphi</math>
| |||