一階述語論理

すべての形式言語と同様に、記号そのものの性質は形式論理の範囲外であり、それらは単に文字や句読点として扱われることが多い。

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

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

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

直感的に言えば、式の中で変数記号が自由であるとは、それがどの時点でも量化されていない場合を指します。 ^{[ 8 ] 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番目に現れる xは束縛変数です。

自由変数を含まない一階述語論理の式は、一階述語論理の文と呼ばれます。これらの式は、解釈の下で明確な真偽値を持ちます。例えば、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と表記されます。 
• その表現${\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).}$この式には、 z という自由変数が 1 つあります。

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

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

議論領域Dは、何らかの「対象」の空でない集合です。直感的には、解釈が与えられると、一階述語論理式はこれらの対象についての記述になります。例えば、${\displaystyle \exists xP(x)}$これは、述語P が真となるようなD内の何らかの対象の存在を述べる(より正確には、解釈によって述語記号Pに割り当てられた述語が真となるような対象の存在を述べる)。例えば、D を整数の集合とすることができる。

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

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

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

まず、変数割り当てμを言語のすべての用語に拡張することで、各用語が談話領域の単一の要素に対応するようにすることができます。この割り当てを行うには、以下の規則を使用します。

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

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

• 原子式（1）式${\displaystyle P(t_{1},\ldots ,t_{n})}$値に応じてtrueまたはfalseに関連付けられています。${\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}}$の場合にtrueが割り当てられます${\displaystyle t_{1}}$そして${\displaystyle t_{2}}$議論領域内の同じ対象として評価する（下記の平等に関するセクションを参照）。
• 論理結合子。次の形式の式${\displaystyle \neg \varphi }$、${\displaystyle \varphi \rightarrow \psi }$、などは、命題論理と同様に、問題となっている結合子の真理値表に従って評価されます。
• 存在量化子。式${\displaystyle \exists x\varphi (x)}$Mによれば、${\displaystyle \mu }$評価が存在する場合${\displaystyle \mu '}$異なる変数のうち${\displaystyle \mu }$xの評価に関して最大​​で、解釈Mと変数割り当てに従ってφが真となる${\displaystyle \mu '}$この正式な定義は、${\displaystyle \exists x\varphi (x)}$φ( x ) を満たすようなxの値を選択する方法がある場合に限り、真である。
• 全称量化子。式${\displaystyle \forall x\varphi (x)}$Mによれば、${\displaystyle \mu }$解釈Mと何らかの変数割り当てによって構成されるすべてのペアに対してφ( x )が真である場合${\displaystyle \mu '}$それは${\displaystyle \mu }$xの値に関して最大​​で。これは、${\displaystyle \forall x\varphi (x)}$xのあらゆる可能な値の選択がφ( x ) を真にする場合、それは真である。

式に自由変数が含まれておらず、したがって文である場合、最初の変数割り当てはその真偽値に影響を与えません。言い換えれば、文はMとに従って真であり、${\displaystyle \mu }$Mおよび他のすべての変数割り当てに従って真である場合に限ります。${\displaystyle \mu '}$。

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

• 存在量化子（代替）。式${\displaystyle \exists x\varphi (x)}$Mによれば、議論領域内に次のようなdが存在する場合に真である。${\displaystyle \varphi (c_{d})}$保持します。${\displaystyle \varphi (c_{d})}$これは、φ 中のxの自由な出現箇所すべてにc _dを代入した結果です 。
• 全称量化子（代替）数式${\displaystyle \forall x\varphi (x)}$Mによれば、議論領域内のすべてのdについて、${\displaystyle \varphi (c_{d})}$Mによれば、これは正しい。

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

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

自由変数を含む式の充足可能性は、解釈だけではその式の真偽値が決定されないため、より複雑です。最も一般的な慣習は、自由変数を含む式φは${\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 ]}この断片は、ペアノ算術や、標準的なツェルメロ・フレンケル集合論（ZFC）を含むほとんどの公理的集合論に十分であるため、非常に興味深い。彼らはまた、原始順序対を持つ一階述語論理が、 2つの順序対射影関数を持つ関係代数と等価であることを証明した。^{[ 24 ]： 803}

特定のシグネチャの一次理論は、そのシグネチャの記号からなる文である公理の集合です。公理の集合は有限であるか、再帰的に列挙可能であることが多く、その場合、理論は有効と呼ばれます。一部の著者は、理論には公理のすべての論理的帰結も含まれる必要があると主張します。公理は理論内で成り立つものとみなされ、そこから理論内で成り立つ他の文を導出することができます。

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

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

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

上記の定義では、いかなる解釈においても議論領域は空であってはならない。包括論理のように、空の領域が許容される設定もある。さらに、代数構造のクラスに空の構造が含まれる場合（例えば、空の半順序集合が存在する場合）、そのクラスが一階述語論理における基本クラスとなるためには、空の領域が許容されるか、あるいは空の構造がクラスから削除される必要がある。

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

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

したがって、空のドメインが許容される場合、それはしばしば特殊なケースとして扱われる必要がある。しかし、ほとんどの著者は、定義上、空のドメインを単純に除外している。

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

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

束縛変数に対する制約が必要な理由を理解するために、論理的に有効な式φを考えてみましょう。${\displaystyle \exists x(x=y)}$、算術の (0,1,+,×,=) の署名において。t が項 "x + 1" の場合、式 φ[ t / y ] は${\displaystyle \exists x(x=x+1)}$これは多くの解釈において誤りとなる。問題は、tの自由変数x が置換中に束縛変数になったことである。意図した置換は、φ の束縛変数x を別のもの、例えばzに名前変更することで得られる。置換後の式は次のようになる。${\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は式であり、ターンスタイル記号は${\displaystyle \vdash }$は、2つの部分を区切る句読点として使用されます。直感的には、シーケントは、${\displaystyle (A_{1}\land \cdots \land A_{n})}$暗示する${\displaystyle (B_{1}\lor \cdots \lor B_{k})}$。

先に述べた方法とは異なり、タブロー法における導出は数式のリストではありません。代わりに、導出は数式のツリーです。数式Aが証明可能であることを示すために、タブロー法はAの否定が充足不可能であることを示そうとします。導出のツリーは${\displaystyle \lnot A}$根元から始まり、木の枝は数式の構造を反映するように伸びていきます。例えば、${\displaystyle C\lor D}$充足不可能であることを示すには、CとDがそれぞれ充足不可能であることを示す必要があります。これは、親を持つツリーの分岐点に対応します。${\displaystyle C\lor D}$そして子供Cと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つの異なる個体を「等しい」と解釈できる点です（ただし、ライプニッツの法則によれば、これらの個体はどのような解釈の下でもまったく同じ式を満たします）。つまり、等号関係は、解釈の機能と関係に合致する、議論領域上の任意の同値関係によって解釈できるということです。

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

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

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

平等に関する他の臨時の定義を認める理論もある。

• 関係記号≤を持つ半順序の理論では、 s = tをs ≤ tの略語として定義することができる。${\displaystyle \wedge }$t ≤ s。
• 1つの関係∈を持つ集合論では、s = t を∀ x ( s ∈ x ↔ t ∈ x )の略記として定義することができる。${\displaystyle \wedge }$∀ x ( x ∈ s ↔ x ∈ t )。この等号の定義は、等号の公理を自動的に満たします。この場合、通常の外延性の公理を置き換える必要があります。それは次のように述べることができます。${\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)]}$これは、集合xとyが同じ要素を持つ場合、それらは同じ集合に属するということを意味します。

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

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

完全な一階述語論理よりも弱いシステムで、論理的帰結関係が決定可能なものがある。これには命題論理や単項述語論理が含まれる。単項述語論理は、一階述語論理を単項述語記号のみに制限し、関数記号は含まないものである。関数記号を持たない決定可能な他の論理としては、一階述語論理のガード付き断片や二変数論理がある。ベルネイズ・シェーンフィンケル一階述語論理式クラスも決定可能である。一階述語論理の決定可能な部分集合は、記述論理の枠組みでも研究されている。（Pratt-Hartmann、2023）のモノグラフを参照のこと。^{[ 29 ]}

決定可能な断片の例: ^{[ 30 ]}

• C _2、2つの変数と計数量化子を持つ一階述語論理${\displaystyle \exists ^{\geq n}}$そして${\displaystyle \exists ^{\leq n}}$[ ^{31 ]​}
• 単項一階述語論理断片（MFO、またはレーヴェンハイム断片）：等号、関数記号、および単項述語記号のみを持つ一階述語論理。
• Löb–Gurevich断片：等号のない一階述語論理、単項関数記号のみ、および単項述語記号のみ。
• ラビン断片：等号を含む一階述語論理、単項関数記号がちょうど1つ、かつ単項述語記号のみを含む。
• Bernays–Schönfinkel–Ramsey断片: プレネックス標準形におけるすべての関係一階述語文${\displaystyle \exists ^{*}\forall ^{*}}$接頭辞と等号。

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

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

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

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

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

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

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

レーヴェンハイム・スコレムの定理は、一階理論が無限モデルを持つならば、あらゆる濃度の無限モデルを持つことを示しています。特に、無限モデルを持つ一階理論は圏論的ではありません。したがって、唯一のモデルが自然数の集合を定義域とする一階理論、あるいは唯一のモデルが実数の集合を定義域とする一階理論は存在しません。無限論理や高階論理など、一階論理の多くの拡張は、自然数や実数の圏論的公理化を許容するという意味で、より表現力に富んでいます。しかし、この表現力にはメタ論理的な代償が伴います。リンドストロームの定理によれば、コンパクト性定理と下方レーヴェンハイム・スコレムの定理は、一階論理よりも強い論理では成り立ちません。

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

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

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

• なぜなら${\displaystyle \exists x\varphi (x)}$次のように表現できます${\displaystyle \neg \forall x\neg \varphi (x)}$、 そして${\displaystyle \forall x\varphi (x)}$次のように表現できます${\displaystyle \neg \exists x\neg \varphi (x)}$2つの量化子のいずれか${\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 }$唯一の論理結合子として。
• 同様に、${\displaystyle \neg }$そして${\displaystyle \rightarrow }$論理結合子として、またはシェファーストローク（NAND）演算子またはピアース矢印（NOR）演算子のみを持つ。
• 関数記号や定数記号を完全に回避し、適切な方法で述語記号を使って書き換えることが可能です。例えば、定数記号を使う代わりに${\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})}$この変更には、使用されている述語記号の解釈が正しい意味を持つように、既存の理論に公理を追加する必要がある。^{[ 34 ]}

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

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

通常の1階述語論理では、すべての量化子が及ぶ単一の議論領域が存在します。多ソート1階述語論理では、変数に異なるソートを持たせることができ、それぞれのソートは異なる領域を持ちます。これは型付き1階述語論理とも呼ばれ、ソートは型（データ型と同様）と呼ばれますが、1階型理論とは異なります。多ソート1階述語論理は、2階述語論理の研究でよく用いられます。^{[ 35 ]}

理論に有限個のソートしかない場合、多ソート一階述語論理は単一ソート一階述語論理に還元できる。^{[ 36 ]： 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 )のような式を省略するために使用できます。${\displaystyle \wedge }$∀ y ( P ( y ) → ( x = y )))。
• 追加の量化子を持つ一階述語論理では、 「…となるようなxが多数存在する」といった意味を持つ新しい量化子Qx ,...が用いられます。分岐量化子や、ジョージ・ブーロスらが提唱した複数量化子も参照してください。
• 有界量化子は、集合論や算術の研究においてしばしば用いられる。

無限論理では、無限に長い文を記述できます。例えば、無限個の論理式の連言や選言、あるいは無限個の変数に対する量化などが可能です。無限に長い文は、位相幾何学やモデル理論など、数学の様々な分野で現れます。

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

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

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

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

不動点論理は、正演算子の最小不動点による閉包を追加することにより、一階述語論理を拡張する。^{[ 38 ]}

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

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

これは合法的な一階述語論理ですが、

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

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

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

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