「一階述語論理」の版間の差分
削除された内容 追加された内容
編集の要約なし |
編集の要約なし |
||
7行目:
:ソクラテスは人間である。
:したがってソクラテスは死ぬ。
一階述語論理では、このような「すべての…について」という表現や、また「ある…について」といった表現を扱えるように、'''全称量化記号''' (universal quantifier) と呼ばれる記号 ∀ と'''存在量化記号''' (existential quantifier) と呼ばれる記号 ∃ が新たに導入される。これらを用いると「すべての ''x'' について φ である」という命題は ∀''x''φ 、「ある ''x'' に対して φ である」は ∃''x''φ と表される。「すべての ''x'' について」といったときの ''x'' が動きうる値の範囲を'''議論領域'''あるいは'''領域''' (universe, domain) と呼ぶ。
二階述語論理（およびそれ以上の高階述語論理）では、述語および関数に対する量化を導入する。例えば、同一性 (equality) は二階述語論理においては、''x'' '''=''' ''y''
一階述語論理は、数学のほぼ全領域を形式化するのに十分な表現力を持っている。実際、現代の標準的な集合論の公理系 [[公理的集合論|ZFC]] は一階述語論理を用いて形式化されており、
<!-- == 一階述語論理の定義 ==
述語論理は以下の要素から構成される。
* 形成規則（[[整論理式]]を形成するための[[再帰的定義]]）
24行目:
述語論理の表現方法はひとつに限定されない。ここで用いる公理や推論規則は必ずしも規範的な例ではなく、同一の論理を別の形式で表現することも可能である（その場合、与えられた公理から同じ定理が導出される）。
-->
== 一階の言語 ==
一階述語論理の言語（'''一階の言語'''）は次のものからなる：
:'''論理記号''' (logical symbol)
:# '''変数'''（あるいは'''個体変数'''）と呼ばれる記号の集合： ''V'' = { ''x''<sub>1</sub> , ''x''<sub>2</sub> , ... }
:# '''結合記号'''： ¬ , ∧ , ∨ , → , ↔
:# '''量化記号'''： ∀ , ∃
:# '''括弧'''： '''(''' , ''')'''
:# '''等号'''： '''=''' （含まなくてもよい。）
:'''非論理記号''' (nonlogical symbol)
:# '''述語記号'''と呼ばれる記号の集合（空集合でも無限集合でもよい）。各述語記号には'''アリティ'''と呼ばれる正の整数が一つ対応しているものとする<ref>「[[引数|アリティ]]」という用語は通常、[[二項関係|関係]]や[[写像|関数]]がとる変数の個数を表す言葉として用いられるが、ここでの意味はそれとは異なることに注意しなければならない。述語記号や関数記号は単なる'''記号'''であって関係や関数ではなく、アリティというのはそれらの記号が持っているある正の整数という意味にすぎない。</ref>。
:# '''関数記号'''と呼ばれる記号の集合（空集合でも無限集合でもよい）。各述語記号にもアリティが備わっているとする。
:# '''定数記号'''と呼ばれる記号の集合（空集合でも無限集合でもよい）。
等号はアリティ 2 の特別な述語記号として扱われる。一階の言語は、それが等号を持つかどうか、非論理記号に何を持っているかを決めることによって定まる。例えば集合論においては、等号を持ち、非論理記号としてはアリティ 2 の述語記号 ∈ だけをもつ一階の言語（'''集合論の言語'''）が使われる。以下に一階の言語について、いくつかの注意を述べる。
== 語彙 ==▼
* 等号 '''=''' はアリティ 2 の特別な述語記号として扱われる。どの一階の言語にも等号を含めて少なくとも一つは述語記号が含まれていなけらばならないものとする。
* アリティ ''n'' の述語（関数）記号を、''n'' 変数述語（関数）記号と呼ぶこともある。
* いくつかの結合記号や量化記号は言語にもともと含まれている記号ではなく、省略記法として定義によって導入される場合がある。例えば、↔ は言語に含まれず、 (φ ↔ ψ) は (φ → ψ) ∧ (ψ → φ) を表すものとして定義される場合もある。上の論理記号すべてを用いて表現される命題は、例えば ¬、∧、∀ だけを用いても十分に表現できることが知られている。
* 文献によっては、→ の代わりに ⊃ を用い、∀ の代わりに Π を用いている場合がある。
* 定数記号はアリティ 0 の関数記号と呼ばれることもある。
* 上の定義では
* 括弧の使い方の流儀は様々である。ある人は ∀''x'' を '''('''∀''x''''')''' と書く。括弧の代わりにコロンや終止符を使う場合もある。もちろんその場合には、言語にコロンや終止符を含めておく必要がある。非常に珍しい表記法として括弧を全く使わずに[[ポーランド記法]]を使用する場合がある。これは、∧ や ∨ を先頭に書いて
== 項と論理式 ==
一階述語論理の'''項''' (term) は次のように帰納的に定義される：
# 変数と定数記号はすべて項である。
# ''t''<sub>1</sub> , ..., ''t''<sub>''n''</sub> が項で
▲* 同一性関係を一階述語論理の一部とみなす場合もある。その場合、等号も含まれることになる。これを「'''等号付き一階述語論理'''」と呼ぶ。
# 上記の 1. と 2. によって項とされるものだけが項である。
項というのは直観的には議論領域に属するある対象をあらわす"名詞"の役割をもった記号列である。
▲* 上の定義では、述語は少なくとも1以上のアリティを持つとされている。アリティ0の述語も考えることができ、それらは「真」や「偽」を意味するものと考えることができる。しかし「真」は ∀''x''(''x'' = ''x'') などと別の方法で表せるので、アリティ0の述語を導入することに大きな意味はない。
▲* 括弧の使い方の流儀は様々である。ある人は ∀''x'' を (∀''x'') と書く。括弧の代わりにコロンや終止符を使う場合もある。非常に珍しい表記法として括弧を全く使わずに[[ポーランド記法]]を使用する場合がある。これは、∧ や ∨ を先頭に書いて引数を後に続ける書き方である。ポーランド記法はコンパクトで美しいのだが、可読性が低いためにほとんど使われない。
例： '''群論の言語'''は等号を持つ一階の言語で、非論理記号として 2 変数関数記号 '''·''' と定数記号 '''0''' を持つ。定義より、
: ''x''<sub>1</sub> , ''x''<sub>5</sub> , '''0''' , '''·''' ''x''<sub>1</sub>'''0'''
はすべて項である。通常、'''·''' , x + (y + −z) と書かれる。
== 形成規則 ==▼
整論理式 (well-formed formula, wff) あるいは'''
▲# ''t''<sub>1</sub> , ..., ''t''<sub>''n''</sub> が項であるとき、[[アリティ]] ''n'' ≥ 1 の関数 ''f'' を用いて作られる式 ''f''(''t''<sub>1</sub>, ..., ''t''<sub>''n''</sub>) は項である。このとき、''t''<sub>1</sub>, ..., ''t''<sub>''n''</sub> それぞれの自由変項が、''f''(''t''<sub>1</sub>, ..., ''t''<sub>''n''</sub>) の自由変項となる。
# '''単純な述語と複雑な述語：''' ''a''<sub>''i''</sub> が項であり、''P'' をアリティ ''n'' ≥ 1 の述語記号とするとき、''Pa''<sub>1</sub> , ..., ''a''<sub>''n''</sub> は整論理式である。''a''<sub>''i''</sub> のいずれかが自由変項を持つなら、それが ''Pa''<sub>1</sub> , ..., ''a''<sub>''n''</sub> の自由変項となる。等号が論理の一部となっている場合、(''a''<sub>1</sub> = ''a''<sub>2</sub>) は整論理式である。これらはいずれも[[原子論理式]]と呼ばれる。
# '''帰納節 I： ''' φ が整論理式なら ¬φ も整論理式である。
66 ⟶ 73行目:
'''代入： ''' ''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'' とすることで問題を回避する。これを忘れるとひどい間違いを犯すことになる。
== 自由変数 ==
== 論理式の真偽 ==
▲* +(''x'', ''y'') = 0, ≤ +(''x'' +(''y'' −(''z''))) +(''x'', ''y'') は'''原子論理式'''であり、通常 ''x'' + ''y'' = 0, ''x'' + ''y'' − ''z'' ≤ ''x'' + ''y'' と書かれる。
▲* (∀''x'' ∃''y'' ≤ +(''x'' ''y'') ''z'' ∧ ∃''x'' +(''x'', ''y'') = 0) は'''論理式'''であり、通常 (∀''x'' ∃''y'' ''x'' + ''y'' ≤ ''z'') ∧ (∃''x'' ''x'' + ''y'' = 0) と書かれる。
== 同一性 ==
124 ⟶ 134行目:
証明可能性については様々な異なる（しかし互いに等価な）定義の方法がある。上述の定義は[[ダフィット・ヒルベルト|ヒルベルト]]流計算の典型例であり、これは異なる公理を多数用意して推論規則を少なくするスタイルをとっている。[[ゲルハルト・ゲンツェン|ゲンツェン]]流の[[シークエント計算|述語計算]]では逆に、公理を少なくして推論規則を豊富に用意している。
==
== 一階述語論理のメタ論理的定理 ==▼
以下、重要なメタ論理的定理を列挙する。
# 命題計算とは異なり、一階述語論理は（高々[[アリティ]]2の述語が一つでも含まれていると）決定不能である。つまり、任意の論理式 ''P'' について、''P'' が恒真であるか否かを決定する一般的なアルゴリズムは存在しない（[[チューリングマシンの停止問題]]を参照せよ）。この結果は[[アロンゾ・チャーチ]]と[[アラン・チューリング]]がそれぞれ独立に導き出した。
144 ⟶ 156行目:
一階述語論理のいくぶんエキゾチックな等価物には、次のものがある。順序対構成をもつ一階述語論理は、特別な関係として順序対の射影を持つ[[関係代数 (数学)|関係代数]]（これは[[アルフレト・タルスキ|タルスキ]]と Givant によって構築された）と精確に等価である。
{{Reflist}}
== 関連項目 ==
| |||