一階述語論理のソースを表示

'''一階述語論理'''（いっかいじゅつごろんり、{{Lang-en-short|first-order predicate logic}}）とは、個体の[[量化]]のみを許す[[述語論理]] (predicate logic) である。述語論理とは、[[数理論理学]]における論理の数学的モデルの一つであり、[[命題論理]]を拡張したものである。個体の量化に加えて述語や関数の量化を許す述語論理を'''[[二階述語論理]]'''（{{Lang-en-short|second-order predicate logic|links=no}}）と呼び、さらなる一般化を加えた述語論理を'''[[高階述語論理]]'''（{{Lang-en-short|higher-order predicate logic|links=no}}）という。本項では主に一階述語論理について解説する。二階述語論理や高階述語論理についての詳細はそれぞれの記事を参照。

== 概要 ==
=== 命題論理との差異 ===
命題論理では文を構成する最も基本的な命題（原子命題）は'''命題記号'''と呼ぶ一つの記号によって表していた。それに対し、一階述語論理においては、最も基本的な命題は'''原子論理式'''と呼ぶ記号列によって表す。原子論理式とは'''述語記号'''( <math>P</math> )と呼ぶ記号と、'''項'''( <math>t_1,\,\cdots,\,t_n</math> ) と呼ぶものの列、からなる <math>P(t_1,\,\cdots,\,t_n)</math> という形の記号列であり、これは個体の間の関係を表すものである。

命題論理にない一階述語論理のもう一つの特徴は'''[[量化]]''' (quantification) である。例えば、定言的命題論理の範囲において、次のような推論の妥当性を扱うことはできない：
:すべての人間は死ぬ。
:ソクラテスは人間である。
:したがってソクラテスは死ぬ。
一階述語論理では、このような「すべての…について」という表現や、また「ある…について」といった表現を扱えるように、'''[[全称記号|全称量化記号]]''' (universal quantifier) と呼ぶ記号 <math>\forall</math>; と'''[[存在記号|存在量化記号]]''' (existential quantifier) と呼ぶ記号 <math>\exists</math>; を新たに導入する。これらを用いると「すべての <math>x</math> について <math>\phi</math>; である」という命題は <math>\forall x\phi</math>; 、「ある <math>x</math> に対して <math>\phi</math>; である」は  <math>\exists x\phi</math>; と表される。これらの記号を用いると上の三つの文はそれぞれ、例えば、
:<math>\forall x[P(x)\Rightarrow Q(x)]</math>
:<math>P(a)</math>
:<math>Q(a)</math> 
のように記号化することができる。ここで、<math>P(x)</math> と <math>Q(x)</math> はそれぞれ「 <math>x</math> は人間である」「<math>x</math> は死ぬ」を表し、<math>a</math> はソクラテスを表すことを意図している。上の日本語による定言命題推論の[[妥当性]]は不決定的だが、仮言命題推論化されるならば、一階述語論理において <math>Q(a)</math>  が
:<math>\{\forall x[P(x)\Rightarrow Q(x)]\,,\,P(a)\}</math> 
の'''[[論理的帰結]]''' (logical consequence) であるという事実に反映される。一般に、論理式 <math>\phi</math>; が論理式の[[可算集合]] <math>\Sigma</math>; の論理的帰結であるとは、<math>\Sigma</math>; の論理式のすべてをみたす解釈は必ず <math>\phi</math>; もみたすこととして定義され、これは、あるいくつかの前提からある結論が論理的に導かれるという概念の数学的な定式化である。

命題論理においては、論理式の解釈は各命題記号に対する真理値 0 , 1 の割り当てが与えられた。これに対して、一階述語論理の論理式の[[解釈#現代論理学|解釈]]は'''[[数学的構造|構造]]''' (structure) と呼ばれ、これは'''[[議論領域|領域]]''' (universe, domain) と呼ぶ空でない集合と、それぞれの非論理記号（述語記号・関数記号・定数記号）の "意味" の割り当てからなる。領域とは「すべての <math>x</math> について」といったときの <math>x</math> が動きうる値の範囲である。一階述語論理の論理式は構造を一つ与えることによって真偽が決定される。

[[二階述語論理]]（およびそれ以上の[[高階述語論理]]）では、述語および関数に対する量化を導入する。

=== 一階述語論理の表現力 ===
一階述語論理は、数学のほぼ全領域を[[形式化]]するのに十分な表現力を持っている。実際、現代の標準的な集合論の公理系 [[公理的集合論|ZFC]] は一階述語論理を用いて形式化されており、数学の大部分はそのように形式化された ZFC の中で行うことができる。すなわち、数学の命題は一階述語論理の論理式によって記述することができ、そのように論理式で記述された数学の定理には ZFC の公理からの'''形式的証明''' (formal proof) が存在する。このことが一階述語論理が重要視される理由の一つである。この他に[[ペアノの公理|ペアノ算術]]のように単独で形式化する理論もある。

== 一階の言語 ==
一階述語論理の言語（'''一階の言語'''）は次のものからなる：
:'''論理記号''' (logical symbol)
:# '''変数'''（あるいは'''個体変数'''）と呼ぶ記号の集合： <math>V=\{x_1,\,x_2,\,\cdots\}</math>
:# '''結合記号'''： <math>\lnot</math>, <math>\land</math> , <math>\lor</math>, <math>\Rightarrow</math>, <math>\Leftrightarrow</math>
:# '''量化記号'''： <math>\forall</math>, <math>\exists</math>
:# '''括弧'''： <math>(</math> , <math>)</math> , <math>[</math> , <math>]</math> , <math>\{</math> , <math>\}</math>
:# '''等号'''： <math>=</math> （含まなくてもよい。）
:'''非論理記号''' (nonlogical symbol)
:# '''述語記号'''と呼ぶ記号の集合（[[有限集合]]でも[[無限集合]]でもよい）。各述語記号には'''アリティ'''（arity）と呼ぶ引数の個数に相当する正の[[整数]]が一つ対応しているものとする<ref>「[[アリティ]]」という用語は通常、[[二項関係|関係]]や[[写像|関数]]がとる変数の個数を表す言葉として用いられるが、ここでの意味はそれとは異なることに注意しなければならない。述語記号や関数記号は単なる'''記号'''であって関係や関数ではなく、アリティというのはそれらの記号が持っているある正の整数という意味にすぎない。</ref>。
:# '''関数記号'''と呼ぶ記号の集合（有限集合でも無限集合でもよい）。各関数記号もアリティを持っているものとする。
:# '''定数記号'''と呼ぶ記号の集合（有限集合でも無限集合でもよい）。

一階の言語は、それが等号を持つかどうか、非論理記号に何を持っているかを決めることによって定まる。例えば集合論においては、等号を持ち、非論理記号としてはアリティ <math>2</math> の述語記号 <math>\in</math>; だけをもつ一階の言語（'''集合論の言語'''）が使われる。以下に一階の言語について、いくつかの注意を述べる。
* 等号 <math>=</math> はアリティ <math>2</math> の特別な述語記号として扱われる。どの一階の言語にも等号を含めて少なくとも一つは述語記号が含まれていなければならないものとする。
* アリティ <math>n</math> の述語（関数）記号を、<math>n</math> 変数述語（関数）記号と呼ぶこともある。
* 記号は一つの用途のみに用いる。すなわち、一つの一階の言語において、ある記号が述語記号であると同時に定数記号でもあるということや、論理記号であると同時に関数記号でもあるというようなことがあってはならない。
* いくつかの結合記号や量化記号は言語にもともと含まれている記号ではなく、省略記法として定義によって導入される場合がある。例えば、<math>\Leftrightarrow</math>; は言語に含まれず、 <math>(\phi\Leftrightarrow\psi)</math> は <math>[(\phi\Rightarrow\psi)\land(\psi\Rightarrow\phi)]</math> を表すものとして定義される場合もある。上の論理記号すべてを用いて表現される命題は、例えば <math>\lnot</math>、<math>\lor</math>、<math>\exists</math> や <math>\lnot</math>、<math>\Rightarrow</math>、<math>\forall</math> だけを用いても十分に表現できることが知られている。
* 文献によっては、<math>\Rightarrow</math> の代わりに <math>\supset</math>; を用い、<math>\forall</math> の代わりに <math>\Pi</math>; を用いている場合がある。
* 同一性関係を一階述語論理の一部とみなす場合もある。その場合、等号は必ず言語に含まれることになる。常に等号が含まれることを仮定した一階述語論理を'''等号付き一階述語論理'''と呼ぶ。
* 定数記号はアリティ 0 の関数記号と呼ぶこともある。
* 上の定義では述語は 1 以上のアリティを持つとされているが、アリティ 0 の述語も考えることができ、それらは「真」や「偽」を意味するものと考えることができる。しかし「真」は <math>\forall x(x=x)</math> などと別の方法で表せるので、アリティ 0 の述語を導入することに大きな意味はない。
* 括弧の使い方の流儀は様々である。ある人は <math>\forall x</math> を <math>(\forall x)</math> と書く。括弧の代わりにコロンや終止符を使う場合もある。もちろんその場合には、言語にコロンや終止符を含めておく必要がある。括弧を全く使わない表記法に[[ポーランド記法]](Polish notation)と呼ぶものがある。これは、<math>\land</math>; や <math>\lor</math>; を先頭に書いて <math>(\phi\land\psi)</math> の代わりに <math>\land\phi\psi</math> のように書く方法である。ポーランド記法はコンパクトで数学的に取り扱いやすいという利点があり、可読性が低いという欠点がある。

== 項と論理式 ==
=== 項 ===
一階述語論理の'''項''' (term) は次のように帰納的に定義される：
# 変数と定数記号はすべて項である。
# <math>t_1,\,\cdots,\,t_n</math> が項で、<math>f</math> がアリティ ''n'' の関数記号ならば、<math>ft_1,\,\cdots,\,t_n</math> は項である<ref>読みやすさを優先させて <math>ft_1,\,\cdots,\,t_n</math> の代わりに <math>f(t_1,\,\cdots,\,t_n)</math> を用いる流儀も存在する。その場合は言語にカンマ "," を含めておく必要がある。</ref>。
# 上記の 1. と 2. によって項とされるものだけが項である。
項というのは直観的には議論領域に属するある対象を表す"[[名前]]"の役割をもった記号列である。

'''例'''． '''自然数論の言語'''は等号を持つ一階の言語で、非論理記号として 、<math>1</math> 変数関数記号 <math>S</math> 、<math>2</math> 変数関数記号 <math>+</math> , <math>\cdot</math> と定数記号 <math>0</math> を持つ。定義より、
: <math>x_1</math> , 　<math>x_5</math> , 　<math>0</math> , 　<math>Sx_1</math> , 　<math>S0</math> , 　<math>SS0</math> , 　<math>+S0S0</math> , 　<math>+0 x_5</math> , 　<math>\cdot Sx_1 + 0 x_5</math>
はすべて項である。 <math>+S0S0</math> や <math>+0 x_5</math> といった[[前置記法]]は読みにくいため、これらの項を表すのに、通常使われている <math>S(0)+S(0)</math> や <math>0+x_5</math> のような表現([[中置記法]])が用いられることもある。したがって   <math>\cdot Sx_1 + 0 x_5</math> は中置記法では <math>S(x_1)\cdot(0 +x_5)</math> のように表される。

=== 論理式 ===
項が何らかの対象を表す記号列であったのに対して、論理式は何らかの命題を表すものである。論理式は原子論理式と呼ぶ最も基本的な論理式から結合記号と量化記号を繰り返し用いることによって形成される。まず、原子論理式は次のように定義される：
: ある正の整数 <math>n</math> に対するアリティ <math>n</math> の述語記号 <math>P</math> と <math>n</math> 個の項 <math>t_1,\,\cdots,\,t_n</math> を用いて <math>P(t_1,\,\cdots,\,t_n)</math> と表される記号列を'''原子論理式''' (atomic formula) と呼ぶ。
原子論理式を用いて、'''論理式''' (well-formed formula, wff) あるいは'''式''' (formula) は次のように帰納的に定義される：
# 原子論理式は論理式である。
# <math>\phi</math> と <math>\psi</math> が論理式ならば、<math>(\lnot\phi)</math> , <math>(\phi\land\psi)</math> , <math>(\phi\lor\psi)</math> , <math>(\phi\Rightarrow\psi)</math> , <math>(\phi\Leftrightarrow\psi)</math> は論理式である。
# <math>\phi</math>  が論理式で <math>x</math>  が変数ならば、<math>(\forall x\phi)</math> , <math>(\exists x\phi)</math> は論理式である。
# 上記の 1. と 2. と 3. によって論理式とされるものだけが論理式である。

'''例'''． 再び自然数論の言語を考える。定義から、
:<math>[(S0+S0)=SS0]</math> ,　 <math>[(0+x_5)=S0]</math>
はすべて原子論理式（したがって論理式）であり、
:<math>\{\lnot[(S0+S0)=SS0]\}</math> , 　<math>\{[(0+x_5)= S0] \land [(S0+S0)=SS0]\}</math> , 　<math>\{\forall x_5[(0+x_5)=S0]\}</math>, 　<math>\{\exists x_2 [(0+x_5)=S0]\}</math>

=== 自由変数 ===
自然数論の言語における論理式 <math>(S0 + S0) = SS0</math> の各記号を通常の意味で解釈すれば「<math>1 + 1 = 2</math>」となり、これは真である論理式である。<math>\lnot[(S0 + S0) = SS0]</math> は「<math>1 + 1 \neq 2</math>」となるので通常の解釈で偽なる論理式である。また、変数の動く範囲（議論領域）は[[自然数]]全体の集合だとすれば、論理式 <math>[\forall x_1(0 = Sx_1)]</math> は「すべての自然数 <math>n</math> について <math>0 =n+ 1</math>」という意味になり、これは偽である論理式であることが分かる。一方、論理式 <math>(0 +x_5) = S0</math> の意味を考えてみると、「<math>0 + x_5 = 1</math>」となるがこれは真であるか偽であるかを判断することができない。なぜなら、<math>x_5</math> という変数が何を表しているかが決まっていないからである。このようなとき、<math>x_5</math> は論理式 <math>(0 +x_5) = S0</math> における'''自由変数''' (free variable) であると言われる。正式には、各論理式 <math>\phi</math> に対して、"<math>\phi</math> における自由変数全体の集合" <math>fr(\phi)</math> を次のように再帰的に定義する：
#<math>\phi</math> が原子論理式ならば、<math>fr(\phi)</math> は記号列 &phi; に現れるすべての変数からなる集合である。
#<math>fr[(\lnot\phi)]= fr(\phi)</math> 。
#<math>fr[(\phi\land\psi)] = fr[(\phi\lor\psi)] = fr[(\phi\Rightarrow\psi)] = fr[(\phi\Leftrightarrow\psi)] = fr(\phi) \cup fr(\psi)</math> 。
#<math>fr(\forall x\phi) = fr(\exists x\phi) = fr(\phi) - \{ x \} </math>。
論理式 <math>\phi</math> が自由変数を一切持たないとき、つまり <math>fr(\phi)=\varnothing</math> のとき、<math>\phi</math> は'''閉論理式''' (closed formula) あるいは'''文''' (sentence) と呼ぶ。直観的には、文とは記号に解釈を与えて意味を考えたときに正しいか正しくないかが決まるような論理式である。<math>(S0 + S0) = SS0</math> や <math>\forall x_1 0 = Sx_1</math> は文であるが、<math>fr[(0 +x_5) = S0] = \{ x_5 \}</math> より <math>(0 +x_5) = S0</math> は文でない。

== 論理式の真偽 ==
=== 構造 ===
はじめに述べたように、一階述語論理の論理式の解釈は構造と呼ぶものによって与えられる。構造は変数が動く領域とそれぞれの非論理記号に対する "意味" の割り当てからなる。正式には、構造は次のように定義される。
: 一階の言語に対する'''構造''' (structure) とは、空でない集合 <math>D</math> と、非論理記号全体の集合を[[写像|定義域]]とする関数 <math>F</math> の組 <math>M = (D,\,F)</math> で次をみたすものをいう：
:#<math>P</math> がアリティ <math>n</math> の述語記号ならば、<math>F(P) \subseteq D^n</math> 、すなわち <math>F(P)</math> は <math>D</math> 上の <math>n</math> 項関係である。
:#<math>f</math> がアリティ <math>n</math> の関数記号ならば、<math>F(f) : D^n \to D</math> 、すなわち <math>F(f)</math> は <math>D</math> 上の <math>n</math> 項演算である。
:#<math>c</math> が定数記号ならば、<math>F(c) \in D</math> 、すなわち <math>F(c)</math> は　<math>D</math> のある要素である。
:集合 <math>D</math> を <math>M</math> の'''領域''' (universe, domain) と呼び、通常 <math>|M|</math> で表す。また、<math>F(P)</math> , <math>F(f)</math> , <math>F(c)</math> などは通常 <math>P^M</math> , <math>f^M</math> , <math>c^M</math> と表される。
<math>M</math> が一階の言語に対する構造であるとき、<math>M</math> の領域  <math>|M|</math> の要素を ''M'' の'''個体''' (individual) と呼ぶ。

=== 論理式の充足 ===
上で見たように、自由変数を持たない論理式（すなわち文）は解釈（構造）を一つ与えることで、正しいか正しくないかが定まる。構造 ''M'' を与えたとき、文 &phi; が正しい命題になっているならば、&phi; は解釈 ''M'' において'''真''' (true) であるといい、正しくない命題である場合、&phi; は ''M'' において'''偽''' (false) であるという。以下で、これらの真偽の概念をより正確に定義する。ただし、論理式の真偽の定義にはいくつかの異なる（同値な）方法があり、ここで述べる定義はその内の一つである。

:''M'' が一階の言語に対する構造であるとき、変数全体の集合 ''V'' から ''M'' の領域 |''M''| への関数を、変数に対する '''''M'' の個体の割り当て関数'''と呼ぶ。変数に対する ''M'' の個体の割り当て関数 ''s'' を一つとったとき、それぞれの項 ''t'' に対して、''t'' の'''値''' (value) ''t'' <sup>''M''</sup>(''s'') が次のように再帰的に定義される：
:#変数 ''x'' に対しては、''x'' <sup>''M''</sup>(''s'') = s(x) 。
:#定数記号 ''c'' に対しては、''c'' <sup>''M''</sup>(''s'') = ''c'' <sup>''M''</sup> 。
:#''t''<sub>1</sub> , ..., ''t''<sub>''n''</sub> が項で、''f'' がアリティ ''n'' の関数記号ならば、(''f t''<sub>1</sub> … ''t''<sub>''n''</sub>)<sup>''M''</sup>(''s'') = ''f'' <sup>''M''</sup> (''t''<sub>1</sub><sup>''M''</sup>(''s''), ..., ''t''<sub>''n''</sub><sup>''M''</sup>(''s'')) 。
直観的には、項 ''t'' の値 ''t'' <sup>''M''</sup>(''s'') とは、各変数 ''x'' が ''M''の個体 ''s''(''x'') を表すとしたとき、''t'' が表す ''M'' の個体のことである。

次に、「構造 ''M'' が個体の割り当て関数 ''s'' によって論理式 &phi; を充足する」と言うことを定義する。''M'' が ''s'' によって &phi; を充足するとは、各変数 ''x'' は ''s''(''x'') を表すとし、各非論理記号は ''M'' によって与えられた意味を表すとしたとき、&phi; が正しい命題になっているということである。
:''M'' が一階の言語に対する構造であるとき、各論理式 &phi; と ''M'' の個体の割り当て関数 ''s'' に対して、''M''(&phi;, ''s'') &isin; { 0, 1 } を次のように再帰的に定義する：
:#''M''(''t''<sub>1</sub> '''=''' ''t''<sub>2</sub> , ''s'') = 1 　&hArr;　 ''t''<sub>1</sub><sup>''M''</sup>(''s'') = ''t''<sub>2</sub><sup>''M''</sup>(''s'') 。
:#''P'' がアリティ ''n'' の非論理述語記号ならば、　''M''(''P t''<sub>1</sub> … ''t''<sub>''n''</sub> , ''s'') = 1　 &hArr;　 (''t''<sub>1</sub><sup>''M''</sup>(''s''), ..., ''t''<sub>''n''</sub><sup>''M''</sup>(''s'')) &isin; ''P'' <sup>''M''</sup> 。
:#''M''('''('''&not; &phi;''')''', ''s'') = 1 　&hArr;　 ''M''(&phi;, ''s'') = 0 。
:#''M''('''('''&phi; &and; &psi;''')''', ''s'') = 1 　&hArr;　 ''M''(&phi;, ''s'') = 1 かつ ''M''(&psi;, ''s'') = 1 。
:#''M''('''('''&phi; &or; &psi;''')''', ''s'') = 1 　&hArr;　 ''M''(&phi;, ''s'') = 1 または ''M''(&psi;, ''s'') = 1 。
:#''M''('''('''&phi; &rarr; &psi;''')''', ''s'') = 1 　&hArr;　 ''M''(&phi;, ''s'') = 0 または ''M''(&psi;, ''s'') = 1 。
:#''M''('''('''&phi; &harr; &psi;''')''', ''s'') = 1 　&hArr;　 ''M''(&phi;, ''s'') = ''M''(&psi;, ''s'') 。
:#''M''(&forall;''x'' &phi;, ''s'') = 1 　&hArr;　 すべての ''m'' &isin; |''M''| に対して ''M''(&phi;, ''s''[''x''|''m'']) = 1 。
:#''M''(&exist;''x'' &phi;, ''s'') = 1 　&hArr;　 ある ''m'' &isin; |''M''| に対して ''M''(&phi;, ''s''[''x''|''m'']) = 1 。
::ただし、''s''[''x''|''m''] は変数 ''x'' には ''m'' を割り当て、''x'' 以外の変数に対しては ''s'' と同じ個体を割り当てる関数を表す。
:''M''(&phi;, ''s'') = 1 であるとき '''''M'' は ''s'' によって &phi; を充足する'''という。
特に &phi; が文である場合は、すべての個体の割り当て関数 ''s'' に対して ''M''(&phi;, ''s'') = 1 であるか、すべての個体の割り当て関数 ''s'' に対して ''M''(&phi;, ''s'') = 0 であるかのいずれかであることが示される。そこで、前者の場合に &phi; は ''M'' において真であるといい、後者の場合に &phi; は ''M'' において偽であるという。すなわち、構造 ''M'' と文 &phi; に対して、
:&phi; は ''M'' において'''真''' (true) 　&hArr;　 任意の ''M'' の個体の割り当て関数 ''s'' に対して、''M''(&phi;, ''s'') = 1 。
:&phi; は ''M'' において'''偽''' (false) 　&hArr;　 任意の ''M'' の個体の割り当て関数 ''s'' に対して、''M''(&phi;, ''s'') = 0 。
と定義する。&phi; が ''M'' において真であるとき、''M'' は &phi; の'''モデル''' (model) であるともいう。また、''M'' が文の集合 &Sigma; のすべての要素のモデルであるとき、単に ''M'' は &Sigma; のモデルであるという。

=== 論理的帰結 ===
&Sigma; を論理式の集合とし、&phi; を論理式とする。&Sigma; に属するすべての論理式 &psi; に対して ''M''(&psi;, ''s'') = 1 であるような任意の構造 ''M'' と ''M'' の個体の割り当て関数 ''s'' が ''M''(&phi;, ''s'') = 1 をみたすとき、&phi; は &Sigma; の'''論理的帰結''' (logical consquence) であるといい、<math>\Sigma \vDash \varphi</math> と書く。論理式 &phi; と &psi; が <math>\{\varphi\} \vDash \psi</math> かつ <math>\{\psi\} \vDash \varphi</math> をみたすとき、&phi; と &psi; は'''論理的に同値''' (logically equivalent) であるという。また、&phi; が &empty; の論理的帰結である場合、すなわち任意の構造 ''M'' と ''M'' の個体の割り当て関数 ''s'' に対して ''M''(&phi;, ''s'') = 1 であるとき、&phi; は'''恒真''' (valid) であるという。&phi; と &psi; が論理的に同値であることは、'''('''&phi; &harr; &psi;''')''' が恒真であることと同値である。

== 形式的証明 ==
命題論理においては、'''論理公理''' (logical axiom) と呼ぶ論理式の集合と、ある論理式たちから新たな論理式を導出する規則（'''[[推論規則]]'''）を導入し、論理公理から推論規則の有限回の適用によって得られる論理式全体と[[トートロジー]]全体が一致するようにすることができる（[[命題論理#規則の健全性と完全性|命題論理の健全性と完全性]]）。一階述語論理においても、適切に論理公理と推論規則を導入することで、論理公理から推論規則を使って導出される論理式全体と恒真論理式全体が一致するようにできる。

形式的証明の定義の仕方はひとつではなく、様々な異なる（等価な）方法がある。ここで述べる定義は[[ダフィット・ヒルベルト|ヒルベルト]]流計算の典型例であり、これは異なる公理を多数用意して推論規則を少なくするスタイルをとっている。[[ゲルハルト・ゲンツェン|ゲンツェン]]流の形式的証明では逆に、公理を少なくして推論規則を多く用いている。ここで述べるものと異なる証明可能性の定義については「[[自然演繹]]」「[[シークエント計算]]」などを参照。

=== 論理公理 ===
以下の形の論理式すべてを論理公理とする。ここで、''x'', ''y'' は変数、''t'', ''t''<sub>1</sub> , ..., ''t''<sub>''n''</sub> は項、&phi;, &psi; は論理式を表す：
*トートロジー（命題論理におけるトートロジーの命題記号を一階の論理式で置き換えて得られる論理式）
*量化記号に関する公理
#&forall;''x'' &phi; &rarr; &phi;<sub>''x''</sub> [ ''t'' ] 　（ただし、&phi; において ''t'' が ''x'' に代入可能（後述）の場合に限る）
#&forall;''x'' '''('''&phi; &rarr; &psi;''')''' &rarr; '''('''&forall;''x'' &phi; &rarr; &forall;''x'' &psi;''')'''
#&forall;''x'' '''('''&not; &phi;''')''' &harr; '''('''&not; &exist;''x'' &phi;''')'''
*等号に関する公理（言語が等号を持つ場合に限る）
#''x'' '''=''' ''x''
#''x'' '''=''' ''y'' &rarr; '''('''''P t''<sub>1</sub> … ''t''<sub>''n''</sub> &rarr; ''P u''<sub>1</sub> … ''u''<sub>''n''</sub>''')''' 　（ただし、''P'' は ''n'' 変数述語記号で、''u''<sub>''i''</sub> は ''t''<sub>''i''</sub> における ''x'' のいくつかを ''y'' で置き換えて得られる項である）
量化記号に関する公理 1. における &phi;<sub>''x''</sub> [ ''t'' ] とは、論理式 &phi; において "束縛されていない" 変数 ''x'' をすべて項 ''t'' で置き換えて得られる論理式を表す（正確な定義は後述）。

=== 推論規則 ===
推論規則とは、あるいくつかの論理式から別の論理式を導出するための規則である。これは正確には、論理式全体の集合の上の関係として定義される。推論規則には様々なものが考えられるが、ここで用いる推論規則は'''[[モーダスポネンス|モーダス・ポーネンス]]''' (modus ponens) と呼ぶ規則と'''[[普遍例化|全称化]]''' (generalization) と呼ぶ規則の二つである。

==== モーダス・ポーネンス (MP) ====
モーダス・ポーネンスとは、&phi; と '''('''&phi; &rarr; &psi;''')''' から &psi; を導出してよいという規則である。これは、論理式全体の集合の上の関係としては次のように定義することができる：
:MP = { (&phi;, '''('''&phi; &rarr; &psi;''')''', &psi;) | &phi; と &psi; は論理式 } 。
(&phi;<sub>1</sub>, &phi;<sub>2</sub>, &phi;<sub>3</sub>) &isin; MP であるとき、&phi;<sub>3</sub> は &phi;<sub>1</sub>, &phi;<sub>2</sub> からのモーダス・ポーネンスによる導出であるという。

==== 全称化 (GEN) ====
全称化規則とは、''x'' が変数のとき、&phi; から &forall;''x'' &phi; を導出してよいという規則である。これは、論理式全体の集合の上の関係としては次のように定義することができる：
:GEN = { (&phi;, &forall;''x'' &phi;)  | &phi; は論理式かつ ''x'' は変数 } 。
(&phi;<sub>1</sub>, &phi;<sub>2</sub>) &isin; GEN であるとき、&phi;<sub>2</sub> は &phi;<sub>1</sub> からの全称化による導出であるという。

=== 証明可能性 ===
論理式 &phi; が論理式の集合 &Sigma; から証明可能であるとは、&Sigma; に属する論理式と論理公理から推論規則の有限回の適用によって &phi; が得られることを意味する。そして、&Sigma; に属する論理式と論理公理から &phi; を導出する仮定を示した論理式の有限列を、&Sigma; からの &phi; の形式的証明とよぶ。これらの概念は次のように厳密に定義することができる。
:&phi; を論理式、&Sigma; を論理式の集合とする。&Sigma; からの &phi; の'''形式的証明''' (formal proof) あるいは'''証明''' (proof) とは、論理式の有限列 (&phi;<sub>0</sub>, ..., &phi;<sub>''n''</sub>) で次をみたすものをいう：
:#&phi;<sub>''n''</sub> = &phi; 。
:#''n'' 以下の任意の自然数 ''k'' に対して、次のいずれかが成り立つ：
:::(a) &phi;<sub>''k''</sub> &isin; &Sigma; 。
:::(b) &phi;<sub>''k''</sub> は論理公理である。
:::(c) ある ''i'', ''j'' &lt; ''k'' が存在して、&phi;<sub>''k''</sub> は &phi;<sub>''i''</sub> , &phi;<sub>''j''</sub> からのモーダス・ポーネンスによる導出である。
:::(d) ある ''i'' &lt; ''k'' が存在して、&phi;<sub>''k''</sub> は &phi;<sub>''i''</sub> からの全称化による導出である。
:&Sigma; からの &phi; の証明が存在するとき、&phi; は &Sigma; から'''証明可能''' (provable) である、あるいは &phi; は &Sigma; の'''定理''' (theorem) であるといい、<math>\Sigma\vdash\varphi</math> と書く。

=== 代入について ===
&phi;<sub>''x''</sub> [ ''t'' ] は、論理式 &phi; において "束縛されていない" 変数 ''x'' をすべて項 ''t'' で置き換えて得られる論理式を表すと述べた。正確には、&phi;<sub>''x''</sub> [ ''t'' ] は再帰によって次に述べるような仕方で定義される。
:まず、それぞれの項 ''u'' に対して ''u''<sub>''x''</sub> [ ''t'' ] を次のように再帰的に定義する：
:#''x''<sub>''x''</sub> [ ''t'' ] = ''t'' 。
:#''y'' が ''x'' と異なる変数ならば、''y''<sub>''x''</sub> [ ''t'' ] = ''y'' 。
:#''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'' ] 。
:そして、&phi;<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'' ] 。
:#'''('''&not; &phi;''')'''<sub>''x''</sub> [ ''t'' ] = '''('''&not; &phi;<sub>''x''</sub> [ ''t'' ]''')'''
:#'''('''&phi; &and; &psi;''')'''<sub>''x''</sub> [ ''t'' ] = '''('''&phi;<sub>''x''</sub> [ ''t'' ] &and; &psi;<sub>''x''</sub> [ ''t'' ]''')'''
:#'''('''&phi; &or; &psi;''')'''<sub>''x''</sub> [ ''t'' ] = '''('''&phi;<sub>''x''</sub> [ ''t'' ] &or; &psi;<sub>''x''</sub> [ ''t'' ]''')'''
:#'''('''&phi; &rarr; &psi;''')'''<sub>''x''</sub> [ ''t'' ] = '''('''&phi;<sub>''x''</sub> [ ''t'' ] &rarr; &psi;<sub>''x''</sub> [ ''t'' ]''')'''
:#'''('''&phi; &harr; &psi;''')'''<sub>''x''</sub> [ ''t'' ] = '''('''&phi;<sub>''x''</sub> [ ''t'' ] &harr; &psi;<sub>''x''</sub> [ ''t'' ]''')'''
:#(&forall;''x'' &phi;)<sub>''x''</sub> [ ''t'' ] = &forall;''x'' &phi; 、(&exist;''x'' &phi;)<sub>''x''</sub> [ ''t'' ] = &exist;''x'' &phi; 。
:#''y'' が ''x'' と異なる変数ならば、(&forall;''y'' &phi;)<sub>''x''</sub> [ ''t'' ] = &forall;''y'' &phi;<sub>''x''</sub> [ ''t'' ] 、(&exist;''y'' &phi;)<sub>''x''</sub> [ ''t'' ] = &exist;''y'' &phi;<sub>''x''</sub> [ ''t'' ] 。

次に、論理式 &phi; において項 ''t'' が変数 ''x'' に代入可能であるということを定義する。このことの直観的な意味は、&phi; が ''x'' について述べていることと同じことを &phi;<sub>''x''</sub> [ ''t'' ] が ''t'' について述べているということである。代入可能性の正式な定義は次の通りである。
:論理式 &phi; において項 ''t'' が変数 ''x'' に'''代入可能''' (substitutable) であるということを次のように再帰的に定義する：
:#原子論理式においては、常に ''t'' は ''x'' に代入可能である。  
:#'''('''&not; &phi;''')''' において ''t'' が ''x'' に代入可能 　&hArr;　 &phi; において ''t'' が ''x'' に代入可能 。
:#'''('''&phi; &and; &psi;''')''' において ''t'' が ''x'' に代入可能 　&hArr;　 &phi; と &psi; において ''t'' が ''x'' に代入可能 。
:#'''('''&phi; &or; &psi;''')''' において ''t'' が ''x'' に代入可能 　&hArr;　 &phi; と &psi; において ''t'' が ''x'' に代入可能 。
:#'''('''&phi; &rarr; &psi;''')''' において ''t'' が ''x'' に代入可能 　&hArr;　 &phi; と &psi; において ''t'' が ''x'' に代入可能 。
:#'''('''&phi; &harr; &psi;''')''' において ''t'' が ''x'' に代入可能 　&hArr;　 &phi; と &psi; において ''t'' が ''x'' に代入可能 。
:#&forall;''y'' &phi; において ''t'' が ''x'' に代入可能 　&hArr;　 ''x'' &notin; fr(&phi;) または（&phi; において ''t'' が ''x'' に代入可能かつ ''t'' の中に ''y'' が現れない）。
:#&exist;''y'' &phi; において ''t'' が ''x'' に代入可能 　&hArr;　 ''x'' &notin; fr(&phi;) または（&phi; において ''t'' が ''x'' に代入可能かつ ''t'' の中に ''y'' が現れない）。

=== 等号に関する公理について ===
等号に関する公理の 2. は、
:''x'' '''=''' ''y'' &rarr; '''('''''P t''<sub>1</sub> … ''t''<sub>''n''</sub> &rarr; ''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'' 　&hArr;　 ''u'' = ''x'' または ''u'' = ''y'' 。
:#''z'' が ''x'' と異なる変数ならば、''z'' ≈ ''u'' 　&hArr;　 ''u'' = ''z'' 。
:#''c'' 定数記号ならば、''c'' ≈ ''u'' 　&hArr;　 ''u'' = ''c'' 。
:#''t''<sub>1</sub> , ..., ''t''<sub>''n''</sub> が項で、''f'' がアリティ ''n'' の関数記号ならば、''f t''<sub>1</sub> … ''t''<sub>''n''</sub> ≈ ''u'' 　&hArr;　 ''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''</sub> 。
:''t'' ≈ ''u'' であるとき、''u'' は ''t'' における ''x'' のいくつかを ''y'' で置き換えて得られる項であるという。

== 健全性と完全性 ==
文 &phi; が文の集合 &Sigma; の論理的帰結であること ( <math>\Sigma \vDash \varphi</math> ) と、&phi; が &Sigma; の定理であること ( <math>\Sigma\vdash\varphi</math> ) は全く別の仕方で定義されている。

健全性とは、&Sigma; の定理はすべて &Sigma; の論理的帰結であることである。
:<math>\Sigma\vdash\varphi \Longrightarrow \Sigma \vDash \varphi</math>
完全性とは、&Sigma; の論理的帰結はすべて &Sigma; の定理であることである。
:<math>\Sigma\vDash\varphi \Longrightarrow \Sigma \vdash \varphi</math>
古典一階述語論理は健全かつ[[ゲーデルの完全性定理|完全]]である。

== 一階述語論理に関する定理 ==
以下、健全性定理と完全性定理以外の重要な定理を列挙する。
# コンパクト性定理 ： 文の集合 &Sigma; のすべての有限[[部分集合]]がモデルを持つならば、&Sigma; 自身もモデルを持つ。
# レーヴェンハイム・スコーレムの定理 ： &kappa; を[[濃度 (数学)|無限基数]]とする。論理式全体の集合の[[濃度 (数学)|濃度]]が &kappa; であるような一階の言語における文の集合がモデルを持つなら、それは濃度 &kappa; 以下のモデルも持つ。
# 恒真論理式全体の集合は（言語にアリティ 2 以上の述語が一つでも含まれていると）[[決定可能]]でない。つまり、任意に論理式が与えられたとき、それが恒真であるか否かを判定する[[アルゴリズム]]は存在しない（「[[チューリングマシンの停止問題]]」を参照）。この結果は[[アロンゾ・チャーチ]]と[[アラン・チューリング]]がそれぞれ独立に導き出した。正確には、恒真論理式の[[ゲーデル数]]全体の集合は[[帰納的関数|帰納的]]でないということである。
# それでも、与えられた論理式が恒真であるとき、かつそのときにのみ 1 (yes) を出力して停止するアルゴリズムは存在する。ただし、恒真でない論理式を入力した場合はこのアルゴリズムは停止しないかもしれない。これを、恒真論理式全体の集合は'''準決定可能'''であるという。これは正確に述べれば、恒真論理式のゲーデル数全体の集合が[[帰納的可算]]であるということである。
# 1 変数述語記号だけを非論理記号に持つ言語の恒真論理式全体の集合は決定可能である。

== 他の論理との比較 ==
*'''型つき一階述語論理'''は変項や項に'''型'''または'''種'''を導入したものである。型の個数が有限個であれば普通の一階述語論理と大きな違いはなく、有限個の単項述語で型を記述し、いくつかの公理を追加すればよい。真理値として &Omega; という特殊な型を持つ場合があるが、その場合の論理式は &Omega; 型の項となる。
* '''弱二階述語論理'''は有限個の部分集合の量化を許すものである。
* '''単項二階述語論理'''は部分集合、すなわち単項述語の量化のみを許すものである。
* '''二階述語論理'''は部分集合および関係、すなわち全ての述語の量化を許すものである。
* '''高階述語論理'''は述語を引数とする述語など、さらに一般化したものの量化を許す。
* '''直観主義的一階述語論理'''は古典命題計算ではなく[[直観主義 (数学の哲学)|直観主義]]を導入するものである。例えば、&not;&not;&phi; は必ずしも &phi; と等しいとは限らない。
* '''[[様相論理学|様相論理]]'''は様相演算子を追加したものである。これは、直観的に説明すれば、「～は必然的である」および「～は可能である」を意味する演算子である。
* '''[[無限論理]]'''は無限に長い文を許す。例えば無限個の論理式の連言や選言が許されたり、無限個の変項を量化できたりする。
* '''新たな量化子を加えた一階述語論理'''は、例えば「……であるような多くの ''x'' が存在する」といった意味の新たな量化子 ''Qx'', ..., を持つ。

こうした論理の多くは、一階述語論理の何らかの拡張と言える。これらは、一階述語論理の論理演算子と量化子を全て含んでいて、それらの意味も同じである。リンドストレムは、一階述語論理の拡張には、レーヴェンハイム・スコーレムの下降定理とコンパクト性定理の両方を満足するものが存在しないことを示した。この定理の内容を精確に述べるには、論理が満たしていなければならない条件を数ページにわたって列挙する必要がある。例えば、言語の記号を変更しても各文の真偽が基本的に変わらないようになっていなければならない。

一階述語論理のいくぶんエキゾチックな等価物には、次のものがある。順序対構成をもつ一階述語論理は、特別な関係として順序対の射影を持つ[[関係代数 (数学)|関係代数]]（これは[[アルフレト・タルスキ|タルスキ]]と Givant によって構築された）と精確に等価である。

== 脚注 ==
{{脚注ヘルプ}}{{Reflist}}

== 関連項目 ==
{{Div col}}
* [[数理論理学]]
* [[ロビンソン算術]]
* [[コンパクト性定理]]
* [[ゲーデルの完全性定理]]
* [[ゲーデルの不完全性定理]]
* [[エルブラン化]]
* [[論理記号の一覧]]
* [[冠頭標準形]]
* [[分析論前書]]
* [[Prolog]]
* [[関係代数 (関係モデル)]]
* [[関係モデル]]
* [[スコーレム標準形]]
* [[真理値表]]
{{Div col end}}

== 参考文献 ==
* {{cite book | 和書 | author=D.ヒルベルト、W.アッケルマン | editor=[[伊藤誠]]{{要曖昧さ回避|date=2023年5月}}（訳） | title=記号論理学の基礎（第３版 ） | year=1954 | publisher=大阪教育図書社 | ref=HA(1954) }}
<!--
*[[List of rules of inference]]
*[[List of first-order theories]]
-->

{{logic}}
{{Mathematical logic}}

{{DEFAULTSORT:いつかいしゆつころんり}}
{{Normdaten}}
[[Category:述語論理]]
[[Category:数理論理学]]
[[Category:計算理論]]
[[Category:数学に関する記事]]