「一階述語論理」の版間の差分
削除された内容 追加された内容
編集の要約なし |
編集の要約なし |
||
115行目:
=== 論理的帰結 ===
Σ を論理式の集合とし、φ を論理式とする。Σ に属するすべての論理式 ψ に対して ''M''(ψ, ''s'') = 1 であるような任意の解釈 ''M'' と ''M'' の個体の割り当て関数 ''s'' が ''M''(φ, ''s'') = 1 をみたすとき、φ は Σ の'''論理的帰結''' (logical consquence) であるといい、<math>\Sigma \vDash \varphi</math> と書く。論理式 φ と ψ が <math>\{\varphi\} \vDash \psi</math> かつ <math>\{\psi\} \vDash \varphi</math> をみたすとき、φ と ψ は'''論理的に同値''' (logically equivalent) であるという。また、φ が ∅ の論理的帰結である場合、すなわち任意の解釈 ''M'' と ''M'' の個体の割り当て関数 ''s'' に対して ''M''(φ, ''s'') = 1 であるとき、φ は'''恒真''' (valid) であるという。φ と ψ が論理的に同値であることは、'''('''φ ↔ ψ''')''' が恒真であることと同値である。
== 形式的証明 ==
123行目:
=== 論理公理 ===
一階述語論理で採用される論理公理は以下のものである：
*すべてのトートロジー（命題論理のトートロジーにおける命題記号を一階の論理式で置き換えたもの）
*量化子について
*同一性についての上述の公理（同一性を論理に含める場合）▼
<!-- * PRED-1: <math> \forall x Z(x) \rightarrow Z(y) </math> -->▼
<!-- * PRED-2: <math> Z(y) \rightarrow \exists x Z(x) </math> -->▼
<!-- * PRED-3: <math> \forall x (W \rightarrow Z(x)) \rightarrow (W \rightarrow \forall x Z(x)) </math> -->▼
<!-- * PRED-4: <math> \forall x (Z(x) \rightarrow W) \rightarrow (\exists x Z(x) \rightarrow W) </math> -->▼
これらは実際には公理図式である。ここで、表現 ''W'' は任意の整論理式であり、''x'' は自由変項ではない。また、表現 ''Z''(''x'') は任意の整論理式であり、''Z''(''y'') は同じ論理式中の ''x'' の自由な出現を全て ''y'' で置換したものを表す。▼
=== 推論規則 ===
推論規則とは、あるいくつかの論理式から別の論理式を導出するための規則である。これは正確には、論理式全体の集合の上の関係として定義される。推論規則には様々なものが考えられるが、ここで用いる推論規則は'''モーダス・ポーネンス''' (modus ponens) と呼ばれる規則と'''全称化''' (generalization) と呼ばれる規則の二つである。
ここでの定式化で用いられる命題論理の推論規則は、[[モーダス・ポネンス]]のみである。これは、φ と φ → ψ がともに証明されていれば、ψ を導いてよいというものである。▼
==== モーダス・ポーネンス (MP) ====
[[全称化]]と呼ばれる推論規則は述語論理に特有のものである。これは、以下のように定義される。▼
▲
: ├ φ ならば ├ ∀''x''φ▼
==== 全称化 (GEN) ====
証明可能性については様々な異なる（しかし互いに等価な）定義の方法がある。上述の定義は[[ダフィット・ヒルベルト|ヒルベルト]]流計算の典型例であり、これは異なる公理を多数用意して推論規則を少なくするスタイルをとっている。[[ゲルハルト・ゲンツェン|ゲンツェン]]流の[[シークエント計算|述語計算]]では逆に、公理を少なくして推論規則を豊富に用意している。「[[自然演繹]]」「[[シークエント計算]]」などを参照。▼
=== 証明可能性 ===
論理式 φ 論理式の集合 Σ から証明可能であるとは、Σ に属する論理式と論理公理から推論規則の有限回の適用によって φ が得られることを意味する。そして、Σ に属する論理式と論理公理から φ を導出する仮定を示した論理式の有限列を、Σ からの φ の形式的証明とよぶ。これらの概念は次のように厳密に定義することができる。
:φ を論理式、Σ を論理式の集合とする。Σ からの φ の'''形式的証明''' (formal proof) あるいは'''証明'''
:#φ<sub>''n''</sub> = φ 。
:#''n'' 以下の任意の自然数 ''k'' に対して、次のいずれかが成り立つ：
:::(a) φ<sub>''k''</sub> ∈ Σ 。
:&Sigma からの &phi の証明が存在するとき、φ は Σ から'''証明可能'''であるといい、<math>\Sigma\vdash\varphi</math> と書く。▼
:::(b) φ<sub>''k''</sub> は論理公理である。
:::(c) ある ''i'', ''j'' < ''k'' が存在して、φ<sub>''k''</sub> は φ<sub>''i''</sub> , φ<sub>''j''</sub> からのモーダス・ポーネンスによる導出である。
:::(d) ある ''i'' < ''k'' が存在して、φ<sub>''k''</sub> は φ<sub>''i''</sub> からの全称化による導出である。
▲:Σ からの φ の証明が存在するとき、φ は Σ から'''証明可能''' (provable) である、あるいは φ は Σ の'''定理''' (theorem) であるといい、<math>\Sigma\vdash\varphi</math> と書く。
▲証明可能性については様々な異なる（しかし互いに等価な）定義の方法がある。上述の定義は[[ダフィット・ヒルベルト|ヒルベルト]]流計算の典型例であり、これは異なる公理を多数用意して推論規則を少なくするスタイルをとっている。[[ゲルハルト・ゲンツェン|ゲンツェン]]流の[[シークエント計算|述語計算]]では逆に、公理を少なくして推論規則を豊富に用意している。ここで述べたやり方とは異なる証明可能性の定義については「[[自然演繹]]」「[[シークエント計算]]」などを参照。
=== 代入に関して ===
''t'' を項、 φ(''x'') を（''x''を自由変項として含む）論理式とする。このとき φ(''t'') は、φ(''x'') 中の ''x'' の自由な出現すべてを ''t'' で置き換えたものと定義される。'''ただしここで、''t'' に含まれるいかなる自由変項も、この置き換えによって束縛されてしまうことがないようにしなければならない'''。もし ''t'' の自由変項が束縛されるなら、''x'' を ''t'' で置換する前に φ 内の[[束縛変項]]名を ''t'' 内の自由変項名以外のものに変更しなければならない。この条件が必要となる理由を説明するために、以下のような場合を考えてみよう。論理式 φ(''x'') の中身が ∀''y'' ''y'' ≤ ''x''（これは「''x'' は最大値」を意味する）だとする。''t'' が ''y'' を自由変項として持たない項であれば、φ(''t'') はまさに ''t'' が最大値であると主張していることになる。しかし、もし ''t'' が ''y'' である場合、φ(''t'') は ∀''y'' ''y'' ≤ ''y'' となり、主張することが変わってしまう。この問題は、自由変項 ''x'' に ''y'' を代入したときに、φ(''x'') の中で ''t'' の自由変項 ''y'' が束縛されてしまうために発生する。そこで、事前に束縛変項 ''y'' を他の名前、例えば ''z'' に変えて、∀''z'' ''z'' ≤ ''y'' とすることで問題を回避する。これを忘れるとひどい間違いを犯すことになる。
=== 同一性に関する公理 ===
一階述語論理での同一性に関する規約には様々なものがあるが、ここではそのうち主なものを要約する。どの規約に従っても同じ結果が（ほぼ同じ手数で）得られ、違うのは主に用語法だけである。
162 ⟶ 176行目:
::∃''x''(''P''(''x'') ∧ ∀''y''(''P''(''y'') → (''x'' = ''y'')))
:これは一般に、∃!''xP''(''x'') と略記される。
▲* PRED-1: ∀''xZ''(''x'') → ''Z''(''y'')
▲* PRED-2: ''Z''(''y'') → ∃''xZ''(''x'')
▲* PRED-3: ∀''x''(''W'' → ''Z''(''x'')) → (''W'' → ∀''xZ''(''x''))
▲* PRED-4: ∀''x''(''Z''(''x'') → ''W'') → (∃''xZ''(''x'') → ''W'')
▲<!-- * PRED-1: <math> \forall x Z(x) \rightarrow Z(y) </math> -->
▲<!-- * PRED-2: <math> Z(y) \rightarrow \exists x Z(x) </math> -->
▲<!-- * PRED-3: <math> \forall x (W \rightarrow Z(x)) \rightarrow (W \rightarrow \forall x Z(x)) </math> -->
▲<!-- * PRED-4: <math> \forall x (Z(x) \rightarrow W) \rightarrow (\exists x Z(x) \rightarrow W) </math> -->
▲これらは実際には公理図式である。ここで、表現 ''W'' は任意の整論理式であり、''x'' は自由変項ではない。また、表現 ''Z''(''x'') は任意の整論理式であり、''Z''(''y'') は同じ論理式中の ''x'' の自由な出現を全て ''y'' で置換したものを表す。
== 健全性と完全性 ==
== 一階述語論理に関する定理 ==
| |||