一階論理

一階述語論理は、述語論理、述語計算、量化論理とも呼ばれ、数学、哲学、言語学、コンピュータサイエンスで使われる形式体系の集合です。一階述語論理は、非論理的オブジェクトに対して量化変数を使用し、変数を含む文の使用を許可します。「すべての人間は死ぬ」などの命題ではなく、一階述語論理では、「すべてのxに対して、xが人間であれば、xは死ぬ」という形式の表現を使用できます。ここで、「すべてのx に対して」は量化子、xは変数、「...は人間である」および「...は死ぬ」は述語です。^{[1]これは、量化子や}関係を使用しない命題論理と区別するものです。^[2]この意味で、命題論理は一階述語論理の基礎です。

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

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

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

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

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

命題論理は単純な宣言的命題を扱いますが、一階述語論理は述語と量化も扱います。述語は、談話領域内の 1 つまたは複数のエンティティに対して真または偽として評価されます。

「ソクラテスは哲学者である」と「プラトンは哲学者である」という2 つの文を考えてみましょう。命題論理では、これらの文自体が研究の個体と見なされ、たとえばpやqなどの変数で表されます。これらは、 などの述語を談話領域内の特定のオブジェクトに適用したものとは見なされず、真か偽かのいずれかである発話としてのみ見なされます。 ^[6]しかし、一階述語論理では、これらの 2 つの文は、特定の個体または非論理的オブジェクトが特性を持っているというステートメントとして組み立てられる場合があります。この例では、両方の文がたまたま何らかの個体 の共通の形式を持ち、最初の文では変数xの値は「ソクラテス」、2 番目の文では「プラトン」です。元の論理接続詞とともに非論理的個体について話すことができるため、一階述語論理には命題論理が含まれます。^[7]${\displaystyle {\text{isPhil}}}$${\displaystyle {\text{isPhil}}(x)}$${\displaystyle 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はフィリップという名前の男性」、またはその他の単項述語を意味すると解釈できます。 ${\displaystyle \land }$${\displaystyle \lor }$

論理記号は著者によって異なる文字のセットですが、通常は次のものが含まれます。^[10]

• 量指定子記号: ∀は全称量化、∃ は存在量化を表す
• 論理接続詞：連言は∧、選言は∨、含意は→、二条件は↔、否定は¬。著者の中には^[11] 、特に→が他の目的で使用されている文脈で、 →の代わりにC pqを、↔の代わりにE pqを使用する人もいます。さらに、馬蹄形⊃は→の代わりに使用できます。^[8]三重バー≡は↔の代わりに使用できます。チルダ( ~ )、N p、またはF pは¬の代わりに使用できます。二重バー、、^[12]またはA pqは∨の代わりに使用できます。特に技術的な理由でこれらの記号が使用できない場合は、アンパサンド&、K pq、または中点⋅は∧の代わりに使用できます。(前述の記号C pq、E pq、N p、A pq、およびK pqはポーランド記法で使用されます。)${\displaystyle \|}$${\displaystyle +}$
• 括弧、角括弧、その他の句読点記号。このような記号の選択はコンテキストによって異なります。
• 変数の無限集合。多くの場合、アルファベットの末尾の小文字x、y、z、... で表されます。変数を区別するために、下付き文字がよく使用されます: x ₀、x ₁、x ₂、... 。
• 等号記号（同一性記号と呼ばれることもある）=（下記の§ 等号とその公理を参照）。

第一階述語論理では、これらの記号のすべてが必要なわけではありません。否定、論理積 (または論理和)、変数、括弧、等号のいずれか 1 つがあれば十分です。

その他の論理シンボルには次のものがあります。

• 真理定数: 「真」の場合は T、V、または⊤、「偽」の場合は F、O、または⊥ (V と O はポーランド記法による)。価数 0 のこのような論理演算子がない場合、これら 2 つの定数は量指定子を使用してのみ表現できます。
• シェファーストローク、D pq (NAND)、排他的論理和、J pqなどの追加の論理接続子。

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

• n ≥ 0 のあらゆる整数に対して、 n項またはn位の述語記号 の集合が存在します。これらはn個の要素間の関係を表すため、関係記号とも呼ばれます。各項 n に対して、それらは無限に存在します。

  Pn0、Pn1、Pn2、Pn3、_...^​_​^​_​^​_​^​

• あらゆる整数n ≥ 0に対して、 n項関数の記号は 無限に存在する。

  fn ₀、fn ₁、fn ₂、fn ³、_...^​​​

述語記号または関数記号のアリティが文脈から明らかな場合、上付き文字nは省略されることが多いです。

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

最近では、想定しているアプリケーションに応じて異なる非論理シンボルを使用するという慣例があります。そのため、特定のアプリケーションで使用されるすべての非論理シンボルのセットに名前を付けることが必要になりました。この選択は署名によって行われます。^[14]

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

シグネチャは、場合によっては非論理シンボルの解釈方法を示すことがありますが、シグネチャ内の非論理シンボルの解釈は別個のものであり、必ずしも固定されているわけではありません。シグネチャは、セマンティクスではなく構文に関係します。

このアプローチでは、すべての非論理シンボルは次のいずれかのタイプになります。

• 0 以上の価数 (または引数の数) を持つ述語記号 (または関係記号)。これらは、P 、 Q 、Rなどの大文字で表されることが多いです。例:
  • P ( x )において、 Pは原子価1の述語記号です。考えられる解釈の1つは「xは男性である」です。
  • Q ( x , y )において、 Qは原子価2の述語記号です。考えられる解釈としては、「x はyより大きい」や「xはyの父である」などがあります。
  • 価数 0 の関係は、任意のステートメントを表すことができる命題変数と同一視できます。 Rの 1 つの解釈は、「ソクラテスは人間である」です。
• 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]

1. 変数。任意の変数シンボルは項です。
2. 関数。f が n 項関数記号で、t 1 、...、t n が項である場合、f ( t 1 _、 ... 、_t n )は項_です。特に_、個々の定数を表す記号は 0 項関数記号であるため、項です。

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

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

1. 述語記号。Pがn項述語記号で、 t ₁、...、t _{n が}項である場合、P ( t ₁、...、t _n ) は式です。
2. 等式。等号記号が論理の一部とみなされ、 t ₁とt ₂が項である場合、 t ₁ = t ₂は式です。
3. 否定。 が式であれば、 は式です。${\displaystyle \varphi }$${\displaystyle \lnot \varphi }$
4. 二項接続詞。⁠ ⁠${\displaystyle \varphi }$と⁠ ⁠ が${\displaystyle \psi }$式である場合、 ( ) は式です。同様の規則が他の二項論理接続詞にも適用されます。${\displaystyle \varphi \rightarrow \psi }$
5. 量指定子。 が式でx が変数である場合、(すべての x に対して、が成り立つ) および( となる x が存在する) は式です。${\displaystyle \varphi }$${\displaystyle \forall x\varphi }$${\displaystyle \varphi }$${\displaystyle \exists x\varphi }$${\displaystyle \varphi }$

規則 1 から 5 を有限回適用して得られる式だけが式です。最初の 2 つの規則から得られる式は原子式と呼ばれます。

例えば：

${\displaystyle \forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))}$

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

定義における括弧の役割は、任意の式が 1 つの方法、つまり帰納的定義に従うことによってのみ得られる (つまり、各式に一意の解析ツリーが存在する) ことを保証することです。この特性は、式の一意の可読性として知られています。式で括弧が使用される場所については、多くの規則があります。たとえば、著者によっては、括弧の代わりにコロンや句点を使用したり、括弧が挿入される場所を変更したりします。各著者の特定の定義には、一意の可読性の証明が添付されている必要があります。

利便性のため、論理演算子の優先順位に関する規則が開発され、場合によっては括弧を記述する必要がなくなりました。これらの規則は算術演算の順序に似ています。一般的な規則は次のとおりです。

• ${\displaystyle \lnot }$最初に評価される
• ${\displaystyle \land }$そして次に評価される${\displaystyle \lor }$
• 量指定子は次に評価される
• ${\displaystyle \to }$最後に評価されます。

さらに、数式を読みやすくするために、定義で必要のない追加の句読点が挿入されることもあります。つまり、次の数式になります。

${\displaystyle \lnot \forall xP(x)\to \exists x\lnot P(x)}$

次のように記述されます。

${\displaystyle (\lnot [\forall xP(x)])\to \exists x[\lnot P(x)].}$

一部の分野では、2 項関係や関数に、上で定義した接頭表記法ではなく、中置表記法を使用するのが一般的です。たとえば、算術では、通常、「=(+(2,2),4)」ではなく、「2 + 2 = 4」と書きます。中置表記法の式は、対応する接頭表記法の式の省略形とみなすのが一般的です。用語構造と表現も参照してください。

上記の定義では、 などの二項接続詞に中置記法を使用しています。あまり一般的ではない慣習として、 、などを引数の間ではなく引数の前に書くポーランド記法があります。この慣習の利点は、句読点記号をすべて省略できることです。このように、ポーランド記法は簡潔で簡潔ですが、人間が読みにくいため、実際にはほとんど使用されません。ポーランド記法では、式: ${\displaystyle \to }$${\displaystyle \rightarrow }$${\displaystyle \wedge }$

${\displaystyle \forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))}$

「∀x∀y→Pfx¬→ PxQfyxz」になります。

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

直感的には、変数記号は、それがどの時点でも量化されていない場合、式の中で自由である：^{[8] pp.142--143} ∀ y P ( x , y )では、変数xの唯一の出現は自由であるが、yの唯一の出現は束縛されている。式中の自由変数と束縛変数の出現は、次のように帰納的に定義される。

原子式

φ が原子式である場合、 x がφ内で自由に出現するのは、 x がφ内で出現する場合のみです。さらに、どの原子式にも束縛変数は存在しません。

否定

x が¬ φで自由に出現するのは、x がφで自由に出現する場合に限ります。x が¬ φで拘束されて出現するのは、 x がφで拘束されて出現する場合に限ります。

二項接続詞

x が( φ → ψ )で自由に出現するのは、xがφまたはψのいずれかで自由に出現する場合に限ります。 x が ( φ → ψ ) で拘束されて出現するのは、 xがφ または ψ のいずれかで拘束されて出現する場合に限ります。→ の代わりに他の任意の二項接続詞にも同じ規則が適用されます。

数量詞

x が∀ y φに自由に現れるのは、 x がφに自由に現れ、かつxがyとは異なる記号である場合に限ります。また、x が∀ y φに束縛されて現れるのは、xがyであるか、x がφに束縛されて現れる場合に限ります。 ∃を∀の代わりに使用しても同じ規則が当てはまります。

例えば、∀ x ∀ y ( P ( x ) → Q ( x , f ( x ), z ))では、xとy は結合した状態でのみ出現し、^[19] z は自由状態の場合にのみ出現し、w は式中に出現しないためどちらでもありません。

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

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

数学では、順序付きアーベル群の言語には、定数記号 0 が 1 つ、単項関数記号 - が 1 つ、2 項関数記号 + が 1 つ、2 項関係記号 ≤ が 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 があります。${\displaystyle (\forall x\forall y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \forall x\,\forall y\,\mathop {+} (x,y)=0)]}$${\displaystyle \forall x\forall y(x+y\leq z)\to \forall x\forall y(x+y=0).}$

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

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

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

談話領域D は、何らかの「オブジェクト」の空でない集合です。直感的には、解釈が与えられた場合、一階述語式はこれらのオブジェクトに関するステートメントになります。たとえば、は、述語Pが真である(または、より正確には、解釈によって述語記号Pに割り当てられた述語が真である) オブジェクトがD内に存在することを述べています。たとえば、D を整数の集合とすることができます。 ${\displaystyle \exists xP(x)}$

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

• n 項関数記号の解釈は、 D ⁿからDへの関数です。たとえば、議論のドメインが整数の集合である場合、引数が 2 の関数記号f は、その引数の合計を与える関数として解釈できます。言い換えると、記号f は、この解釈では加算である関数⁠ ⁠に関連付けられています。${\displaystyle I(f)}$

• 定数シンボル（引数が 0 の関数シンボル）の解釈は、D ^{0 （メンバーが空の}タプルのみである集合）からDへの関数であり、これはD内のオブジェクトと簡単に識別できます。たとえば、解釈によって定数シンボル に値を割り当てることができます。${\displaystyle I(c)=10}$${\displaystyle c}$

• n項述語記号の解釈は、 Dのn組の要素の集合であり、述語が真となる引数を示します。たとえば、2 項述語記号Pの解釈は、最初の引数が 2 番目の引数より小さい整数のペアの集合である場合があります。この解釈によると、述語P は、最初の引数が 2 番目の引数より小さい場合に真になります。同様に、述語記号には、 D ⁿからまでのブール値関数を割り当てることができます。${\displaystyle I(P)}$${\displaystyle \{\mathrm {true,false} \}}$

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

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

• 変数。各変数xはμ ( x )と評価される。
• 関数。談話領域の要素に評価された項とn項関数記号fが与えられると、項は に評価されます。${\displaystyle t_{1},\ldots ,t_{n}}$${\displaystyle d_{1},\ldots ,d_{n}}$${\displaystyle f(t_{1},\ldots ,t_{n})}$${\displaystyle (I(f))(d_{1},\ldots ,d_{n})}$

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

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

式に自由変数が含まれず、文にも自由変数が含まれない場合、最初の変数割り当ては真理値に影響しません。言い換えると、文がMに従って真であるのは、 Mと他のすべての変数割り当てに従って真である場合のみです。 ${\displaystyle \mu }$${\displaystyle \mu '}$

変数割り当て関数に頼らない真理値の定義方法には、2 つ目の一般的な方法があります。代わりに、解釈Mが与えられた場合、まずシグネチャに定数記号のコレクションを追加します。定数記号は、 M内の論議領域の各要素に 1 つずつあります。つまり、領域内の各dに対して定数記号c _dが固定されているとします。解釈は拡張され、新しい定数記号はそれぞれ、領域の対応する要素に割り当てられます。次に、量化式の真理を構文的に次のように定義します。

• 存在量指定子（代替） 。M によれば、論理式が真となるのは、論理ドメインにdが存在し、 が成り立つ場合です。以下は、 φ におけるxの自由な出現ごとにc _{d を}代入した結果です 。${\displaystyle \exists x\varphi (x)}$${\displaystyle \varphi (c_{d})}$${\displaystyle \varphi (c_{d})}$
• 全称量指定子（代替）。ある式がMに従って真であるとは、談話領域内のすべてのdに対して、 Mに従って真であることを意味する。${\displaystyle \forall x\varphi (x)}$${\displaystyle \varphi (c_{d})}$

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

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

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

論理式が論理的に有効（または単に有効）であるとは、あらゆる解釈において真である場合を言う。^[22]これらの論理式は、命題論理における トートロジーと同様の役割を果たす。

式 φ が式 ψ の論理的帰結であるとは、 ψ を真とするすべての解釈が φ も真とすることである。この場合、 φ は ψ によって論理的に導かれると言う。

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

• 円筒代数、アルフレッド・タルスキとその同僚著
• ポリアディック代数、 Paul Halmos著;
• 述語関数論理。主にウィラード・クワインに由来。

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

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

特定のシグネチャの1 階理論は、そのシグネチャのシンボルで構成される文である公理の集合です。公理の集合は有限または再帰的に列挙可能であることが多く、その場合、理論は有効と呼ばれます。著者によっては、理論には公理のすべての論理的帰結も含まれることを要求します。公理は理論の範囲内で成立すると考えられ、そこから理論の範囲内で成立する他の文を導き出すことができます。

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

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

理論は、理論の公理から矛盾を証明できない場合に、一貫性があります。理論が完全であるのは、そのシグネチャ内のすべての式について、その式またはその否定が理論の公理の論理的帰結である場合です。ゲーデルの不完全性定理は、自然数理論の十分な部分を含む有効な第 1 階理論が、一貫性と完全性の両方を持つことは決してないことを示しています。

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

ただし、空のドメインにはいくつかの問題があります。

• 多くの一般的な推論規則は、論議領域が空でないことが要求される場合にのみ有効です。 1 つの例は、x が内の自由変数でない場合にが成立するという規則です。 式を冠頭正規形にするために使用されるこの規則は、空でない領域では有効ですが、空領域が許される場合は無効です。${\displaystyle \varphi \lor \exists x\psi }$${\displaystyle \exists x(\varphi \lor \psi )}$${\displaystyle \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に置き換えるには、まず φ のバインド変数をtの自由変数と異なるように変更する必要があります。)

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

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

ヒルベルトスタイルの演繹システムにおける演繹は、各式が論理公理である式のリストです。論理公理は、現在の導出に対して仮定されている仮説、または推論規則を介して前の式から導かれる仮説です。論理公理は、論理的に有効な式の公理スキーマから構成され、かなりの量の命題論理を網羅しています。推論規則により、量指定子の操作が可能になります。典型的なヒルベルトスタイルのシステムには、少数の推論規則と、論理公理の無限スキーマがいくつかあります。推論規則としては 、モダスポネンスと普遍一般化のみを持つことが一般的です。

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

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

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

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

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

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

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

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

${\displaystyle \lnot \forall x\,P(x)\Leftrightarrow \exists x\,\lnot P(x)}$

${\displaystyle \lnot \exists x\,P(x)\Leftrightarrow \forall x\,\lnot P(x)}$

${\displaystyle \forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)}$

${\displaystyle \exists x\,\exists y\,P(x,y)\Leftrightarrow \exists y\,\exists x\,P(x,y)}$

${\displaystyle \forall x\,P(x)\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\land Q(x))}$

${\displaystyle \exists x\,P(x)\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P(x)\lor Q(x))}$

${\displaystyle P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))}$（ここでは、自由に出現してはならない）${\displaystyle x}$${\displaystyle P}$

${\displaystyle P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))}$（ここでは、自由に出現してはならない）${\displaystyle x}$${\displaystyle P}$

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

• 反射性。各変数xについて、x = xです。
• 関数の代入。すべての変数xとy、および任意の関数記号fについて、

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

• 式の代入。任意の変数xとyおよび任意の式 φ( z ) について、 φ 内の任意の数のxの自由出現をyで置き換えて φ' が得られ、これらがyの自由出現のままである場合、次のようになります。

  x = y → (φ → φ')。

これらは公理スキーマであり、それぞれが無限の公理セットを指定します。3 番目のスキーマは、ライプニッツの法則、「代替性の原理」、「同一物の識別不能性」、または「置換特性」として知られています。関数シンボル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。[ ^27]
• 推移性。x = yかつy = zならばx = zである。^[28]

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

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

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

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

いくつかの理論では、平等の 他のアドホックな定義が認められています。

• 1 つの関係記号 ≤ を持つ半順序理論では、 s = t をs ≤ t t ≤ sの略記として定義できます。${\displaystyle \wedge }$
• 関係 ∈ が 1 つだけの集合論では、s = t を∀ x ( s ∈ x ↔ t ∈ x ) ∀ x ( x ∈ s ↔ x ∈ t )${\displaystyle \wedge }$の省略形として定義できます。この等式の定義は、等式の公理を自動的に満たします。この場合、と表現できる通常の外延性公理 を、集合xとy が同じ要素を持つ場合、それらは同じ集合にも属するという別の定式 に置き換える必要があります。${\displaystyle \forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y]}$${\displaystyle \forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)]}$

高階論理ではなく一階論理を使用する理由の 1 つは、一階論理にはより強い論理にはないメタ論理的性質が多数あることです。これらの結果は、個々の理論の性質ではなく、一階論理自体の一般的な性質に関するものです。これらは、一階理論のモデルを構築するための基本的なツールを提供します。

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

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

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

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

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

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

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

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

ペル・リンドストロームは、今述べたメタ論理的性質は、より強い論理がそれらの性質を同時に持つことはできないという意味で、実際には第一階論理を特徴づけるものであることを示した (エビングハウスとフラム 1994、第 13 章)。リンドストロームは、抽象論理システムのクラスと、このクラスのメンバーの相対的な強さの厳密な定義を定義した。彼は、このタイプのシステムについて 2 つの定理を確立した。

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

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

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

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

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

それでも、自然言語には一階述語論理では表現できない複雑な特徴がある。「自然言語の分析のための手段として適切な論理体系は、一階述語論理よりもはるかに豊かな構造を必要とする」^{[31] 。}

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

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

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

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

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

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

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

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

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

${\displaystyle \exists x(P_{1}(x)\land \varphi (x))}$。

第一階論理に追加の量指定子を追加できます。

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

無限論理では、無限に長い文が許されます。たとえば、無限の数式の論理積や論理和、あるいは無限の数の変数の量化などが許されます。無限に長い文は、位相幾何学やモデル理論などの数学の分野で発生します。

無限論理は、一階論理を一般化して、無限長の式を可能にします。式が無限になる最も一般的な方法は、無限の連言と選言です。ただし、関数と関係のシンボルが無限の引数を持つことができる、または量指定子が無限の数の変数をバインドできる一般化されたシグネチャを認めることもできます。無限の式は有限の文字列で表すことができないため、式の別の表現を選択する必要があります。このコンテキストでの通常の表現はツリーです。したがって、式は、本質的に、解析される文字列ではなく、その解析ツリーで識別されます。

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

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

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

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

一階述語論理の特徴は、個体は量化できるが述語は量化できないことである。

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

は正当な一階式であるが、

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

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

1 つの意味論のみが研究される 1 階論理とは異なり、2 階論理には複数の意味論が考えられます。2 階論理および高階論理で最も一般的に使用される意味論は、完全意味論として知られています。追加の量指定子とこれらの量指定子の完全意味論の組み合わせにより、高階論理は 1 階論理よりも強力になります。特に、2 階論理および高階論理の (意味論的) 論理的帰結関係は半決定可能ではありません。つまり、完全意味論のもとで健全かつ完全な 2 階論理の有効な演繹システムは存在しません。

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

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

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

Metamathなどの証明検証器は、完全な導出を入力として要求します。MizarやIsabelleなどの他の証明検証器は、適切にフォーマットされた証明スケッチ (それでも非常に長く詳細な場合があります) を受け取り、簡単な証明検索を行うか、既知の決定手順を適用することで、不足している部分を埋めます。結果として得られる導出は、小さなコア「カーネル」によって検証されます。このようなシステムの多くは、主に人間の数学者による対話型の使用を目的としており、証明アシスタントとして知られています。また、型理論などの一階述語論理よりも強力な形式論理を使用する場合もあります。一階演繹システムにおける非自明な結果の完全な導出は、人間が記述するには非常に長くなるため、^[39]結果は一連の補題として形式化されることが多く、それらの補題に対して個別に導出を構築できます。

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

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

• ラウテンバーグ、ヴォルフガング（2010）、A Concise Introduction to Mathematical Logic（第3版）、ニューヨーク、NY：Springer Science+Business Media、doi：10.1007/978-1-4419-1221-3、ISBN 978-1-4419-1220-6
• アンドリュース、ピーター B. (2002);数理論理学と型理論入門：証明を通して真実へ、第 2 版、ベルリン：Kluwer Academic Publishers。Springer から入手可能。
• Avigad, Jeremy、Donnelly, Kevin、Gray, David、Raff, Paul (2007)、「素数定理の形式的に検証された証明」、ACM Transactions on Computational Logic、vol. 9 no. 1 doi :10.1145/1297658.1297660
• バーワイズ、ジョン(1977)。「一階述語論理入門」。バーワイズ、ジョン (編)。数理論理学ハンドブック。論理学と数学の基礎研究。アムステルダム、オランダ: 北ホラント (1982 年出版) 。ISBN 978-0-444-86388-1。
• モンク、J.ドナルド（1976）。数学論理学。ニューヨーク、NY：Springer New York。doi ：10.1007 / 978-1-4684-9452-5。ISBN 978-1-4684-9454-9。
• バーワイズ、ジョン、エチェメンディ、ジョン(2000); Language Proof and Logic、スタンフォード、カリフォルニア州: CSLI Publications (シカゴ大学出版局より配布)
• ボチェンスキ、ヨゼフ・マリア（2007年）『数学論理学の概説』、ドルドレヒト、オランダ：D. ライデル、フランス語版とドイツ語版からオットー・バードが翻訳
• フェレイロス、ホセ (2001); 現代論理への道 - 解釈、Bulletin of Symbolic Logic、第 7 巻、第 4 号、2001 年、pp. 441–484、doi :10.2307/2687794、JSTOR  2687794
• Gamut, LTF (1991)、「論理、言語、意味、第2巻：内包論理と論理文法」、シカゴ、イリノイ州：シカゴ大学出版局、ISBN 0-226-28088-8
• デヴィッド・ヒルベルト;およびアッカーマン、ヴィルヘルム(1950)。Principles of Mathematical Logic 、Chelsea ( Grundzüge der theoretischen Logikの英語翻訳、1928 年ドイツ語初版)
• ホッジス、ウィルフリッド（2001）、「古典論理学 I：第一階述語論理」、ゴブル、ルー（編）、「ブラックウェル哲学論理ガイド」、ブラックウェル
• エビングハウス、ハインツ・ディーター;フルム、ヨルグ。およびトーマス、ヴォルフガング (1994)。数学的論理学、数学の学部テキスト、ベルリン、デラウェア州/ニューヨーク州ニューヨーク: Springer-Verlag、第 2 版、ISBN 978-0-387-94258-2 
• Tarski, Alfred および Givant, Steven (1987);変数​​なしの集合論の形式化。アメリカ数学会コロキウム出版第 41 巻、プロビデンス RI: アメリカ数学会、ISBN 978-0821810415 

• 「述語計算」、数学百科事典、EMS Press、2001 [1994]
• スタンフォード哲学百科事典: シャピロ、スチュワート、「古典論理」。自然演繹スタイルの一階論理の構文、モデル理論、およびメタ理論をカバーしています。
• Magnus, PD; forall x: 形式論理入門。一階述語論理の形式意味論と証明理論をカバーしています。
• Metamath: 一階述語論理と公理的集合論 ZFC を使用して、数学を巨大な一階述語理論として再構築する進行中のオンライン プロジェクト。Principia Mathematicaが現代化されました。
• ポドニエクス、カール;数理論理学入門
• Cambridge Mathematical Tripos ノート (John Fremlin によるタイプセット)。これらのノートは、通常 3 年目までの学部生に教えられた過去のCambridge Mathematical Triposコースの一部をカバーしています。このコースは「論理、計算、集合論」と題されており、序数と基数、Poset と Zorn の補題、命題論理、述語論理、集合論、ZFC およびその他の集合論に関連する一貫性の問題をカバーしています。
• Tree Proof Generator は、セマンティック タブローメソッドを使用して、一階述語論理の式を検証または無効化できます。