一階述語論理

一階述語論理は、述語論理、述語計算、量化論理とも呼ばれ、数学、哲学、言語学、コンピュータサイエンスで用いられる形式体系の一種である。一階述語論理では、非論理的対象に対して量化変数を用い、変数を含む文を用いることができる。「すべての人間は死ぬ」といった命題の代わりに、一階述語論理では「すべてのxに対して、xが人間であれば、xは死ぬ」という形式の表現を用いる。ここで「すべてのxに対して」は量化子、xは変数、「…は人間である」および「…は死ぬ」は述語である。^{[1]この点が、量化子や}関係式を用いない命題論理との違いである。^[2]^{: 161}この意味で、一階述語論理は命題論理の拡張である。

集合論、群論^{[3] 、または}算術の形式理論など、あるトピックに関する理論は、通常、特定の議論領域（量化変数の範囲）、その領域からそれ自身への有限個の関数、その領域で定義された有限個の述語、そしてそれらについて成り立つと信じられている公理の集合を伴う一階論理です。「理論」は、より正式な意味で、一階論理における単なる文の集合として理解されることがあります。

「一階」という用語は、一階論理を、述語または関数を引数として持つ述語がある、または述語、関数、またはその両方に対する量化が許容される高階論理と区別します。 ^[4]^：56一階理論では、述語はしばしば集合に関連付けられます。解釈された高階理論では、述語は集合の集合として解釈される場合があります

一階論理には、健全（つまり、証明可能なすべてのステートメントはすべてのモデルで真である）かつ完全（つまり、すべてのモデルで真であるすべてのステートメントは証明可能である）である演繹体系が数多くあります。論理的帰結関係は半決定可能（semi-decidable）に過ぎませんが、一階論理における自動定理証明は大きく進歩しました。一階論理はまた、レーヴェンハイム・スコーレム定理やコンパクト性定理など、証明理論における解析に適したいくつかのメタ論理定理を満たしています

一階論理は数学を公理として形式化するための標準であり、数学の基礎で研究されています。ペアノ算術とツェルメロ＝フランケル集合論は、それぞれ数論と集合論を一階論理に公理化したものです。しかし、一階論理には、自然数や実数直線のような無限領域を持つ構造を一意に記述できる強さはありません。これらの2つの構造を完全に記述する公理系、すなわち圏論的公理系は、二階論理などのより強い論理によって得られます。

第一階述語論理の基礎は、ゴットロブ・フレーゲとチャールズ・サンダース・パースによって独立して発展しました。^[5]第一階述語論理の歴史とそれがどのようにして形式論理を支配するようになったかについては、ホセ・フェレイロス（2001）を参照してください。

はじめに

命題論理は単純な宣言的命題を扱いますが、一階述語論理はさらに述語と量化を扱います。述語は、談話領域内の実体（複数可）に対して真または偽として評価されます

「ソクラテスは哲学者である」と「プラトンは哲学者である」という2つの文を考えてみましょう。命題論理では、これらの文自体が研究対象の個体と見なされ、例えばpやqなどの変数で表されることがあります。これらは、談話領域内の特定のオブジェクトへの述語（など）の適用とは見なされず、真か偽かのいずれかである発話としてのみ見なされます。^[6]しかし、一階述語論理では、これらの2つの文は、特定の個体または非論理的なオブジェクトが特性を持つという文として構成される場合があります。この例では、両方の文はたまたまある個体について共通の形式を持っており、最初の文では変数xの値は「ソクラテス」、2番目の文では「プラトン」です。元の論理接続詞に加えて非論理的な個体について語ることができるため、一階述語論理には命題論理が含まれます。^[7]^{: 29–30} ${\text{isPhil}}$ ${\text{isPhil}}(x)$ $x$

「 xは哲学者である」のような式の真偽は、 xによって表される対象と、述語「は哲学者である」の解釈に依存します。したがって、「xは哲学者である」だけでは、真か偽かという明確な真理値を持たず、文の断片に似ています。^{[8]述語間の関係は、}論理接続詞を用いて述べることができます。例えば、「 xが哲学者であるならば、xは学者である」という一階述語は、「xは哲学者である」を仮定とし、「xは学者である」を結論とする条件文であり、これも明確な真理値を持つためには xを特定する必要があります

量指定子は式内の変数に適用できます。例えば、前の式の変数xは、「すべてのxについて、xが哲学者であれば、xは学者である」という一階述語文で全称量化できます。この文の全称量指定子「すべての」は、「 xが哲学者であれば、xは学者である」という主張が、 xのすべての選択に対して成り立つという考えを表しています

「すべてのxについて、xが哲学者ならば、xは学者である」という文の否定は、「 xが哲学者であり、x が学者ではないようなxが存在する」という文と論理的に同値です。存在量化子「存在する」は、「 xは哲学者であり、xは学者ではない」という主張が、あるxの選択に対して成り立つという考えを表現しています。

述語「は哲学者である」と「は学者である」はそれぞれ1つの変数を取ります。一般に、述語は複数の変数を取ることができます。「ソクラテスはプラトンの教師である」という一階述語では、「は教師である」という述語は2つの変数を取ります

一階述語論理式の解釈（またはモデル）は、各述語の意味と、変数を具体化できる実体を指定します。これらの実体は談話領域または宇宙を形成し、通常は空でない集合である必要があります。例えば、「xが存在し、 xは哲学者である」という文を考えてみましょう。この文は、談話領域がすべての人間で構成され、述語「哲学者である」が「『国家』の著者であった」と理解されるような解釈では真であるとみなされます。これは、プラトンのテキストで証明されているように真です。^{[説明が必要]}

一階述語論理には2つの重要な部分があります。統語論は、一階述語論理においてどの有限の記号列が整形式の表現であるかを決定し、意味論はこれらの表現の背後にある意味を決定します。

統語論

英語などの自然言語とは異なり、一階述語論理の言語は完全に形式的であるため、与えられた式が整形式かどうかを機械的に判断できます。整形式表現には、オブジェクトを直感的に表す項と、真または偽になり得る文を直感的に表す式という2つの主要な種類があります。一階述語論理の項と式は記号の列であり、すべての記号が一緒に言語の アルファベットを形成します。

アルファベット

すべての形式言語と同様に、記号自体の性質は形式論理の範囲外であり、多くの場合、単なる文字や句読点として扱われます。

アルファベットの記号は、常に同じ意味を持つ論理記号と、解釈によって意味が変化する非論理記号に分けるのが一般的です。 ^[9]例えば、論理記号は常に「and」を表します。論理記号で表される「or」と解釈されることはありません。しかし、Phil( x )のような非論理述語記号は、解釈に応じて「xは哲学者である」、「xはPhilipという名前の男性である」、またはその他の単項述語を意味すると解釈される可能性があります。 $\land$ $\lor$

論理記号

論理記号は、著者によって異なる文字の集合ですが、通常は以下を含みます。^[10]

量指定子記号：全称量化の場合は $گ$ 、存在量化の場合は $\exists$
論理接続詞：連言は $\land$ 、選言は $\lor$ 、含意は $\to$ 、二条件文は $\leftrightarrow$ 、否定は¬。一部の著者 $[$ ^{11]は、特に} $\to$ が他の目的で使用されている文脈において、 $\to$ の代わりにC pqを、 $\leftrightarrow$ の代わりにE pqを使用しています。さらに、馬蹄形 $\supsetは$ $\to$ の代わりに使用されることがあります。 ^[8]三重バー $\equivは$ $\leftrightarrowの$ 代わりに使用されることがあります。チルダ（ $~$ ）、N p、またはF pは $\neg$ の代わりに使用されることがあります。二重バー、、^[12]またはA pqは $\lorの$ 代わりに使用されることがあります。また、特に技術的な理由でこれらの記号が使用できない場合は、アンパサンド＆、K pq、または中点⋅は∧の代わりに使用されることがあります。 $\|$ $+$
括弧、角括弧、その他の句読点。これらの記号の選択は文脈によって異なります。
変数の無限集合。アルファベットの末尾に小文字x、y、z、 ... で表されることが多い。添え字は変数を区別するためによく使用される。例： $x 0 、 x 1 、 x 2 、 ... 。$
等号記号（同一性記号と呼ばれることもある） $=$ （以下の§ 等号とその公理を参照）。

これらの記号のすべてが一階述語論理で必要なわけではない。量指定子のいずれか1つと、否定、連言（または選言）、変数、括弧、および等号があれば十分である。

その他の論理記号には以下が含まれる。

真理値定数：「真」の場合はT、または $⊤$ 、「偽」の場合はF、または $⊥$ 。このような価数0の論理演算子がない場合、これらの2つの定数は量指定子を使用してのみ表現できる。
シェファーストローク、D pq（NAND）、排他的論理和、J pqなどの追加の論理接続詞

非論理記号

非論理記号は、述語（関係）、関数、定数を表します。かつては、あらゆる目的に固定された無限の非論理記号の集合を使用するのが標準的な方法でした。

n ≥ 0のすべての整数に対して、 n項またはn位の述語記号の集合が存在します。これらはn個の要素間の関係を表すため、関係記号とも呼ばれます。各項数nに対して、それらは無限に存在します。
P ⁿ₀、P ⁿ₁、P ⁿ₂、P ⁿ₃、…
n ≥ 0のすべての整数に対して、 n項関数記号は 無限に存在します。
f ⁿ₀、f ⁿ₁、f ⁿ₂、f ⁿ₃、…

述語記号または関数記号の項数が文脈から明らかな場合、上付き文字nは省略されることがよくあります

この伝統的なアプローチでは、一階述語論理の言語は1つしかありません。^[13]このアプローチは、特に哲学志向の書籍では今でも一般的です

最近の慣習では、想定している用途に応じて異なる非論理記号を使用することになっています。そのため、特定の用途で使用されるすべての非論理記号の集合に名前を付ける必要が生じています。この選択は、シグネチャ^[14]を介して行われます。

数学における典型的なシグネチャは、群の場合は{1, ×}または単に{×}、 ^{[3] 、}順序付き体の場合は{0, 1, +, ×, <}です。非論理記号の数に制限はありません。シグネチャは空、有限、無限、さらには無数にすることができます。無数シグネチャは、例えば、レーヴェンハイム・スコーレム定理の現代の証明に見られます。

シグネチャは場合によっては非論理記号の解釈方法を暗示するかもしれませんが、シグネチャ内の非論理記号の解釈は別個であり（必ずしも固定されているわけではありません）、シグネチャは意味論ではなく構文に関係します。

このアプローチでは、すべての非論理記号は次のいずれかのタイプになります

0以上の価数（または引数の数）を持つ述語記号（または関係記号）。これらは、P 、 Q 、 Rなどの大文字で表記されることが多いです。例：
- P ( x )において、Pは価数1の述語記号です。考えられる解釈としては、「xは男性である」などがあります。
- Q ( x , y )において、Qは価数2の述語記号です。考えられる解釈としては、「xはyより大きい」や「xはyの父親である」などがあります。
- 価数0の関係は、任意の文を表すことができる命題変数と同一視できます。Rの考えられる解釈としては、「ソクラテスは男性である」などがあります。
0以上の価数を持つ関数記号。これらは、f、g、hなどの小文字のローマ字で表記されることが多いです。例：
- f ( x ) は「 xの父」と解釈されることがあります。算術では「-x」を表すこともあります。集合論では「 x の冪集合」を表すこともあります。
- 算術では、g ( x , y )は「 x + y 」を表すことがあります。集合論では、「xとyの和」を表すことがあります。
- 価数0の関数記号は定数記号と呼ばれ、アルファベットの先頭に小文字で表されます（a、b、cなど）。記号aはソクラテスを表すことがあります。算術では0を表すことがあります。集合論では空集合を表すことがあります。

従来のアプローチは、単に「カスタム」シグネチャを従来の非論理記号のシーケンスで構成するように指定するだけで、現代的なアプローチで再現できます。

形成規則

形成規則は、一階述語論理の項と式を定義します。^[16]項と式が記号の列として表現される場合、これらの規則を使用して項と式の形式文法を記述できます。これらの規則は一般に文脈自由です（各生成規則の左側には1つの記号があります）。ただし、記号の集合が無限に許される場合があり、開始記号が多数存在する場合があります（例えば、項の場合の変数）。

項

項の集合は、以下の規則によって帰納的に定義されます。^[17]

変数。任意の変数記号は項です。
関数。fがn項関数記号であり、t ₁ , ..., t _{n が}項である場合、f ( t ₁ , ..., t _n ) は項です。特に、個々の定数を表す記号は零項関数記号であり、したがって項です。

規則1と規則2を有限回適用して得られる式のみが項です。たとえば、述語記号を含む式は項ではありません。

式

式（整形式式^[18]またはWFFとも呼ばれる）の集合は、以下の規則によって帰納的に定義されます

Predicate symbols. If P is an n-ary predicate symbol and t₁, ..., t_n are terms then P(t₁,...,t_n) is a formula.
- 等号。等号記号が論理の一部とみなされ、 t ₁とt ₂が項である場合、 t ₁ = t ₂は式です。
否定。が式である場合、 $\varphi$ $\lnot \varphi$ は式です。
二項接続詞。⁠ ⁠ と⁠ ⁠ が式である場合、 $\varphi$ （ $\psi$ $\varphi \rightarrow \psi$ ) は式です。同様の規則は他の二項論理接続詞にも適用されます。
量指定子。が式で、xが変数である場合、（すべてのxに対して、が成り立ちます）であり、（となるxが存在する $\varphi$ $\forall x\varphi$ $\varphi$ $\exists x\varphi$ $\varphi$ )は式です。

規則1～4を有限回適用することで得られる式のみが式です。最初の2つの規則から得られる式は、原子式と呼ばれます。と呼ばれます。

例えば：

\forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))

が式である場合、fが単項関数記号、Pが単項述語記号、Qが三項述語記号です。ただし、 $\forall x\,x\rightarrow$ はアルファベットの記号の文字列ですが、式ではありません

定義における括弧の役割は、任意の式が帰納的定義に従うことによってのみ1つの方法でのみ得られることを保証することです（つまり、各式には一意の構文木があります）。この特性は一意の可読性として知られていますとして知られています。式における括弧の使用箇所については、多くの慣習があります。例えば、著者によっては括弧の代わりにコロンやピリオドを使用したり、括弧の挿入場所を変更したりします。各著者の特定の定義には、一意の可読性の証明を添付する必要があります。

表記規則

便宜上、論理演算子の優先順位に関する慣習が開発されており、場合によっては括弧を書かなくても済むようになっています。これらの規則は、算術における演算の順序に似ています。一般的な慣習は次のとおりです。

$\lnot$ が最初に評価されます
$\land$ そして $\lor$ 次に評価されます
量指定子は次に評価されます
$\to$ そして $\leftrightarrow$ 最後に評価されます

さらに、式を読みやすくするために、定義で必要のない追加の句読点が挿入される場合があります。したがって、式：

\lnot \forall xP(x)\to \exists x\lnot P(x)

は次のように書かれるかもしれません：

(\lnot [\forall xP(x)])\to \exists x[\lnot P(x)].

自由変数と束縛変数

式において、変数は自由出現または束縛出現（あるいはその両方）することがあります。この概念の形式化の一つはQuineによるもので、まず変数出現の概念が定義され、次に変数出現が自由か束縛か、そして変数記号全体が自由か束縛かが定義されます。同一の記号xの異なる出現を区別するために、式φにおける変数記号xの各出現は、記号xのインスタンスが現れる時点までのφの最初の部分文字列と同一視されます。^[8]^{p. 297}次に、xの出現が、またはの少なくとも一方のスコープ内にある場合、その出現は束縛されていると言われます。最後に、φにおけるxのすべての出現が束縛されている場合、 xはφにおいて束縛されています。 ^[8] $\exists x$ $\forall x$ ^{pp. 142–143}

$直感的に、変数記号は$ $、どの時点で$ $も$ 量化されていない場合 $、$ 式において自由です。 $[$ $8$ ^] $pp$ ^{. 142–143} $...$ 変数

x が( φ → ψ )において自由出現する場合、かつその場合において、 x がφまたはψのいずれかにおいて自由出現する。xが( φ → ψ )において束縛出現する場合、かつその場合において、 x がφまたはψのいずれかにおいて束縛出現する。→ の代わりに他の二項接続詞にも同じ規則が適用されます。: φが原子式である場合、 xがφに自由出現するのは、 xがφに出現する場合に限ります。
否定: x が¬ φに自由出現する場合、かつその場合においてx がφに自由出現する。xが¬ φに束縛出現する場合、かつその場合においてx がφに束縛出現する。
二項接続詞: x が( φ → ψ ) で自由出現する場合、かつその場合、x がφまたはψのいずれかで自由出現する場合に限ります。xが( φ → ψ ) で束縛出現する場合、かつその場合、xがφまたはψのいずれかで束縛出現する場合に限ります。. The same rule applies to any other binary connective in place of →.
量指定子: x が $\forall y φ$ に自由出現する場合、 x がφに自由出現し、かつxがyとは異なる記号である場合に限ります。また、x が $\forall y φ$ に束縛出現する場合、x がyであるか、またはx がφに束縛出現する場合に限ります。同じ規則は、 $\exists を$ $\forall$ の代わりに使用した場合にも適用されます。

例えば、 $\forall x y (P (x) \to Q (x, f (x), z))$ では、xとy は束縛出現する場合のみ出現します。^[19] z自由出現のみで、 w は自由変数としてのみ出現します。 is neither because it does not occur in the formula.

式の自由変数と束縛変数は、互いに素な集合である必要はありません。式 $P (x) \to \forall x Q (x)において、$ Pの引数として最初に出現するxはQの引数としての 2 番目の出現は束縛されています

一階述語論理において、自由変数の出現がない式は一階述語文と呼ばれます。これらは、ある解釈の下で明確に定義された真理値を持つ式です。例えば、Phil( x ) のような式が真かどうかは、 x が何を表しているかに依存します。しかし、文 $\exists x Phil(x)$ は、与えられた解釈においては真か偽かのいずれかになります。

例：順序アーベル群

数学において、順序付きアーベル群の言語はは、定数記号0が1つ、単項関数記号-が1つ、二項関数記号+が1つ、二項関係記号≤が1つあります。したがって、

+( x , y ) と +( x ,+( y ,-( z ))) という式は項です。これらは通常、 x + yとx + y - zと書きますです。これらは通常、
+( x , y ) = 0 および ≤(+( x , +( y , −( z ))), +( x , y )) は原子式です。これらは通常、 x + y = 0 およびx + y − z ≤ x + yと書きます。
この式は式であり、通常は次のように書きます。この式には1つの自由変数zがあります。 $(\forall x\forall y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \forall x\,\forall y\,\mathop {+} (x,y)=0)]$ $\forall x\forall y(x+y\leq z)\to \forall x\forall y(x+y=0).$

順序付きアーベル群の公理は、言語の文の集合として表現できます。たとえば、群が可換であるという公理は通常、次のように書きます。 $(\forall x)(\forall y)[x+y=y+x].$

意味論

第一階言語の解釈は、その言語の非論理記号（述語記号、関数記号、または定数記号）にそれぞれ表示を割り当てます。また、量指定子の範囲を指定する談話領域も決定します。その結果、各項にはそれが表すオブジェクトが割り当てられ、各述語にはオブジェクトのプロパティが割り当てられ、各文には真理値が割り当てられます。このように、解釈は言語の項、述語、および式に意味論的な意味を提供します。形式言語の解釈の研究は形式意味論と呼ばれます。以下は、第一階論理の標準的またはタルスキアン意味論の説明です。（第一階論理のゲーム意味論を定義することも可能ですが、選択公理を必要とすることを除いて）、ゲーム意味論は第一階論理のタルスキアン意味論と一致するため、ここではゲーム意味論については詳しく説明しません。）

第一階構造

解釈を特定する最も一般的な方法（特に数学において）は、構造（モデルとも呼ばれます。以下を参照）を特定することです。構造は談話領域Dで構成されますと、非論理記号を述語、関数、定数にマッピングする解釈関数 $Iで構成されます$

議論領域Dは、ある種の「オブジェクト」の空でない集合です。直感的に、解釈が与えられた場合、一階述語論理式はこれらのオブジェクトに関する文になります。例えば、述語Pが真である（より正確には、解釈によって述語記号Pに割り当てられた述語が真である） D内のオブジェクトの存在を述べています。例えば、Dを取ることができます。 $\exists xP(x)$ 整数の集合とすることができます。

非論理記号は次のように解釈されます。

n項関数記号の解釈は、 D ⁿからDへの関数です。例えば、議論領域が整数の集合である場合、引数が2の関数記号f は、引数の和を与える関数として解釈できます。言い換えれば、記号fは関数に関連付けられています。 $I(f)$ に関連付けられており、この解釈では、これは加算です
定数記号（引数が0の関数記号）の解釈は、 D ^{0 （唯一の要素が空の}組である集合）からDへの関数であり、これはD内のオブジェクトと単純に同一視できます。例えば、解釈は定数記号に値を割り当てることがあります $I(c)=10$ $c$ 。
n項述語記号の解釈は、 Dの要素のn組の集合であり、述語が真となる引数を与えます。たとえば、2項述語記号Pの解釈は、最初の引数が2番目の引数より小さい整数のペアの集合である可能性があります。この解釈によれば、述語Pは、最初の引数が2番目の引数より小さい場合に真となります。同様に、述語記号にはD ⁿからへのブール値関数を割り当てることができます。 $I(P)$ $\{\mathrm {true,false} \}$

真理値の評価

式は、解釈と、談話領域の要素を各変数に関連付ける変数割り当てμが与えられた場合、真または偽に評価されます。変数割り当てが必要な理由は、などの自由変数を持つ式に意味を与えるためです。この式の真理値は、 xとの値によって変化します。 $y=x$ yが示す

まず、変数割り当てμは言語のすべての用語に拡張でき、その結果、各用語は談話領域の単一の要素にマッピングされます。この割り当てを行うために、以下の規則が使用されます。

変数。各変数xはμ（）に評価されます。談話領域の要素に評価された項と、 n項関数記号場合x )
次に、各式に真理値が割り当てられます。この割り当てを行うために使用される帰納的定義は、 Tスキーマと呼ばれます。 $t_{1},\ldots ,t_{n}$ $d_{1},\ldots ,d_{n}$ $f(t_{1},\ldots ,t_{n})$ $(I(f))(d_{1},\ldots ,d_{n})$ 。

次に、各式に真理値が割り当てられます。この割り当てを行うために使用される帰納的定義は、Tスキーマと呼ばれます。

原子式（1）。式は、かどうかに応じて真または偽の値が関連付けられます。ここで、は用語の評価であり、はの解釈であり、仮定によりのサブセットです。 $P(t_{1},\ldots ,t_{n})$ $\langle v_{1},\ldots ,v_{n}\rangle \in I(P)$ $v_{1},\ldots ,v_{n}$ $t_{1},\ldots ,t_{n}$ $I(P)$ $P$ $D^{n}$
原子式（2） 。とが談話領域の同じオブジェクトに評価される場合、式は真に割り当てられます（以下の等式に関するセクションを参照）。 $t_{1}=t_{2}$ $t_{1}$ $t_{2}$
論理接続詞。、などの形式の式は、命題論理と同様に、該当する接続詞の真理値表に従って評価されます。 $\neg \varphi$ $\varphi \rightarrow \psi$
存在量指定子。式は、 Mと変数の評価がxの評価に関して最大でと異なり、解釈Mと変数割り当てに従って φ が真となる場合、真となります。この正式な定義は、 φ( x ) が満たされるようにxの値を選択する方法がある場合にのみ真となるという考えを捉えています。 $\exists x\varphi (x)$ $\mu$ $\mu '$ $\mu$ $\mu '$ $\exists x\varphi (x)$
全称量指定子。式は、 Mと、解釈Mと変数割り当てによって構成されるすべてのペアに対して φ(x) が真である場合、真となります。これは、xの値のあらゆる可能な選択がφ( x ) を真にする場合に真となるという考えを捉えています $\forall x\varphi (x)$ $\mu$ $\mu '$ $\mu$ $\forall x\varphi (x)$

式が自由変数を含まず、したがって文である場合、最初の変数代入はその真理値に影響を与えません。言い換えれば、文がMに従って真であり、かつMと他のすべての変数代入に従って真である場合に限ります。 $\mu$ $\mu '$

変数割り当て関数に依存しない、真理値を定義する2つ目の一般的なアプローチがあります。代わりに、解釈Mが与えられた場合、まずシグネチャに定数記号の集合を追加します。定数記号は、Mの談話領域の各要素に1つずつ割り当てられます。つまり、領域内の各dに対して、定数記号c _dが固定されているとします。解釈は拡張され、新しい定数記号はそれぞれ、対応する領域の要素に割り当てられます。ここで、量化式の真理値は、次のように構文的に定義されます。

存在量化子（代替） 。談話領域にdが存在し、かつが成り立つ場合、式はMに従って真です。φにおけるxの自由出現ごとにc _dを代入した結果は次のとおりです。 $\exists x\varphi (x)$ $\varphi (c_{d})$ $\varphi (c_{d})$
全称量化子（代替） 。談話領域内のすべてのdに対して、 Mに従ってが真である場合、式はMに従って真です。 $\forall x\varphi (x)$ $\varphi (c_{d})$

この代替アプローチは、変数割り当てによるアプローチとまったく同じ真理値をすべての文に与えます

妥当性、充足可能性、および論理的帰結

文φが与えられた解釈Mの下で真と評価される場合、Mはφを満たすと言われます。これは^[20]で表されます。文が充足可能であるとは、それが真となる解釈が存在する場合です。これはモデル理論の記号とは少し異なります。ここで、はモデルにおける充足可能性を表します。つまり、「のドメイン内の値をの変数記号に適切に割り当てることができる」ということです $M\vDash \varphi$ $\vDash$ $M\vDash \phi$ $M$ $\phi$ 適切に割り当てることができる」ことを表します。^[21]

自由変数を持つ式の充足可能性はより複雑です。なぜなら、解釈だけではそのような式の真理値を決定しないからです。最も一般的な慣習は、自由変数, ...,を持つ式 φ が、その自由変数, ... ,に談話領域のどの個体が割り当てられているかにかかわらず、式 φ が真のままであるとき、その解釈によって充足されるというものです。これは、式 φ が満たされるには、その全称閉包が満たされる必要があるという場合と同じ効果があります。 $x_{1}$ $x_{n}$ $x_{1}$ $x_{n}$ $\forall x_{1}\dots \forall x_{n}\phi (x_{1},\dots ,x_{n})$ が満たされる

式は、すべての解釈において真である場合、論理的に妥当（または単に妥当）です。 ^[22]これらの式は、これらの式は、命題論理におけるトートロジー

式 φ は論理的帰結です。である場合、 ψ を真とするすべての解釈が φ も真とします。この場合、 φ は ψ によって論理的に含意されると言えます。

代数化

第一階述語論理の意味論への別のアプローチは、抽象代数を介して行われます。このアプローチは、命題論理のリンデンバウム・タルスキ代数を一般化します。量化子を他の変数結合項演算子に置き換えることなく、第一階述語論理から量化変数を除去する方法は3つあります。

これらの代数はすべて、適切に拡張する束です 2要素ブール代数です。

TarskiとGivant（1987）は、 3つ以上の量化子のスコープ内にある原子文を持たない一階述語論理の断片は、関係代数と同じ表現力を持つことを示した。^[23]^：32–33この断片は、ペアノ算術と、標準的なツェルメロ・フランケル集合論（ZFC）を含むほとんどの公理的集合論に十分であるため、非常に興味深い。彼らはまた、原始的な順序対を持つ一階述語論理が、2つの順序対射影関数を持つ関係代数と同値であることを証明している。^[24]^：803

一階述語理論、モデル、および基本クラス

特定のシグネチャの一階述語理論は、そのシグネチャの記号からなる文である公理の集合である。公理の集合は、しばしば有限または再帰的に列挙可能である。あり、その場合、理論はと呼ばれる有効と呼ばれます。一部の著者は、理論が公理のすべての論理的帰結も含むことを要求します。公理は理論の範囲内で成立すると考えられ、そこから理論の範囲内で成立する他の文を導き出すことができます

与えられた理論のすべての文を満たす一階述語構造は、その理論のモデルと呼ばれる。基本クラスとは、特定の理論を満たすすべての構造の集合です。これらのクラスは、主要な研究対象ですモデル理論の主要な研究対象です。

多くの理論には、意図された解釈、つまり理論を研究する際に念頭に置かれる特定のモデルがあります。例えば、ペアノ算術の意図された解釈は、通常の自然数で構成されています。とその通常の演算から構成されます。しかし、レーヴェンハイム・スコーレムの定理は、ほとんどの一階理論には他の解釈もあることを示しています。とその通常の演算で構成されます。しかし、レーヴェンハイム・スコーレムの定理は、非標準的なモデルもあることを示しています

理論は、理論の公理から矛盾を証明できない場合、（演繹体系において）整合しています。理論は、そのシグネチャ内のすべての式について、その式またはその否定のいずれかが理論の公理の論理的帰結である場合、完全です。ゲーデルの不完全性定理自然数の算術の十分な部分を含む有効な一階理論は、無矛盾かつ完全であることは決してできないことを示している。

空領域

上記の定義では、あらゆる解釈の論議領域が空でないことが必要です。包含論理などの設定があります。。さらに、代数構造のクラスに空構造が含まれる場合（たとえば、空半集合がある場合）、そのクラスは空領域が許容されるか、空構造がクラスから削除される場合にのみ、一階論理の基本クラスになることができる。

しかし、空領域にはいくつかの困難がある

多くの一般的な推論規則は、論議領域が空でないことが必要な場合にのみ有効です。一例として、 xがにおいて自由変数でない場合、が成り立つという規則があります。この規則は、式を冠頭正規形にするために使用されます $\varphi \lor \exists x\psi$ $\exists x(\varphi \lor \psi )$ $\varphi$ 空でない領域では健全ですが、空領域が許容される場合は不健全です
変数代入関数を用いる解釈における真理値の定義は、空の定義域では機能しません。なぜなら、値域が空である変数代入関数は存在しないからです。（同様に、定数記号に解釈を割り当てることはできません。）この真理値定義では、原子式であっても真理値を定義する前に、変数代入関数（上記のμ）を選択しなければなりません。すると、文の真理値は任意の変数代入におけるその真理値として定義され、この真理値はどの代入が選択されるかに依存しないことが証明されます。この手法は代入関数が全く存在しない場合は機能しません。空の定義域に対応するように変更する必要があります。

したがって、空の定義域が許容される場合、それはしばしば特別なケースとして扱われなければなりません。しかし、ほとんどの著者は定義によって空の定義域を単に除外しています。

演繹システム

演繹体系は、純粋に統語論的な根拠に基づいて、ある式が別の式の論理的帰結であることを示すために使用されます。一階述語論理には、ヒルベルト式演繹体系、自然演繹、シークエント計算、タブロー法、導出など、多くのそのような体系があります。これらは、演繹が有限の統語的オブジェクトであるという共通の性質を共有しています。このオブジェクトの形式と構築方法は多岐にわたります。これらの有限の演繹自体は、証明論ではしばしば導出と呼ばれます。また、証明とも呼ばれますが、自然言語とは異なり、完全に形式化されています。と呼ばれることもありますが、数学的証明とは異なり、完全に形式化されています

演繹体系は、その体系で導出できる式が論理的に有効である場合に健全です。逆に、演繹体系は、論理的に有効なすべての式が導出可能である場合に完全です。この記事で説明するすべての体系は、健全かつ完全です。また、有効であるとされる演繹が実際に演繹であることを効果的に検証できるという性質も共有しています。このような演繹体系は、。このような演繹体系は、有効であると呼ばれる。

演繹体系の重要な性質は、純粋に統語論的であるため、解釈を考慮せずに導出を検証できることである。したがって、健全な議論は、その解釈が数学、経済学、またはその他の分野に関するものであるかどうかに関係なく、言語のあらゆる可能な解釈において正しい

一般に、一階述語論理における論理的帰結は半決定可能のみです。文Aが文Bを論理的に含意する場合、これは発見可能です（例えば、効果的で健全で完全な証明システムを用いて、証明が見つかるまで証明を探すことによって）。しかし、Aが論理的にBを含意しない場合でも、Aが論理的にBの否定を含意するわけではありません。式AとBが与えられたときに、Aが論理的にBを含意するかどうかを常に正しく判断できる効果的な手順はありません。

推論規則

推論の規則は、ある性質を持つ特定の式（または式の集合）を仮説として与えられた場合、別の特定の式（または式の集合）を結論として導き出せることを述べています。ある解釈が仮説を満たすときはいつでも、その解釈は結論も満たすという意味で妥当性を維持する場合、その規則は健全（または真理保存）です

例えば、一般的な推論規則の1つに置換規則があります。tが項で、φが変数xを含む可能性のある式である場合、 φ [ t / x ]はφにおけるxのすべての自由インスタンスをtに置き換えた結果です。置換規則は、任意のφと任意の項tについて、置換プロセス中にtの自由変数が束縛されない限り、φからφ[ t / x ]を推論できると述べています。（ tの自由変数が束縛された場合、 tをxに置き換えるには、まずφの束縛変数をxの自由変数と異なるように変更する必要があります。）まずφの束縛変数をt。）

束縛変数への制限がなぜ必要なのかを理解するために、算術の(0,1,+,×,=)の符号において、で与えられる論理的に有効な式 φ を考えてみましょう。tが項「x + 1」である場合、式 φ[ t / y ] はとなり、多くの解釈において誤りとなります。問題は、tの自由変数x が置換中に束縛されたことです。意図した置換は、φの束縛変数x を別の名前、例えばzに変更することで得られます。置換後の式は次のようになります $\exists x(x=y)$ $\exists x(x=x+1)$ $\exists z(z=x+1)$ 、これも論理的に有効になります

置換規則は、推論規則のいくつかの一般的な側面を示しています。これは完全に統語論的なものであり、いかなる解釈にも頼ることなく、正しく適用されたかどうかを判断できます。適用できるタイミングには（統語論的に定義された）制限があり、導出の正確性を保つためには、この制限を尊重する必要があります。さらに、よくあることですが、これらの制限は、推論規則に含まれる式の統語的操作中に発生する自由変数と束縛変数間の相互作用のために必要です。

ヒルベルトスタイルのシステムと自然演繹

ヒルベルト式の演繹体系における演繹は、論理公理、すなわち、現在の導出のために仮定された仮説、または推論規則を介して前の式から導かれる仮説である式のリストです。論理公理は、論理的に有効な式の複数の公理スキーマで構成され、これらはかなりの量の命題論理を包含しています。推論規則は、量化子の操作を可能にします。典型的なヒルベルト式の体系は、少数の推論規則と、複数の無限の論理公理スキーマを持っています。通常は、可能性法と普遍一般化のみを持つのが一般的です。

自然演繹体系は、演繹が式の有限のリストであるという点で、ヒルベルト式の体系に似ています。しかし、自然演繹体系には論理公理がありません。証明における式の論理接続詞を操作するために使用できる追加の推論規則を追加することでそれを補います。

シークエント計算

シークエント計算は、自然演繹体系の特性を研究するために開発されました。^[25]一度に1つの式を扱う代わりに、次の形式の表現である シークエントを使用します

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},

ここで、A ₁、…、A _n、B ₁、…、B _kは式であり、回転式記号は2つの部分を区切る句読点として使用されています。直感的に、シークエントは次の考えを表現します $\vdash$ $(A_{1}\land \cdots \land A_{n})$ $(B_{1}\lor \cdots \lor B_{k})$ 。

タブロー法

先ほど説明した方法とは異なり、タブロー法における導出は式のリストではありません。導出は式のツリーです。式Aが証明可能であることを示すために、タブロー法はAの否定が不満足であることを証明しようとします。導出のツリーはルートにを持ち、式の構造を反映してツリーは分岐します。例えば、が不満足であることを示すには、CとDがそれぞれ不満足であることを示す必要があります。これは、親を持つツリーの分岐点に対応します。 $\lnot A$ $C\lor D$ $C\lor D$ と子がCとD

解決

解決規則統一と組み合わせることで、一階述語論理に対して健全かつ完全な単一の推論規則です。タブロー法と同様に、式は式の否定が不満足であることを示すことによって証明されます。解決は、自動定理証明でよく使用されます

解決法は、原子式の選言である式に対してのみ機能します。任意の式は、まずスコレム化によってこの形式に変換する必要があります。解決規則は、仮説とから結論を述べています。 $A_{1}\lor \cdots \lor A_{k}\lor C$ $B_{1}\lor \cdots \lor B_{l}\lor \lnot C$ $A_{1}\lor \cdots \lor A_{k}\lor B_{1}\lor \cdots \lor B_{l}$

証明可能恒等式

特定の式間の同値性を証明する多くの恒等式が証明できます。これらの恒等式は、量指定子を他の接続詞間で移動することで式を並べ替えることを可能にし、式を冠頭正規形にするのに役立ちます。証明可能恒等式には以下が含まれます。

\lnot \forall x\,P(x)\Leftrightarrow \exists x\,\lnot P(x)

\lnot \exists x\,P(x)\Leftrightarrow \forall x\,\lnot P(x)

\forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)

\exists x\,\exists y\,P(x,y)\Leftrightarrow \exists y\,\exists x\,P(x,y)

\forall x\,P(x)\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\land Q(x))

\exists x\,P(x)\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P(x)\lor Q(x))

P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))

（ただし、はにおいて自由に出現してはならない）

x

P

P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))

ただし、自由に出現してはならない）

x

P

）

等式とその公理

一階述語論理において等式（または恒等式）を使用するには、いくつかの異なる慣例があります。最も一般的な慣例は、等式を伴う一階述語論理として知られており、等式記号を基本論理記号として含みます。これは常に、談話領域のメンバー間の真の等式関係として解釈され、「2つの」与えられたメンバーは同じメンバーです。このアプローチは、使用される演繹システムに等式に関する特定の公理も追加します。これらの等式公理は次のとおりです。^[26]^：198–200

反射性。各変数xについて、x = xです
関数の置換。すべての変数xとy、および任意の関数記号についてfについてについて、
x = y → f (..., x , ...) = f (..., y , ...)
式の置換。任意の変数xとy、および任意の式φ( zについて 、および自由変数 z を持つ
x = y → (φ(x) → φ(y))。

これらは公理スキームであり、それぞれが無限の公理の集合を指定します。3番目のスキームはライプニッツの法則、「置換原理」、「同一物の識別不能性」、または「置換特性」として知られています。2番目のスキームは、関数記号fを含みます。を含む2番目のスキームは、3番目のスキームの特殊なケース（と同等）であり、次の式を使用します。

φ(z): f (..., x , ...) = f (..., z , ...)

そして

x = y → ( f (..., x , ...) = f (..., x , ...) → f (..., x , ...) = f (..., y , ...))

x = yが与えられており、反射性によりf (..., x , ...) = f (..., x , ...)が成り立つため、 f (..., x , ...) = fとなります。 (...,y , ...) が成り立ちます。

等式に関する他の多くの性質は、上記の公理の帰結です。例えば

対称性。x = yの場合、y = xです
推移性。x = y かつ y = z ならば、x = zである。[ 28 ]

等式のない一階述語論理

アプローチでは、等式関係を非論理記号とみなします。この慣習は、等式のない一階述語論理として知られています。等式関係がシグネチャに含まれている場合、等式公理は、論理の規則とみなされるのではなく、必要に応じて検討中の理論に追加する必要があります。この方法と等式のある一階述語論理の主な違いは、解釈によって2つの異なる個体が「等しい」と解釈できるようになったことです（ただし、ライプニッツの法則によれば、これらはどのような解釈においても全く同じ式を満たします）。つまり、等式関係は、談話領域上の任意の同値関係によって解釈できるようになりました解釈の機能と関係に関して合同

この2番目の慣例に従う場合、「正規モデル」という用語は、 a = bを満たす異なる個体aとbが存在しない解釈を指すために使用されます。等式を含む一階述語論理では、正規モデルのみが考慮されるため、正規モデル以外のモデルを表す用語は存在しません。等式を含まない一階述語論理を研究する場合、次のような結果の記述を修正する必要があります。レーヴェンハイム・スコーレム定理などの結果の記述を修正し、正規モデルのみが考慮されるようにする必要があります。

等式のない一階述語論理は、二階算術の文脈でしばしば用いられます。やその他の高階算術理論の文脈でよく用いられ、自然数の集合間の等式関係は通常省略されます。

理論における等式の定義

理論が反射性とライプニッツの法則を満たす二項式A ( x , y )を持つ場合、その理論は等式を持つ、または等式を持つ理論であると言われます。理論は上記の図式のすべてのインスタンスを公理として持つとは限らず、導出可能な定理として持つ場合があります。例えば、関数記号がなく、関係が有限数しかない理論では、sを変更しても関係が変化しない場合、2つの項sとtを等しいと定義することにより、関係に基づいて等式を定義することができます。tに任意の議論でt

一部の理論では、他のアドホックな等式の定義が可能です。

1つの関係記号≤を持つ半順序理論では、 s = tをs ≤ t t ≤の略語として定義できます $\wedge$ 略記ます
$関係\in$ $が$ $1つ$ ある集合論において、s = tを、の略語として定義することができます $。$ この等式の $定義$ $は$ $\wedge$ 等式 $の$ $公理$ $を$ $自動的$ $に$ 満たし $ます$ $。$ $この$ 場合、 $と$ 述べることができる通常の外延性公理を、 $集合$ $x$ $と$ $y$ $が$ $...$ $\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y]$ $\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)]$

メタ論理的性質

1929年にクルト・ゲーデルによって証明されたゲーデルの完全性定理は、一階述語論理には健全で完全かつ有効な演繹体系が存在することを確立し、したがって一階述語論理的帰結関係は有限証明可能性によって捉えられます。素朴に言えば、式φが論理的に式ψを導くという命題は、φのあらゆるモデルに依存します。これらのモデルは一般に任意に大きな基数を持つため、すべてのモデルをチェックすることによって論理的帰結を効果的に検証することはできません。しかし、すべての有限導出を列挙し、φからψの導出を探すことは可能です。ψがφから論理的に導かれる場合、そのような導出は最終的に発見されるでしょう。したがって、一階述語論理的帰結は性質があるためです。これらの結果は、個々の理論の性質ではなく、一階論理自体の一般的な性質に関するものです。これらは、一階理論のモデル構築のための基本的なツールを提供します。

完全性と決定不能性

1929年にクルト・ゲーデルによって証明されたゲーデルの完全性定理は、一階述語論理には健全で完全かつ有効な演繹体系が存在することを確立し、したがって一階述語論理的帰結関係は有限証明可能性によって捉えられます。単純に言えば、式φが論理的に式ψを含意するという命題は、φのすべてのモデルに依存します。これらのモデルは一般に任意に大きな基数を持つため、すべてのモデルをチェックすることによって論理的帰結を効果的に検証することはできません。しかし、すべての有限導出を列挙し、φからψの導出を探すことは可能です。ψがφから論理的に含意される場合、そのような導出は最終的に発見されるでしょう。したがって、一階述語論理的帰結は半決定可能であり、ψがφの論理的帰結となるようなすべての文のペア（φ、ψ）を効果的に列挙することが可能です

命題論理とは異なり、一階述語論理は、言語が少なくとも2アリティの述語（等式を除く）を少なくとも1つ持つ限り、決定不可能である（ただし半決定可能）。これは、任意の論理式が論理的に妥当であるかどうかを決定する決定手続きが存在しないことを意味する。この結果は、1936年と1937年にアロンゾ・チャーチとアラン・チューリングによってそれぞれ独立に確立され、1928年にデイヴィッド・ヒルベルトとヴィルヘルム・アッカーマンによって提起された決定問題（Entscheidungsproblem）に否定的な解答を与えた。彼らの証明は、一階述語論理の決定問題の解決不可能性と、に否定的な答えを与えました。彼らの証明は、一階述語論理の決定問題の解決不可能性と停止問題

完全な一階述語論理よりも弱い体系があり、その論理的帰結関係は決定可能です。これらには、命題論理とモナド述語論理が含まれます。モナド述語論理は、単項述語記号に制限され、関数記号を持たない一階述語論理です。関数記号を持たない他の決定可能な論理には、一階述語論理のガード付きフラグメントと2変数論理があります。一階述語論理のバーナイズ・シェーンフィンケルクラスも決定可能です。一階述語論理の決定可能な部分集合は、記述論理の枠組みでも研究されています。。

レーヴェンハイム＝スコーレムの定理

レーヴェンハイム・スコーレムの定理は、濃度λの一階理論に無限モデルがある場合、λ以上のすべての無限濃度のモデルが存在することを示しています。モデル理論における最も初期の結果の1つであり、可算性を特徴付けることができないことを意味します。つまり、一階述語論理φ(x )は、Mの議論領域が可算（または後者の場合は非可算）である場合に限り存在しません

レーヴェンハイム＝スコーレムの定理は、無限構造は一階論理では圏論的に公理化できないことを意味します。例えば、唯一のモデルが実数直線である一階理論は存在しません。無限モデルを持つすべての一階理論は、連続体よりも大きな濃度のモデルも持ちます。実数直線は無限であるため、実数直線によって満たされる理論は、いくつかの非標準的なモデルによっても満たされます。レーヴェンハイム＝スコーレムの定理を一階集合論に適用すると、直観に反する帰結は次のように知られています。スコーレムのパラドックスとして知られています。。

コンパクト性定理

コンパクト性定理は、一階文の集合がモデルを持つ場合と、そのすべての有限部分集合がモデルを持つ場合に限って、そのことを述べています。^[29]これは、ある式が一階述語公理の無限集合の論理的帰結である場合、それはそれらの公理の有限個の論理的帰結であることを意味する。この定理は、完全性定理の結果としてクルト・ゲーデルによって最初に証明されたが、時間の経過とともに多くの追加の証明が得られてきた。これはモデル理論における中心的なツールであり、モデルを構築するための基本的な方法を提供する

コンパクト性定理は、どの一階構造の集合が基本クラスであるかという制限効果を持ちます。例えば、コンパクト性定理は、任意に大きな有限モデルを持つすべての理論は無限モデルを持つことを意味します。したがって、すべての有限のクラスはグラフのクラスは基本クラスではありません（他の多くの代数構造についても同様です）。

コンパクト性定理によって暗示される、一階述語論理のより微妙な限界もあります。例えば、コンピュータサイエンスでは、多くの状況を状態（ノード）と接続（有向エッジ）の有向グラフとしてモデル化できます。このようなシステムを検証するには、いかなる「良い」状態からも「悪い」状態に到達できないことを示す必要がある場合があります。したがって、良い状態と悪い状態がグラフの異なる接続要素にあるかどうかを判断しようとします。しかし、コンパクト性定理は、接続グラフが一階述語論理の基本クラスではないことを示すために使用でき、グラフの論理において、 xからyへのパスがあるという考えを表現する一階述語論理の式φ( x , y )は存在しません。ただし、接続性は二階述語論理で表現できますが、存在集合量化子だけでは表現できません。 $\Sigma _{1}^{1}$ 。

リンドストロームの定理

ペル・リンドストローム、今議論したメタ論理的性質は、より強い論理がそれらの性質を同時に持つことはできないという意味で、実際には一階述語論理を特徴づけることを示した（Ebbinghaus and Flum 1994、第13章）。リンドストロームは抽象論理体系のクラスと、このクラスのメンバーの相対的な強さの厳密な定義を定義した。彼はこのタイプの体系について2つの定理を確立した。

一階述語論理を含み、レーヴェンハイム＝スコーレム定理とコンパクト性定理の両方を満たすリンドストロームの定義を満たす論理体系は、一階述語論理と同値でなければならない。
半決定可能な論理的帰結関係を持ち、レーヴェンハイム＝スコーレム定理を満たすリンドストロームの定義を満たす論理体系は、一階述語論理と同値でなければならない。

制限事項

一階述語論理は数学の多くを形式化するのに十分であり、コンピュータサイエンスなどの分野で一般的に使用されていますが、一定の限界があります。これには、表現力の限界と、記述できる自然言語の断片の限界が含まれます。

例えば、一階述語論理は決定不可能であり、証明可能性のための健全で完全かつ停止的な決定アルゴリズムは不可能であることを意味します。これは、C _{2 ：2つの変数と}計数量化子とを含む一階述語論理のような興味深い決定可能なフラグメントの研究につながりました。^[30] $\exists ^{\geq n}$ $\exists ^{\leq n}$

表現力

レーヴェンハイム・スコーレムの定理は、一階理論が任意の無限モデルを持つ場合、あらゆる濃度の無限モデルを持つことを示しています。特に、無限モデルを持つ一階理論は圏論的になり得ません。したがって、唯一のモデルが自然数の集合を定義域とする一階理論、または唯一のモデルが実数の集合を定義域とする一階理論は存在しません。無限論理や高階論理を含む一階論理の多くの拡張は、自然数または実数の圏論的公理化を可能にするという意味で、より表現力豊かです^[要説明]。しかし、この表現力はメタ論理的なコストを伴います。リンドストロームの定理により、コンパクト性定理と下向きのレーヴェンハイム・スコーレム定理は、一階よりも強い論理では成り立ちません。

自然言語の形式化

一階述語論理は、「パースに住むすべての人はオーストラリアに住んでいる」など、自然言語の多くの単純な量化子構文を形式化することができます。したがって、一階述語論理は、 FO(.)などの知識表現言語の基礎として使用されます。の基礎として使用されます。

それでも、一階述語論理では表現できない自然言語の複雑な特徴があります。「自然言語の分析のための道具として適切な論理システムは、一階述語論理よりもはるかに豊富な構造を必要とします。」^[31]

制約、拡張、およびバリエーション

第一階述語論理には多くのバリエーションがあります。これらの中には、意味に影響を与えずに表記法を変えるだけという意味で本質的ではないものもあります。他のバリエーションは、追加の量指定子やその他の新しい論理記号によって意味を拡張することで、表現力をより大きく変化させます。例えば、無限論理は無限サイズの式を許可し、様相論理は可能性と必然性の記号を追加します。

制約言語

第一階述語論理は、上記よりも論理記号の少ない言語で研究することができます。

はと表現でき、はと表現できるため、2つの量化子のいずれかと $\exists x\varphi (x)$ $\neg \forall x\neg \varphi (x)$ $\forall x\varphi (x)$ $\neg \exists x\neg \varphi (x)$ $\exists$ $\forall$ 削除できます
はと表すことができ、はと表すことができるため、またはのいずれかを省略できます。言い換えれば、と、またはとがあれば十分です。 $\varphi \lor \psi$ $\lnot (\lnot \varphi \land \lnot \psi )$ $\varphi \land \psi$ $\lnot (\lnot \varphi \lor \lnot \psi )$ $\vee$ $\wedge$ $\neg$ $\vee$ $\neg$ $\wedge$ 論理接続詞として
同様に、論理接続詞としてとのみ、またはシェファーストローク（NAND）またはパース矢印のみがあれば十分です $\neg$ $\rightarrow$
関数記号と定数記号を完全に回避し、述語記号を介して適切な方法で書き換えることが可能です。例えば、定数記号の代わりに述語（と解釈される）を使用し、などのすべての述語をに置き換えることができます。のような関数も同様にと解釈される述語に置き換えられます。この変更には、使用される述語記号の解釈が正しい意味を持つように、理論に追加の公理を追加する必要があります。^[32] $\;0$ $\;0(x)$ $\;x=0$ $\;P(0,y)$ $\forall x\;(0(x)\rightarrow P(x,y))$ $f(x_{1},x_{2},...,x_{n})$ $F(x_{1},x_{2},...,x_{n},y)$ $y=f(x_{1},x_{2},...,x_{n})$

このような制限は、演繹体系における推論規則や公理スキーマの数を減らす手法として有用であり、メタ論理的結果の証明を短縮することにつながります。しかし、この制限の代償として、自然言語の文を手元の形式体系で表現することがより困難になります。これは、自然言語の文で使用される論理接続詞を、制限された論理接続詞の集合を用いた（より長い）定義に置き換えなければならないためです。同様に、制限されたシステムにおける導出は、追加の接続詞を含むシステムにおける導出よりも長くなる可能性があります。したがって、形式体系内での作業の容易さと、形式体系に関する結果の証明の容易さの間にはトレードオフの関係があります。

十分に表現力のある理論では、関数記号と述語記号のアリティを制限することも可能です。ペアリング関数を含む理論では、原理的に、アリティが2より大きい関数とアリティが1より大きい述語を完全に省略することができます。これは、ドメインの要素のペアを取り、順序付きペアを返す、アリティが2の関数ですを返す、アリティが2の関数です。順序付きペアからその要素への射影関数を定義する、アリティが2の述語記号を2つ持つだけで十分です。どちらの場合も、ペアリング関数とその射影の自然公理が満たされている必要があります。

多ソート論理

通常の一階解釈は、すべての量化子が及ぶ単一の議論領域を持ちます。多ソート一階論理では、変数が異なるソートを持つことが許され、ソートは異なる領域を持ちます。これは型付き一階論理とも呼ばれ、ソートは型（データ型のように）と呼ばれますが、一階型理論とは異なります。多ソート一階論理は、二階算術の研究でよく用いられます。^[33]

理論に有限個の種しか存在しない場合、多ソート一階述語論理は単ソート一階述語論理に還元できる。^[34]^{: 296–299} 単ソート理論に、多ソート理論の各種に対応する単項述語記号を導入し、これらの単項述語が議論領域を分割するという公理を加える。例えば、2つの種が存在する場合、述語記号とと公理を加える。 $P_{1}(x)$ $P_{2}(x)$

\forall x(P_{1}(x)\lor P_{2}(x))\land \lnot \exists x(P_{1}(x)\land P_{2}(x))

そして、を満たす要素は第一種の要素、を満たす要素は第二種の要素とみなされます。対応する述語記号を用いて量化の範囲を制限することで、各種について量化を行うことができます。例えば、式を満たす第一種の要素が存在すると言うには、次のように書きます。 $P_{1}$ $P_{2}$ $\varphi (x)$

\exists x(P_{1}(x)\land \varphi (x))

追加の量化子

第一階述語論理には、追加の量化子を追加することができます。

$「 P (x)はちょうど1つの$ xに対して成り立つ」と言うことが便利な場合があり、これは $\exists! x P (x)$ と表すことができます。この表記法は一意性量化と呼ばれ、 $\wedge$ のような式を省略したものとみなすことができます
追加の量指定子を持つ一階述語論理には、新しい量指定子Qx 、…があり、「…となるようなxが多数存在する」などの意味を持ちます。また、ジョージ・ブーロスらによる分岐量指定子と複数量指定子も参照してください。
有界量指定子は、集合論や算術の研究でよく使用されます。

無限論理

無限論理は、無限に長い文を許容します。例えば、無限に多くの式の連言や選言、あるいは無限に多くの変数の量化を許容する場合があります。無限に長い文は、位相幾何学やモデル理論などの数学の分野で発生します

無限論理は一階述語論理を一般化し、無限長の式を許容します。式が無限になる最も一般的な方法は、無限の連言と選言です。しかし、関数記号や関係記号が無限の引数を持つことを許容したり、量指定子が無限の数の変数を束縛できるような一般化されたシグネチャを許容することも可能です。無限の式は有限の文字列で表現できないため、式の別の表現を選択する必要があります。この文脈における通常の表現は木です。したがって、式は本質的に、解析される文字列ではなく、その構文木と同一視されます

最も一般的に研究されている無限論理はL _αβと表記されます。ここで、α と β はそれぞれ基数または記号∞です。この記法では、通常の一階述語論理はL _ωωと表されます。論理L _∞ωでは、式を構築する際に任意の連言または選言が許され、変数の数は無制限です。より一般的には、κ個未満の構成要素を持つ連言または選言を許す論理はL _κωと呼ばれます。例えば、L _{ω ₁ ω は}可算な連言と選言を許します。

L _κωの論理式における自由変数の集合は、κ より小さい任意の濃度を持つことができますが、ある論理式が別の論理式の部分式として現れる場合、任意の量化子のスコープ内に存在できるのは有限個だけです。^[35]他の無限論理では、部分式は無限個の量化子のスコープ内に存在する場合があります。例えば、L _κ∞では、単一の全称量化子または存在量化子が、任意の数の変数を同時に束縛することができます。同様に、論理L _{κλ は}、λ 個未満の変数に対する同時量化、および κ 個未満のサイズの連言と選言を可能にします。

非古典論理と様相論理

直観主義的一階述語論理は、古典推論ではなく直観主義的推論を使用します。例えば、¬¬φ は φ と同値である必要はなく、¬ ∀x.φ は一般に ∃ x.¬φ と同値ではありません
第一階様相論理は、私たちが住むこの偶然的に真な世界だけでなく、他の可能世界を記述することを可能にします。いくつかのバージョンでは、可能世界の集合は、人がどの可能世界に住むかによって変化します。様相論理には、例えば「φが必然的である」（すべての可能世界で真）や「φが可能である」（ある可能世界で真）のように、非公式に特徴付けられる意味を持つ追加の様相演算子があります。標準的な第一階様相論理では、単一の定義域を持ち、各述語には一つの外延が割り当てられます。第一階様相論理では、各可能世界に独自の定義域を割り当てる定義域関数を持ち、各述語はこれらの可能世界に対してのみ外延を持ちます。これにより、例えばアレックスは哲学者だが、数学者だった可能性があり、そもそも存在しなかったかもしれないというケースをモデル化できます。最初の可能世界ではP ( a )は真であり、2番目の可能世界ではP ( a )は偽であり、3番目の可能世界では定義域にaが全く存在しません。
一階ファジー論理は、古典的な命題計算ではなく、命題ファジー論理の一階拡張です。

不動点論理

不動点論理は、正の演算子の最小不動点の下での閉包を追加することで、一階述語論理を拡張します。^[36]

高階論理

一階論理の特徴は、個体は量化できますが、述語は量化できないことです。したがって、

\exists a({\text{Phil}}(a))

は正当な一階論理式ですが、

\exists {\text{Phil}}({\text{Phil}}(a))

一階論理のほとんどの形式化ではそうではありません。二階論理は、後者の量化を追加することで一階論理を拡張します。他の高階論理では、二階論理よりもさらに高いタイプの量化が可能です。これらの高次のタイプには、関係間の関係、関係から関係間の関係への関数、およびその他の高次のオブジェクトが含まれます。したがって、一階論理における「最初の」は、量化できるオブジェクトのタイプを表します

一つの意味論のみが研究される一階論理とは異なり、二階論理には複数の意味論が考えられます。二階論理および高階論理で最も一般的に用いられる意味論は、完全意味論と呼ばれます。追加の量指定子とそれらの量指定子の完全意味論の組み合わせにより、高階論理は一階論理よりも強力になります。特に、二階論理および高階論理の（意味的）論理帰結関係は半決定可能ではありません。つまり、完全意味論の下で健全かつ完全な二階論理の有効な演繹体系は存在しません。

完全な意味論を持つ二階述語論理は、一階述語論理よりも表現力に優れています。例えば、二階述語論理では、自然数と実数直線を一意に特徴付ける公理系を作成できます。この表現力の代償として、二階述語論理および高階述語論理は、一階述語論理よりも魅力的なメタ論理的性質が少なくなります。例えば、一階述語論理のレーヴェンハイム・スコーレム定理とコンパクト性定理は、完全な意味論を持つ高階述語論理に一般化すると偽になります。

自動定理証明と形式手法

自動定理証明とは、数学定理の導出（形式的な証明）を探索して見つけるコンピュータプログラムの開発を指します。^[37]導出を見つけることは、探索空間が非常に大きくなる可能性があるため、困難な作業です。すべての可能な導出を網羅的に探索することは理論的には可能ですが、数学の多くの関心対象システムでは計算的に実行不可能です。そのため、ブラインドサーチよりも短時間で導出を見つけようとするために、複雑なヒューリスティック関数が開発されています。 ^[38]

関連分野の自動証明検証では、コンピュータプログラムを使用して、人間が作成した証明が正しいことを確認します。複雑な自動定理証明器とは異なり、検証システムは十分に小さいため、その正しさは手作業と自動ソフトウェア検証の両方で確認できます。この証明検証器の検証は、「正しい」とラベル付けされた導出が実際に正しいという確信を与えるために必要です

Metamathのような証明検証器の中には、完全な導出を入力として必要とするものもあります。Mizar や Isabelle のような証明検証器は、整然とした証明の概略（それでも非常に長く詳細な場合もある）を受け取り、簡単な証明検索や既知の決定手続きの適用によって不足部分を補います。そして、得られた導出は、小さなコア「カーネル」によって検証されます。このようなシステムの多くは、主に人間の数学者による対話的な利用を目的としており、これらは証明支援器として知られています。また、型理論など、一階述語論理よりも強力な形式論理を使用する場合もあります。一階述語演繹システムにおける非自明な結果の完全な導出は、人間が記述するには非常に長くなるため、^[39]結果は一連の補題として形式化されることが多く、それぞれの補題ごとに導出を個別に構築することができます。

自動定理証明器は、コンピュータサイエンスにおける形式検証の実装にも使用されます。この設定では、定理証明器は、プログラムやプロセッサなどのハードウェアの正しさを形式仕様に従って検証するために使用されます。このような分析は時間がかかり、したがって費用がかかるため、通常は誤動作が人的または経済的に重大な影響を与えるプロジェクトにのみ使用されます。

モデル検査の問題については、入力された有限構造が計算複雑度の境界に加えて、一階述語論理を満たすかどうかを判断する効率的なアルゴリズムが知られています。モデル検査 § 一階述語論理を参照してください。

参照

注釈

^ ホジソン、JPE、名誉教授（「第一階論理学」）、セントジョセフ大学、フィラデルフィア、1995年。
^ ヒューズ、GE、クレスウェル、MJ、『様相論理への新入門』（ロンドン：ラウトレッジ、1996年）、161ページ。
^ A. タルスキ、『決定不能理論』（1953年）、77ページ。『論理と数学の基礎研究』（ノースホランド）
^ メンデルソン、E.（1964年）。『数理論理学入門』、ヴァン・ノストランド・ラインホールド、56ページ
^ エリック・M・ハマー：「存在グラフの意味論」『哲学論理ジャーナル』第27巻第5号（1998年10月）、489ページ：「フレーゲとは独立に一階述語論理を展開し、冠頭とスコーレム正規形を予見する」
^ H. Friedman、「数学基礎の冒険 1：論理的推論」、ロスプログラム2022、講義ノート。2023年7月28日アクセス。
^ Goertzel, B.、Geisweiller, N.、Coelho, L.、Janičić, P.、Pennachin, C.、『実世界推論：スケーラブルで不確実な時空間、文脈、因果推論に向けて』（アムステルダム＆パリ：Atlantis Press、2011年）、29～30ページ
^ abcde WVO Quine , Mathematical Logic (1981). Harvard University Press , 0-674-55451-5.
^ Davis, Ernest (1990). Representations of Commonsense Knowledge . Morgan Kauffmann. pp. 27– 28 978-1-4832-0770-4.
^ 「述語論理 | Brilliant Math & Science Wiki」brilliant.org 。 2020年8月20日閲覧。
^ 「記号論理入門：講義2」cstl-cla.semo.edu 。2021年1月4日閲覧。「記号^{[永久リンク切れ]}
^ Hans Hermes (1973). Introduction to Mathematical Logic. Hochschultext (Springer-Verlag). London: Springer. ISBN 3540058192 . ISSN 1431-4657.
より正確には、1ソート1階述語論理の各変種には、等号の有無、関数の有無、命題変数の有無など、1つの言語しかありません
^ 「言語」という言葉は署名の同義語として使われることがありますが、「言語」は一連の式を指すこともあるため、混乱を招く可能性があります
^ Eberhard Bergmann and Helga Noll (1977). Mathematische Logik mit Informatik-Appendungen . Heidelberger Taschenbücher, Sammlung Informatik (in German). Vol. 187. Heidelberger: Springer. pp. 300–302
^ スマリヤン, R.M.、『一階述語論理』（ニューヨーク：ドーバー出版、1968年）、5ページ。
^ タケウティ, G.、『証明理論』（ガーデンシティ、ニューヨーク：ドーバー出版、2013年）、6ページ。
^ 「整形式の式」という用語を使用する著者の中には、「式」をアルファベットの記号の任意の文字列を意味するために使用する人もいます。しかし、数理論理学の著者のほとんどは、「式」を「整形式の式」の意味で使用し、整形式ではない式を表す用語を持っていません。あらゆる文脈において、興味深いのは整形式の式だけです。
^ yは規則4によって束縛されますが、どの原子部分式にも現れません。
^ この記号はKleeneによって導入されたようです。Doverの著書『Mathematical Logic』（John Wiley and Sons, 1967年）の2002年再版の脚注30を参照してください。 $\vDash$
^ F.R. Drake, Set theory: An introduction to large cardinals (1974年)
^ ロジャース, RL.、『数理論理と形式化理論：基本概念と結果の概説』（アムステルダム/ロンドン：ノースホランド出版、1971年）、39ページ。
^ Brink, C.、Kahl, W.、Schmidt, G.編著、『Relational Methods in Computer Science』（ベルリン／ハイデルベルク：Springer、1997年）、32～33ページ。
^ Anon., Mathematical Reviews ( Providence : American Mathematical Society , 2006), p. 803.
^ Shankar, N.、Owre, S.、Rushby, JM、Stringer-Calvert, DWJ著、『PVS Prover Guide 7.1』（メンロパーク：SRI International、2020年8月）。
^ Fitting, M.、『First-Order Logic and Automated Theorem Proving』（ベルリン／ハイデルベルク：Springer、1990年）、198～200ページ。
^ φ(z) がz = xである式置換を用いると、φ(x) は x=x となり、φ(y): y=x となるので、反射性を用いる。
^ φ(a) がa = zである式置換を用いて、 y = x → ( y = z → x = z )を得る。対称性と非カリー化を用いる
^ Hodel, RE, 『An Introduction to Mathematical Logic』（ニューヨーク州ミネオラ：ドーバー、1995年）、199ページ
^ Horrocks, Ian (2010). 「記述論理：言語とツールのための形式的基盤」（PDF）。スライド22。 2015年9月6日にオリジナルからアーカイブ（PDF）。
^ Gamut 1991, p. 75.
^ 左全体性は公理で、右一意性はで表現できます（等号記号が認められる場合）。どちらも定数置換（の場合）にも適用されます。 $\forall x_{1},...,x_{n}.\exists y.F(x_{1},...,x_{n},y)$ $\forall x_{1},...,x_{n},y,y'.$ $F(x_{1},...,x_{n},y)\land F(x_{1},...,x_{n},y')\rightarrow y=y'$ $n=0$
^ Uzquiano, Gabriel (2018年10月17日). 「量指定子と量化」。Zalta , Edward N. (編).スタンフォード哲学百科事典（2018年冬版）。特にセクション3.2「多ソート量化」を参照してください
^ Enderton, H. A Mathematical Introduction to Logic , second edition. Academic Press , 2001, pp.296–299.
^ 一部の著者は、 L _κωに有限個の自由変数を持つ式のみを許容し、より一般的にはL _κλにλ個未満の自由変数を持つ式のみを許容する。
^ ボッセ、ウーヴェ (1993). 「不動点論理と層別不動点論理のためのエーレンフォイヒト・フレッセゲーム」。Börger, Egon (編).コンピュータサイエンス論理：第6回ワークショップ、CSL'92、イタリア、サン・ミニアート、1992年9月28日～10月2日。選集。コンピュータサイエンス講義ノート。第702巻。シュプリンガー出版社。100 ～ 114ページ。ISBN 3-540-56992-8. Zbl 0808.03024.
^ Melvin Fitting (2012年12月6日). First-Order Logic and Automated Theorem Proving. Springer Science & Business Media. ISBN 978-1-4612-2360-3.
^ 「15-815 自動定理証明」www.cs.cmu.edu 。 2024年1月10日閲覧。
^ Avigad , et al. (2007) は、素数定理の証明を形式的に検証するプロセスについて議論しています。形式化された証明には、Isabelle証明検証器への約30,000行の入力が必要でした。

参考文献

ラウテンバーグ、ウォルフガング(2010)、『数理論理学の簡潔な入門（第3版）』、ニューヨーク、ニューヨーク州：シュプリンガー・サイエンス+ビジネス・メディア、doi :10.1007/978-1-4419-1221-3、ISBN 978-1-4419-1220-6
アンドリュース、ピーター・B. (2002); 『数理論理学と型理論入門：証明を通して真理へ』第2版、ベルリン：クルーワー・アカデミック・パブリッシャーズ。シュプリンガーから入手可能。
アビガッド、ジェレミー、ドネリー、ケビン、グレイ、ポール・ラフ (2007)、「素数定理の形式的に検証された証明」、ACM Transactions on Computational Logic、第9巻第1号doi :10.1145/1297658.1297660
バーワイズ、ジョン(1977)。「一階述語論理入門」。バーワイズ、ジョン（編）『数理論理ハンドブック　論理学と数学の基礎研究』。アムステルダム、オランダ：北ホラント（1982年出版）。ISBN 。.
モンク, J. ドナルド (1976). 数学論理学. ニューヨーク: Springer New York. doi :10.1007/978-1-4684-9452-5. ISBN Barwise, Jon; Etchemendy, John (2000); Language Proof and Logic . Stanford, CA: CSLI Publications (University of Chicago Press より頒布).
Bocheński, Józef Maria (2007); A Précis of Mathematical Logic . Dordrecht, NL: D. Reidel, Otto Birdによるフランス語版とドイツ語版からの翻訳
ボチェンスキ、ヨゼフ・マリア(2007); 『数理論理学の概説』, Dordrecht, NL: D. Reidel, translated from the French and German editions by Otto Bird
Gamut, LTF (1991)、『論理、言語、そして意味、第2巻：内包論理と論理文法』、イリノイ州シカゴ：シカゴ大学出版局、 ISBN
0-226-28088-8 ヒルベルト、デイヴィッド；アッカーマン、ヴィルヘルム(1950); 『数理論理学の原理』、チェルシー（『論理理論の基礎』、1928年ドイツ語初版の英訳）
ホッジス、ウィルフリッド（2001年）、「古典論理学 I：一階述語論理」、ゴブル、ルー（編）、『ブラックウェル哲学論理ガイド』、ブラックウェル
エビングハウス、ハインツ＝ディーター、フルム、イェルク、トーマス、ヴォルフガング（1994年）、『数学論理学、数学学部テキスト』、ベルリン、ドイツ／ニューヨーク、ニューヨーク州：
978-0-387-94258-2 タルスキ、アルフレッド、ギヴァント、スティーブン (1987); 変数なしの集合論の形式化。アメリカ数学会コロキウム出版第41巻、プロビデンス、ロードアイランド州：アメリカ数学会、 ISBN
「述語計算」、数学百科事典、EMSプレス、2001年 [1994] 978-0821810415

外部リンク

「述語計算」、数学百科事典、EMSプレス、2001年 [1994]
スタンフォード哲学百科事典（2000年）：シャピロ、S.、「古典論理学」。自然演繹様式の一階論理の統語論、モデル理論、メタ理論を網羅しています。
Magnus, PD; forall x: 形式論理入門。一階述語論理の形式意味論と証明理論を網羅している
メタマス：一階論理と公理的集合論ZFCを用いて、数学を巨大な一階理論として再構築する進行中のオンラインプロジェクト。プリンキピア・マテマティカの現代版。
ポドニエクス、カール；数理論理学入門
ケンブリッジ数学トリポスノート（ジョン・フレムリンによるタイプセット）。これらのノートは、通常3年生までに学部生に教えられた過去のケンブリッジ数学トリポスコースの一部を網羅しています。このコースは「論理、計算、集合論」と題され、順序数と基数、半集合とツォルンの補題、命題論理、述語論理、集合論、ZFCおよびその他の集合論に関連する一貫性の問題を扱っています。
ツリー証明生成器は、意味表法を用いて一階論理の式を検証または無効化できます。