「一階述語論理」の版間の差分
削除された内容 追加された内容
編集の要約なし |
編集の要約なし |
||
46行目:
* 定数記号はアリティ 0 の関数記号と呼ばれることもある。
* 上の定義では述語は 1 以上のアリティを持つとされているが、アリティ 0 の述語も考えることができ、それらは「真」や「偽」を意味するものと考えることができる。しかし「真」は ∀''x''(''x'' '''=''' ''x'') などと別の方法で表せるので、アリティ 0 の述語を導入することに大きな意味はない。
* 括弧の使い方の流儀は様々である。ある人は ∀''x'' を '''('''∀''x''''')''' と書く。括弧の代わりにコロンや終止符を使う場合もある。もちろんその場合には、言語にコロンや終止符を含めておく必要がある。
== 項と論理式 ==
53行目:
# ''t''<sub>1</sub> , ..., ''t''<sub>''n''</sub> が項で、''f'' がアリティ ''n'' の関数記号ならば、''f t''<sub>1</sub> … ''t''<sub>''n''</sub> は項である<ref>読みやすさを優先させて ''f t''<sub>1</sub> … ''t''<sub>''n''</sub> の代わりに ''f'' '''('''''t''<sub>1</sub>, …, ''t''<sub>''n''</sub>''')''' を用いる流儀も存在する。その場合は言語にカンマ "," を含めておく必要がある。</ref>。
# 上記の 1. と 2. によって項とされるものだけが項である。
項というのは直観的には議論領域に属するある対象を
例
: ''x''<sub>1</sub> , ''x''<sub>5</sub> , '''0''' , '''+''' ''x''<sub>1</sub>'''0''' , '''+ +''' ''x''<sub>1</sub>'''0'''''x''<sub>5</sub>
はすべて項である。 '''+''' ''x''<sub>1</sub>'''0''' や '''+ +''' ''x''<sub>1</sub>'''0'''''x''<sub>5</sub> は極めて読みにくいため、通常、これらの項を表すのに ''x''<sub>1</sub> '''+ 0''' や (''x''<sub>1</sub> '''+ 0''') '''+''' ''x''<sub>5</sub> のような表現が用いられる。
項が何らかの対象を表す記号列であったのに対して、'''
原子論理式を用いて、'''整論理式''' (well-formed formula, wff) あるいは'''論理式''' (formula) は次のように帰納的に定義される：
# 原子論理式は論理式である。
#
# φ が論理式で ''x'
# 上記の 1. と 2. と 3. によって論理式とされるものだけが論理式である。
例． 再び自然数論の言語を考える。定義から、
:
は原子論理式
'''代入： ''' ''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'' とすることで問題を回避する。これを忘れるとひどい間違いを犯すことになる。▼
== 自由変数 ==
77 ⟶ 76行目:
== 論理式の真偽 ==
== 論理的帰結 ==
== 形式的証明 ==
== 代入 ==
▲'''代入： ''' ''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'' とすることで問題を回避する。これを忘れるとひどい間違いを犯すことになる。
== 同一性 ==
98 ⟶ 100行目:
ここでの定式化で用いられる命題論理の推論規則は、[[モーダス・ポネンス]]のみである。これは、φ と φ → ψ がともに証明されていれば、ψ を導いてよいというものである。
[[
: ├ φ ならば ├ ∀''x''φ
<!-- : <math>\mathrm{if} \vdash \phi, \mathrm{then} \vdash \forall x \phi</math> -->
104 ⟶ 106行目:
<!-- Universal Generalization が 汎化 でいいのか自信なし（訳者）-->
: ├ ''P'' ならば ├ □''P''
<!-- :<math>\mathrm{if} \vdash P, \mathrm{then} \vdash \Box P.</math> -->
133 ⟶ 135行目:
証明可能性については様々な異なる（しかし互いに等価な）定義の方法がある。上述の定義は[[ダフィット・ヒルベルト|ヒルベルト]]流計算の典型例であり、これは異なる公理を多数用意して推論規則を少なくするスタイルをとっている。[[ゲルハルト・ゲンツェン|ゲンツェン]]流の[[シークエント計算|述語計算]]では逆に、公理を少なくして推論規則を豊富に用意している。
== 健全性と完全性 ==
== 一階述語論理に関する定理 ==
以下、健全性定理と完全性定理以外の重要なメタ
# 命題計算とは異なり、一階述語論理は（高々[[アリティ]]2の述語が一つでも含まれていると）決定不能である。つまり、任意の論理式 ''P'' について、''P'' が恒真であるか否かを決定する一般的なアルゴリズムは存在しない（[[チューリングマシンの停止問題]]を参照せよ）。この結果は[[アロンゾ・チャーチ]]と[[アラン・チューリング]]がそれぞれ独立に導き出した。
# ただし、与えられた文（論理式）が恒真であるとき、かつそのときにのみ停止するチューリングマシンは存在する。逆に恒真でない論理式の場合は判定が停止しないかもしれない。これを「部分決定性がある」という。
| |||