「一階述語論理」の版間の差分
削除された内容 追加された内容
編集の要約なし |
編集の要約なし |
||
13行目:
のように記号化することができる。ここで、''Px'' と ''Qx'' はそれぞれ「''x'' は人間である」「''x'' は死ぬ」を表し、''a'' はソクラテスを表すことを意図している。上の日本語における推論の妥当性は、一階述語論理において ''Qa'' が { ∀x '''('''''Px'' → ''Qx''''')''' , ''Pa'' } の'''論理的帰結''' (logical consquence) であるという事実に反映されている。一般に、論理式 φ が論理式の集合 Σ の論理的帰結であるとは、Σ の論理式のすべてをみたす解釈は必ず φ もみたすこととして定義され、これは、あるいくつかの前提からある結論が論理的に導かれるという概念の数学的な定式化である。
命題論理においては、論理式の解釈は各命題記号に対する真理値 0 , 1 の割り当て与えられた。これに対して、一階述語論理の論理式の解釈は'''構造''' (structure) と呼ばれ、これは'''領域''' (universe, domain) と呼ばれる空でない集合と、それぞれの非論理記号（述語記号・関数記号・定数記号）の "意味" の割り当てからなる。領域とは「すべての ''x'' について」といったときの ''x'' が動きうる値の範囲である。一階述語論理の論理式は構造を一つ与えることによって真偽が決定される。
二階述語論理（およびそれ以上の高階述語論理）では、述語および関数に対する量化を導入する。
一階述語論理は、数学のほぼ全領域を形式化するのに十分な表現力を持っている。実際、現代の標準的な集合論の公理系 [[公理的集合論|ZFC]] は一階述語論理を用いて形式化されており、数学の大部分はそのように形式化された ZFC の中で行うことができる。すなわち、数学の命題は一階述語論理の論理式によって記述することができ、そのように論理式で記述された数学の定理には ZFC の公理からの'''形式的証明''' (formal proof) が存在する。このことが一階述語論理が重要視される理由の一つである。この他に[[ペアノの公理|ペアノ算術]]のように単独で形式化される理論もある
== 一階の言語 ==
36行目:
* アリティ ''n'' の述語（関数）記号を、''n'' 変数述語（関数）記号と呼ぶこともある。
* 記号は一つの用途のみに用いる。すなわち、一つの一階の言語において、ある記号が述語記号であると同時に定数記号でもあるということや、論理記号であると同時に関数記号でもあるというようなことがあってはならない。
* いくつかの結合記号や量化記号は言語にもともと含まれている記号ではなく、省略記法として定義によって導入される場合がある。例えば、↔ は言語に含まれず、 '''('''φ ↔ ψ''')''' は '''(('''φ → ψ''')''' ∧ '''('''ψ → φ'''))''' を表すものとして定義される場合もある。上の論理記号すべてを用いて表現される命題は、例えば ¬、&
* 文献によっては、→ の代わりに ⊃ を用い、∀ の代わりに Π を用いている場合がある。
* 同一性関係を一階述語論理の一部とみなす場合もある。その場合、等号は必ず言語に含まれることになる。常に等号が含まれることを仮定した一階述語論理を'''等号付き一階述語論理'''と呼ぶ。
79行目:
== 論理式の真偽 ==
===
はじめに述べたように、一階述語論理の論理式の解釈は構造と呼ばれるものによって与えられる。構造は変数が動く領域とそれぞれの非論理記号に対する "意味" の割り当てからなる。正式には、構造は次のように定義される。
: 一階の言語に対する'''構造''' (structure) とは、空でない集合 ''D'' と、非論理記号全体の集合を[[写像|定義域]]とする関数 ''F'' の組 ''M'' = (''D'', ''F'') で次をみたすものをいう：
116行目:
=== 論理的帰結 ===
Σ を論理式の集合とし、φ を論理式とする。Σ に属するすべての論理式 ψ に対して ''M''(ψ, ''s'') = 1 であるような任意の
== 形式的証明 ==
命題論理においては、'''論理公理''' (logical axiom) とよばれる論理式の集合と、ある論理式たちから新たな論理式を導出する規則（'''推論規則'''）を導入し、論理公理から推論規則の有限回の適用によって得られる論理式全体と[[トートロジー]]全体が一致するようにすることができる（[[命題論理#規則の健全性と完全性|命題論理の健全性と完全性]]）。一階述語論理においても、適切に論理公理と推論規則を導入することで、論理公理から推論規則を使って導出される論理式全体と恒真論理式全体が一致するようにできる。
形式的証明の定義の仕方はひとつ
=== 論理公理 ===
127行目:
*トートロジー（命題論理におけるトートロジーの命題記号を一階の論理式で置き換えて得られる論理式）
*量化記号に関する公理
#∀''x'' φ → φ<sub>''x''</sub> [ ''t'' ] （ただし、
#∀''x'' '''('''φ → ψ''')''' → '''('''∀''x'' φ → ∀''x'' ψ''')'''
#∀''x'' '''('''¬ φ''')''' ↔ '''('''¬ ∃''x'' φ''')'''
133行目:
#''x'' '''=''' ''x''
#''x'' '''=''' ''y'' → '''('''''P t''<sub>1</sub> … ''t''<sub>''n''</sub> → ''P u''<sub>1</sub> … ''u''<sub>''n''</sub>''')''' （ただし、''P'' は ''n'' 変数述語記号で、''u''<sub>''i''</sub> は ''t''<sub>''i''</sub> における ''x'' のいくつかを ''y'' で置き換えて得られる項である）
量化記号に関する公理 1. における φ<sub>''x''</sub> [ ''t'' ] とは、論理式 φ において "束縛されていない" 変数 ''x'' をすべて項 ''t'' で置き換えて得られる論理式を表す（正確な定義は後述）。
=== 推論規則 ===
175行目:
:#(∀''x'' φ)<sub>''x''</sub> [ ''t'' ] = ∀''x'' φ 、(∃''x'' φ)''x''</sub> [ ''t'' ] = ∃''x'' φ 。
:#''y'' が ''x'' と異なる変数ならば、(∀''y'' φ)<sub>''x''</sub> [ ''t'' ] = ∀''y'' φ<sub>''x''</sub> [ ''t'' ] 、(∃''y'' φ)<sub>''y''</sub> [ ''t'' ] = ∃''x'' φ<sub>''x''</sub> [ ''t'' ] 。
次に、論理式 φ において項 ''t'' が変数 ''x'' に代入可能であるということを定義する。このことの直観的な意味は、φ が ''x'' について述べていることと同じことを φ<sub>''x''</sub> [ ''t'' ] が ''t'' について述べているということである。例えば、。これに対して、。
代入可能性の正式な定義は次の通りである。
:論理式 φ において項 ''t'' が変数 ''x'' に代入可能であるということを次のように再帰的に定義する：
:#
:#
:#
:#
:#
:#
:#
=== 等号に関する公理について ===
等号に関する公理の 2. は、
:''x'' '''=''' ''y'' → '''('''''P t''<sub>1</sub> … ''t''<sub>''n''</sub> → ''P u''<sub>1</sub> … ''u''<sub>''n''</sub>''')''' （ただし、''P'' は ''n'' 変数述語記号で、''u''<sub>''i''</sub> は ''t''<sub>''i''</sub> における ''x'' のいくつかを ''y'' で置き換えて得られる項である）
となっている。ここで、項 ''u'' が項 ''t'' における ''x'' のいくつかを ''y'' で置き換えて得られる項であるということを
:変数 ''x'' と ''y'' を固定し、項の間の関係 ≈ を次のように再帰的に定義する：
:#''x'' ≈ ''u'' ⇔ ''u'' = ''x'' または ''u'' = ''y'' 。
:#''z'' が ''x'' と異なる変数ならば、''z'' ≈ ''u'' ⇔ ''u'' = ''z'' 。
:#''c'' 定数記号ならば、''c'' ≈ ''u'' ⇔ ''u'' = ''c'' 。
:#''t''<sub>1</sub> , ..., ''t''<sub>''n''</sub> が項で、''f'' がアリティ ''n'' の関数記号ならば、''f t''<sub>1</sub> … ''t''<sub>''n'' ≈ ''u'' ⇔ ''t''<sub>1</sub> ≈ ''u''<sub>1</sub> , ..., ''t''<sub>''n''</sub> ≈ ''u''<sub>''n''</sub> であるような ''u''<sub>1</sub> , ..., ''u''<sub>''n''</sub> が存在して ''u'' = ''f u''<sub>1</sub> … ''u''<sub>''n'' 。
''t'' ≈ ''u'' であるとき、''u'' は ''t'' における ''x'' のいくつかを ''y'' で置き換えて得られる項であるという。
== 健全性と完全性 ==
188 ⟶ 205行目:
== 一階述語論理に関する定理 ==
以下、健全性定理と完全性定理以外の重要な定理を列挙する。
# コンパクト性定理 ： 論理式の集合 Σ のすべての有限[[部分集合]]が
# レーヴェンハイム・スコーレムの定理 ： κ が[[濃度 (数学)|無限基数]]のとき、非論理記号全体の集合の[[濃度 (数学)|濃度]]が κ であるような一階の言語における文の集合がモデルを持つなら、それは濃度 κ 以下のモデルも持つ。
# 恒真論理式全体の集合は（言語にアリティ 2 以上の述語が一つでも含まれていると）[[決定可能]]でない。つまり、任意に論理式が与えられたとき、それが恒真であるか否かを判定する[[アルゴリズム]]は存在しない（「[[チューリングマシンの停止問題]]」を参照）。この結果は[[アロンゾ・チャーチ]]と[[アラン・チューリング]]がそれぞれ独立に導き出した。正確には、恒真論理式の[[ゲーデル数]]全体の集合は[[帰納的関数|帰納的]]でないということである。
| |||