一階述語論理

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

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

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

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

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

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

はじめに

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

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

論理記号

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

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

一階述語論理では、これらの記号のすべてが必須というわけではありません。量指定子のいずれか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]項と式が記号列として表現される場合、これらの規則を用いて項と式の形式文法を記述することができる。これらの規則は一般に文脈自由（各生成規則の左側に単一の記号が存在）であるが、記号の集合が無限大であってもよく、また項の場合の変数のように開始記号が複数存在してもよいという点が異なる。

用語

用語の集合は、以下の規則によって帰納的に定義される。^[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 )は式です。
   • 等式。等号が論理の一部とみなされ、 t ₁とt _{2 が}項である場合、 t ₁ = t ₂は式です。
2. 否定。 が式であれば、 も式です。${\displaystyle \varphi }$ ${\displaystyle \lnot \varphi }$
3. 二項接続詞。⁠ ⁠ と ⁠ ⁠ が式である場合、${\displaystyle \varphi }$ ( )も式${\displaystyle \psi }$ です。同様の規則が他の二項論理接続詞にも適用されます。${\displaystyle \varphi \rightarrow \psi }$
4. 量指定子。 が式でx が変数である場合、(すべての x に対して、が成り立つ) および( となる x が存在する) は式です。${\displaystyle \varphi }$ ${\displaystyle \forall x\varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \exists x\varphi }$ ${\displaystyle \varphi }$

規則1～4を有限回適用して得られる式のみが式である。最初の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 }$

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

表記規則

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

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

さらに、数式を読みやすくするために、定義に必要のない句読点が挿入されることもあります。例えば、次の式は次のようになります。

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

次のように記述されるかもしれません:

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

自由変数と束縛変数

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

直感的に言えば、変数記号は式の中で自由変数とは、いかなる点においても量化されていない変数である。[ 8 ^] pp ^. 142–143 ...

原子式

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

否定

x が¬ φに自由出現する場合、かつその場合においてx がφに自由出現する。xが¬ φに束縛出現する場合、かつその場合においてx がφに束縛出現する

二項接続詞

x が( φ → ψ )において自由出現する場合、かつその場合において、x がφまたはψのいずれかにおいて自由出現する。xが( φ → ψ )において束縛出現する場合、かつその場合において、x がφまたはψのいずれかにおいて束縛出現する。→ の代わりに他の二項接続詞を用いる場合も同様の規則が適用される

量指定子

x がϕに 自由出現する場合、 x がϕに自由出現し、かつxがyとは異なる記号である場合に限ります。また、x がϕ に束縛出現する場合、 xがyであるか、またはx がϕに束縛出現する場合に限ります。 ∃ を ϕ の代わりに用いた場合も同様の規則が適用されます。

例えば、∀ x（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つずつあります。したがって、

• +( 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組の要素の集合であり、述語が真となる引数を与える。例えば、二項述語記号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の値の1倍の差しかない変数割り当てとの組み合わせすべてにおいてφ(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つあります

• 円筒代数、Alfred Tarskiらによる。
• ポリアディック代数、Paul Halmos著;
• 述語関数論理、主にウィラード・クワインが提唱。

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

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

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

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

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

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

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

空ドメイン

上記の定義では、あらゆる解釈の議論領域は空でないことが必要である。包含論理のように、空の領域が許容される設定もある。さらに、代数構造のクラスに空の構造が含まれる場合（例えば、空のposetが存在する場合）、そのクラスは、空の領域が許容されるか、クラスから空の構造が除去される場合にのみ、一階述語論理の基本クラスとなり得る。

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

• 多くの一般的な推論規則は、議論領域が空でないことが要求される場合にのみ有効です。一例として、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)}$

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

ヒルベルト型システムと自然演繹

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

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

シークエント計算

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

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

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

タブロー法

命題論理式((a ∨ ¬b) ∧ b) → a のタブロー証明

先ほど説明した方法とは異なり、タブロー法における導出は式のリストではありません。導出は式のツリーです。式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を持つ 任意の式φ( z )について、次の式が成り立ちます。

  x = 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 ) ...​${\displaystyle \wedge }$ ​​​​​​​​​${\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)]}$

金属学的特性

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

完全性と決定不能性

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

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

完全な一階述語論理よりも弱い体系があり、その論理的帰結関係は決定可能である。これには、命題論理や、一項述語記号のみに制限され関数記号を含まない一階述語論理などが含まれる。関数記号を含まない決定可能な他の論理としては、一階述語論理の保護部分や二変数論理などがある。一階述語論理式のベルネイス・シェーンフィンケルクラスも決定可能である。一階述語論理の決定可能な部分集合は、記述論理の枠組みでも研究されている。

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

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

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

コンパクト性定理

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

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

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

リンドストロームの定理

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

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

限界

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

例えば、一階述語論理は決定不可能であり、つまり、証明可能性のための健全で完全かつ停止性のある決定アルゴリズムは不可能である。このため、C ₂ : 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 のみ、または Sheffer ストローク (NAND) 演算子または Peirce 矢印 (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))}$ 。

を満たす元は第一種、を満たす元は第二種と考えられます。対応する述語記号を用いて量化の範囲を制限することで、各種について量化を行うことができます。例えば、式 を満たす第一種元が存在すると述べるには、次のように書きます。 ${\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.¬φ と同等ではありません。
• 第一階様相論理は、私たちが住むこの偶然的に真な世界だけでなく、他の可能世界を記述することを可能にします。いくつかのバージョンでは、可能世界の集合は、人がどの可能世界に住むかによって変化します。様相論理には、例えば「φが必然的である」（すべての可能世界で真）や「φが可能である」（ある可能世界で真）のように、非公式に特徴付けられる意味を持つ追加の様相演算子があります。標準的な第一階様相論理では、単一の定義域を持ち、各述語には一つの外延が割り当てられます。第一階様相論理では、各可能世界に独自の定義域を割り当てる定義域関数を持ち、各述語はこれらの可能世界に対してのみ外延を持ちます。これにより、例えばアレックスは哲学者だが、数学者だった可能性があり、そもそも存在しなかったかもしれないというケースをモデル化できます。最初の可能世界ではP ( a )は真であり、2番目の可能世界ではP ( a )は偽であり、3番目の可能世界では定義域にaが全く存在しません。
• 一次ファジー論理は、古典的な命題計算ではなく、命題ファジー論理の一次拡張です。

固定小数点論理

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

高階論理

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

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

は正当な一階式だが、

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

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

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

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

自動定理証明と形式手法

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

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

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

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

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

参照

• 哲学ポータル

• ACL2 — アプリケーション型Common Lispの計算ロジック
• アリストテレス論理
• 等矛盾性
• エーレンフォイヒト＝フライスゲーム
• 定義による拡張
• 拡張（述語論理）
• ハーブ化
• 論理記号一覧

• ロジバン
• レーヴェンハイム数
• 非第一順序化可能性
• 冠頭正規形
• 事前分析
• Prolog
• 関係代数
• 関係モデル
• スコーレム正規形
• タルスキの世界
• 真理値表
• 型（モデル理論）

注釈

1. セントジョセフ大学名誉教授（「第一階論理学」）、フィラデルフィア、1995年。
2. Hughes, GE、Cresswell, MJ、「A New Introduction to Modal Logic」（ロンドン：Routledge、1996年）、p.161。
3. A. Tarski, Undecidable Theories (1953), p. 77. 論理学と数学の基礎研究、北ホラント
4. メンデルソン, E. (1964).数理論理学入門.ヴァン・ノストランド・ラインホールド. p. 56.
5. エリック・M・ハマー「存在グラフの意味論」『哲学論理ジャーナル』第27巻第5号（1998年10月）、489ページ：「フレーゲとは独立して一階述語論理を展開し、冠頭とスコーレム正規形を予見する」
6. H. Friedman、「数学基礎の冒険1：論理的推論」、ロスプログラム2022、講義ノート。2023年7月28日にアクセス。
7. Goertzel, B.、Geisweiller, N. 、Coelho, L. 、Janičić, P. 、および Pennachin, C.、「Real-World Reasoning: Toward Scalable, Uncertain Spatiotemporal, Contextual and Causal Inference」（アムステルダム＆パリ：Atlantis Press、2011年）、pp. 29–30。
8. WVO Quine , Mathematical Logic (1981). Harvard University Press , 0-674-55451-5.
9. デイヴィス、アーネスト (1990). 『常識的知識の表象』 モーガン・カウフマン. pp.  27– 28. ISBN 978-1-4832-0770-4。
10. 「述語論理 | Brilliant Math & Science Wiki」brilliant.org . 2020年8月20日閲覧。
11. 「記号論理学入門：講義2」cstl-cla.semo.edu . 2021年4月15日時点のオリジナルよりアーカイブ。 2021年1月4日閲覧。
12. ハンス・ヘルメス(1973). 『数理論理学入門』 Hochschultext (Springer-Verlag). ロンドン: Springer. ISBN 3540058192. ISSN  1431-4657.
13. より正確には、1ソート一階述語論理の各変種には、等号の有無、関数の有無、命題変数の有無など、1つの言語しかありません
14. 言語という単語は署名の同義語として使用されることもありますが、「言語」は数式の集合を指すこともあるため、混乱を招く可能性があります。
15. エバーハルト・バーグマンとヘルガ・ノル (1977)。Informatik-Anwendungen による数学論理。 Heidelberger Taschenbücher、Sammlung Informatik (ドイツ語)。 Vol. 187. ハイデルベルク：シュプリンガー。 300–302ページ。
16. Smullyan, RM、「第一階論理」（ニューヨーク：ドーバー出版、1968年）、5ページ。
17. Takeuti, G. , Proof Theory ( Garden City, NY : Dover Publications , 2013), p. 6.
18. 「整形式式」という用語を使用する著者の中には、「式」をアルファベットの任意の記号列を指すために使用する人もいます。しかし、数理論理学のほとんどの著者は「式」を「整形式式」の意味で使用し、整形式ではない式を表す用語は存在しません。あらゆる文脈において、重要なのは整形式式のみです。
19. yは規則4によって制限されるが、どの原子部分式にも現れない。
20. この記号はクリーネによって導入されたようです。ドーバーが 2002 年に再版した著書『数学論理学』（John Wiley and Sons、1967 年）の脚注 30 を参照してください。${\displaystyle \vDash }$
21. FRドレイク『集合論：大規模基数入門』（1974年）
22. Rogers, RL, Mathematical Logic and Formalized Theories: A Survey of Basic Concepts and Results (Amsterdam/London: North-Holland Publishing Company , 1971), p. 39.
23. Brink, C.、Kahl, W.、およびSchmidt, G.編、コンピュータ サイエンスにおけるリレーショナル メソッド(ベルリン/ハイデルベルク: Springer、1997)、32–33 ページ。
24. 匿名、数学レビュー（プロビデンス：アメリカ数学会、2006年）、803ページ。
25. Shankar, N.、Owre, S.、Rushby, JM、Stringer-Calvert, DWJ、「PVS Prover Guide 7.1」（メンロパーク：SRI International、2020年8月）。
26. フィッティング、M.、「第一階論理と自動定理証明」（ベルリン/ハイデルベルク：シュプリンガー、1990年）、pp.198-200。
27. φ(z) がz = xである式置換を使用すると、 φ(x) は x=x となり、 φ(y): y=x となるので、反射性を使用します。
28. φ(a) をa = zとして式を置換し、 y = x → ( y = z → x = z )を取得し、対称性と非カリー化を使用します。
29. Hodel, RE,数学論理入門( Mineola NY : Dover , 1995)、199ページ。
30. Horrocks, Ian (2010). 「記述論理：言語とツールのための形式的基盤」（PDF） . スライド22. 2015年9月6日時点のオリジナルよりアーカイブ（PDF） .
31. ガマット1991、75ページ。
32. 左全体性は公理 で表現でき、右一意性は で表現できる（ただし等号記号が許される）。どちらも定数置換にも適用される（ の場合）。${\displaystyle \forall x_{1},...,x_{n}.\exists y.F(x_{1},...,x_{n},y)}$ ${\displaystyle \forall x_{1},...,x_{n},y,y'.}$ ${\displaystyle F(x_{1},...,x_{n},y)\land F(x_{1},...,x_{n},y')\rightarrow y=y'}$ ${\displaystyle n=0}$
33. Uzquiano, Gabriel (2018年10月17日). 「Quantifiers and Quantification」. Zalta, Edward N. (編). Stanford Encyclopedia of Philosophy (2018年冬版).特にセクション 3.2「Many-Sorted Quantification」を参照してください。
34. エンダートン、H. 『論理学への数学入門』第2版、アカデミックプレス、2001年、296-299頁。
35. 一部の著者は、 L _κωに有限個の自由変数を持つ式のみを認め、より一般的には、 L _κλに λ 個未満の自由変数を持つ式のみを認めています。
36. Bosse, Uwe (1993). 「不動点論理と層状不動点論理のためのエーレンフォイヒト・フレッセゲーム」. Börger, Egon (編).コンピュータサイエンスロジック: 第6回ワークショップ, CSL'92, サン・ミニアート, イタリア, 1992年9月28日 - 10月2日. 選集. コンピュータサイエンス講義ノート. 第702巻. Springer-Verlag . pp.  100– 114. ISBN 3-540-56992-8. Zbl  0808.03024。
37. メルビン・フィッティング（2012年12月6日）「一階述語論理と自動定理証明」Springer Science & Business Media. ISBN 978-1-4612-2360-3。
38. 「15-815 自動定理証明」www.cs.cmu.edu . 2024年1月10日閲覧。
39. Avigad他(2007) は、素数定理の証明を形式的に検証するプロセスについて議論している。形式化された証明には、Isabelle証明検証器への約3万行の入力が必要であった。

参考文献

• ラウテンバーグ、ヴォルフガング（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版、ベルリン：クルーワー・アカデミック・パブリッシャーズ。シュプリンガーから入手可能。
• Avigad, Jeremy; Donnelly, Kevin; Gray, David; Raff, Paul (2007);「素数定理の形式的に検証された証明」、ACM Transactions on Computational Logic、第9巻第1号doi :10.1145/1297658.1297660
• バーワイズ、ジョン(1977). 「一階述語論理入門」. バーワイズ、ジョン (編). 『数理論理ハンドブック. 論理学と数学の基礎研究』. アムステルダム, オランダ: 北ホラント (1982年出版). ISBN 978-0-444-86388-1。
• モンク, J. ドナルド (1976). 数学論理学. ニューヨーク: Springer New York. doi :10.1007/978-1-4684-9452-5. ISBN 978-1-4684-9454-9。
• バーワイズ、ジョン、エチェメンディ、ジョン（2000年）『言語の証明と論理』、スタンフォード、カリフォルニア州：CSLI出版（シカゴ大学出版局より配布）
• ボチェンスキ、ヨゼフ・マリア（2007年）『数学論理学の概説』ドルドレヒト、オランダ：D.ライデル、フランス語版とドイツ語版からのオットー・バードによる翻訳
• フェレイロス、ホセ（2001）「現代論理への道 ― 解釈」『記号論理学会誌』第7巻第4号、2001年、pp. 441–484、doi :10.2307/2687794、JSTOR  2687794
• Gamut, LTF (1991)、「論理、言語、意味、第2巻：内包論理と論理文法」、シカゴ、イリノイ州：シカゴ大学出版局、ISBN 0-226-28088-8
• ヒルベルト、デイヴィッド、アッカーマン、ヴィルヘルム（1950年）『数理論理学の原理』チェルシー（ 『論理理論の基礎』 1928年ドイツ語初版の英訳）
• ホッジス、ウィルフリッド（2001年）、「古典論理学I：第一階述語論理」、ゴブル、ルー（編）、『ブラックウェル哲学論理ガイド』、ブラックウェル
• エビングハウス、ハインツ・ディーター;フルム、ヨルグ。およびトーマス、ヴォルフガング (1994)。数学的論理学、数学の学部テキスト、ベルリン、デラウェア州/ニューヨーク州ニューヨーク: Springer-Verlag、第 2 版、ISBN 978-0-387-94258-2
• タルスキ、アルフレッド、ギヴァント、スティーブン（1987年）「変数を使わない集合論の形式化」アメリカ数学会コロキウム出版第41巻、プロビデンス、ロードアイランド州：アメリカ数学会、ISBN 978-0821810415

外部リンク

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