二階述語論理

論理学と数学において、二階述語論理は一階述語論理の拡張であり、一階述語論理自体は命題論理の拡張である。^{[ a ]}二階述語論理は、さらに高階述語論理と型理論によって拡張される。

一階述語論理は、個体（議論領域の要素）を対象とする変数のみを量化します。二階述語論理は、それに加えて関係も量化します。例えば、二階述語論理の文は、${\displaystyle \forall P\,\forall x(Px\lor \neg Px)}$論理は、すべての式Pとすべての個体xに対して、Pxが真であるか、または ( Px ) が真でないかのどちらかであることを示しています (これは排中律です)。 2 階論理には、集合、関数、およびその他の変数に対する量化も含まれます (以下のセクションを参照)。 1 階論理と 2 階論理の両方で、議論領域(単に「領域」または「宇宙」と呼ばれることが多い)の概念が使用されます。領域は、個々の要素を量化できる集合です。

一階述語論理は個体に対しては量化できますが、性質に対しては量化できません。つまり、Cube( b ) のような原子文を取り、名前を変数に置き換えて量化子を付けることで量化された文を得ることができます。^{[ 1 ]}

$${\displaystyle \exists x\,\mathrm {Cube} (x)}$$

しかし、述語については同じことはできません。つまり、次の式は成り立ちません。

$${\displaystyle \exists \mathrm {P} \,\mathrm {P} (b)}$$

これは一階述語論理の文ではありませんが、これは正当な二階述語論理の文です。ここで、Pは述語変数であり、意味的には個体の集合です。^{[ 1 ]}

その結果、二階述語論理は一階述語論理よりも表現力に優れている。例えば、一階述語論理では、すべての立方体と正四面体の集合を特定する方法はない。しかし、二階述語論理では、この集合の存在を次のように主張することができる。

$${\displaystyle \exists \mathrm {P} \,\forall x\,(\mathrm {P} x\leftrightarrow (\mathrm {Cube} (x)\vee \mathrm {Tet} (x)).}$$

すると、この集合の性質を主張することができます。例えば、次の記述は、すべての立方体と正四面体の集合には正十二面体は含まれないことを示しています。

$${\displaystyle \forall \mathrm {P} \,(\forall x\,(\mathrm {P} x\leftrightarrow (\mathrm {Cube} (x)\vee \mathrm {Tet} (x)))\rightarrow \lnot \exists x\,(\mathrm {P} x\wedge \mathrm {Dodec} (x))).}$$

二階述語論理は、到達可能性の性質を表現できるため、特に有用です。たとえば、Parent( x , y )がxがyの親であることを意味する場合、一階述語論理ではxがyの祖先であるという性質を表現できません。二階述語論理では、 y を含み、Parent 関係で閉じているすべての人物の集合にはx が含まれる、と表現できます。

$${\displaystyle \forall \mathrm {P} \,((\mathrm {P} y\wedge \forall a\,\forall b\,((\mathrm {P} b\wedge \mathrm {親} (a,b))\rightarrow \mathrm {P} a))\rightarrow \mathrm {P} x)。}$$

注目すべきは、二階述語論理では述語を表す変数がある一方で、述語のプロパティを表す変数はないということである。例えば、述語P Cube、Tet、Dodec に対して真となるプロパティ Shape( P ) が存在すると言うことはできない。これには三階述語論理が必要となる。^{[ 2 ]}

二階述語論理の構文は、どの式が整形式論理式であるかを規定する。一階述語論理の構文に加えて、二階述語論理には多くの新しい種類の変数（型と呼ばれることもある）が含まれる。それらは以下のとおりである。

• 個体の集合を範囲とする変数の一種。Sがこの種の変数であり、tが一次項である場合、式t ∈ S ( S ( t ) または括弧を省略してStとも表記) は原子式である。個体の集合は、定義域上の単項関係とみなすこともできる。
• 各自然数kに対して、個体上のすべてのk項関係を表す変数群が存在する。Rがそのようなk項関係変数であり、t ₁ ,..., t _kが一階項である場合、式R ( t ₁ ,..., t _k ) は原子式である。
• 各自然数kに対して、定義域のk個の要素を受け取り、定義域の 1 つの要素を返すすべての関数を網羅する変数があります。fがそのようなk項関数変数であり、t ₁ ,..., t _kが一次項である場合、式f ( t ₁ ,..., t _k ) は一次項です。

先に定義した各変数は、全称量化および／または存在量化によって式を構築することができる。したがって、量化子には多くの種類があり、変数の種類ごとに2種類ずつ存在する。二階述語論理における文は、一階述語論理と同様に、自由変数（いかなる種類の自由変数も含む）を持たない整形式の式である。

上記の定義において関数変数を導入しないことも可能です（実際にそうする著者もいます）。なぜなら、n項関数変数は、 n +1項の関係変数と、その関係のn +1番目の引数における「結果」の一意性を表す適切な式によって表現できるからです。（シャピロ 2000、p.63  ）

弱二階述語論理（WSO）は、有限集合に対する量化のみを許容する二階述語論理の制限である。つまり、有限個の正の要素を持つ単項関係に対する量化のみを許容する。

単項二階論理(MSO) は、単項関係 (つまり集合) に対する量化のみを許容する二階論理の制限です。これは WSO よりも強力です。上記のように関係と等価であるため、関数に対する量化も許容されません。これらの制限のない二階論理は、単項バージョンと区別するために、完全二階論理と呼ばれることがあります。単項二階論理は、グラフ理論におけるアルゴリズム的メタ定理であるクールセルの定理の文脈で特に使用されます。完全無限二分木 ( S2S )の MSO 理論は決定可能です。対照的に、任意の無限集合 (またはたとえば (${\displaystyle \mathbb {N} }$,+)) は真の2階算術を解釈できるため、決定不能です。

一階述語論理と同様に、二階述語論理においても、特定の二階言語における非論理記号を含めることができる。ただし、これらの記号は、それらが形成するすべての項が、一階述語論理の項（一階述語論理の変数に代入できるもの）か、二階述語論理の項（適切な種類の二階述語論理の変数に代入できるもの）のいずれかでなければならないという制約がある。

2 階論理の式は 1 階であると言われ、(そして時には と表記される)${\displaystyle \Sigma _{0}^{1}}$または${\displaystyle \Pi _{0}^{1}}$）その量化子（全称量化子または存在量化子の場合がある）が1階変数のみを対象とする場合、2階の自由変数を持つ可能性はあるが、A${\displaystyle \Sigma _{1}^{1}}$（存在二階）式は、二階変数に対する存在量化子をいくつか追加的に持つ式である。${\displaystyle \exists R_{0}\ldots \exists R_{m}\phi }$、 どこ${\displaystyle \phi }$は一階述語論理式である。存在二階述語論理式のみからなる二階述語論理の断片は存在二階述語論理と呼ばれ、ESOと略される。${\displaystyle \Sigma _{1}^{1}}$、あるいは∃SOとしても。${\displaystyle \Pi _{1}^{1}}$式は双対的に定義され、普遍的な二階述語論理と呼ばれます。より表現力豊かな断片は、相互再帰によって任意のk > 0 に対して定義されます。${\displaystyle \Sigma _{k+1}^{1}}$形式は${\displaystyle \exists R_{0}\ldots \exists R_{m}\phi }$、 どこ${\displaystyle \phi }$は${\displaystyle \Pi _{k}^{1}}$式、および類似の式、${\displaystyle \Pi _{k+1}^{1}}$形式は${\displaystyle \forall R_{0}\ldots \forall R_{m}\phi }$、 どこ${\displaystyle \phi }$は${\displaystyle \Sigma _{k}^{1}}$公式。（2階算術の類似の構成については、解析階層を参照のこと。）

二階述語論理の意味論は、各文の意味を確立します。一階述語論理には標準的な意味論が一つしかないのに対し、二階述語論理では、標準意味論とヘンキン意味論という、一般的に使用される二つの異なる意味論があります。これらの意味論のそれぞれにおいて、一階述語論理の量化子と論理結合子の解釈は、一階述語論理と同じです。二種類の意味論で異なるのは、二階述語論理の変数に対する量化子の範囲だけです。^{[ 3 ]}

標準意味論（完全意味論とも呼ばれる）では、量化子は適切な種類のすべての集合または関数の範囲をとります。この条件を満たすモデルは完全モデルと呼ばれ、これは、2 階量化子の範囲がモデルの 1 階部分の冪集合であるモデルと同じです。^{[ 3 ]}したがって、1 階変数の定義域が確立されると、残りの量化子の意味が固定されます。2 階論理に表現力を与えるのはこの意味論であり、この記事の残りの部分ではこの意味論を前提とします。

レオン・ヘンキン（1950）は、2階および高階理論のための代替的な意味論を定義しました。この意味論では、高階領域の意味は、型理論に基づいて、対象となる集合または関数の性質を明示的に公理化することによって部分的に決定されます。ヘンキン意味論は、多ソートされた1階意味論の一種であり、標準意味論のように意味論が標準モデルに固定されるのではなく、公理のモデルのクラスが存在します。ヘンキン意味論におけるモデルは、高階領域の解釈として集合または関数の集合を提供します。これは、その種のすべての集合または関数の真部分集合である可能性があります。ヘンキンは、自身の公理化に関して、 1階論理で成り立つゲーデルの完全性定理とコンパクト性定理が、ヘンキン意味論を用いた2階論理にも引き継がれることを証明しました。ヘンキン意味論についてもレーヴェンハイム・スコレムの定理が成り立つため、リンドストロームの定理はヘンキンモデルが単なる偽装された一階モデルであることを示唆している。^{[ 4 ]}

2階算術などの理論では、高階領域の非標準的な解釈の存在は、ヘンキンが用いた型理論から派生した特定の公理化の欠陥であるだけでなく、ゲーデルの不完全性定理の必然的な帰結でもある。つまり、ヘンキンの公理は、標準的な解釈が唯一可能なモデルであることを保証するために、これ以上補完することはできない。ヘンキン意味論は、 2階算術の研究において一般的に用いられている。

Jouko Väänänenは、2階述語論理におけるヘンキン意味論と完全意味論の区別は、ZFCにおける証明可能性とVにおける真理の区別に類似していると主張した。前者はレーヴェンハイム・スコレムの定理やコンパクト性などのモデル理論的性質に従い、後者は範疇性現象を持つからである。^{[ 3 ]}例えば、「我々は意味のある問いを立てることはできないが、${\displaystyle V}$定義される${\displaystyle \mathrm {ZFC} }$本当の${\displaystyle V}$しかし、もし私たちが再定式化するならば${\displaystyle \mathrm {ZFC} }$内部${\displaystyle \mathrm {ZFC} }$すると、再定式化された${\displaystyle \mathrm {ZFC} }$…は可算モデルを持つため、カテゴリカルにはなり得ない。」

二階述語論理は一階述語論理よりも表現力に優れています。例えば、定義域がすべての実数の集合である場合、一階述語論理では、各実数の加法逆元の存在を次のように主張できます。${\displaystyle \forall x\exists y(x+y=0)}$しかし、実数の集合に対する最小上界の性質を主張するには、二階述語論理が必要です。この性質は、有界で空でない実数の集合はすべて上限を持つというものです。定義域がすべての実数の集合である場合、次の二階述語論理の文（2行に分割）が最小上界の性質を表します。 $${\displaystyle {\begin{aligned}\forall A{\biggl (}&{\bigl (}\exists w(w\in A)\wedge \exists z\forall u(u\in A\rightarrow u\leq z){\bigr )}\rightarrow \\&\exists x{\Bigl (}\forall u(u\in A\rightarrow u\leq x)\wedge \forall y\forall u{\bigl (}(u\in A\rightarrow u\leq y)\rightarrow x\leq y{\bigr )}{\Bigr )}{\biggr )}\\\end{aligned}}}$$ ここで、最初の行の部分は${\displaystyle w}$という仮定を表しています${\displaystyle A}$空ではない（要素がある）${\displaystyle w}$最初の行の残りの部分は、${\displaystyle A}$上限が定められている（ある数が存在する）${\displaystyle z}$すべての要素以上${\displaystyle u}$の${\displaystyle A}$2行目は最小上界の存在を表しています。${\displaystyle x}$それは次のように主張する。${\displaystyle x}$上限値です（任意の要素以上です）${\displaystyle u}$で${\displaystyle A}$）そして、もしある数が${\displaystyle y}$も上限値なので、${\displaystyle x\leq y}$この性質を満たす順序体は、実数体と同型である。一方、実数で有効な一階述語論理の文の集合は、コンパクト性定理により、任意の大きさのモデルを持つ。したがって、最小上界の性質は、一階述語論理の文の集合では表現できない。（実際には、実数閉体はすべて、シグネチャにおいて同じ一階述語論理の文を満たす。）${\displaystyle \langle +,\cdot ,\leq \rangle }$（実際の数値として。）

二階述語論理では、「定義域は有限である」または「定義域は可算濃度である」という形式的な文を書くことができます。定義域が有限であると言うには、定義域から自身へのすべての全射関数が単射であるという文を用います。定義域が可算濃度であると言うには、定義域の任意の2つの無限部分集合の間に全単射が存在するという文を用います。コンパクト性定理と上方レーヴェンハイム・スコレム定理から、一階述語論理ではそれぞれ有限性や可算性を特徴付けることはできないことがわかります。

ESOのような二階述語論理の断片は、完全な二階述語論理よりは表現力が劣るものの、一階述語論理よりも表現力に優れている。また、ESOは、ヘンキン量化子で拡張された一階述語論理、ヒンティッカとサンドゥの独立性重視の論理、ヴァーナネンの依存論理など、量化子の依存関係の非線形順序付けを可能にする一階述語論理の拡張と翻訳等価性を持つ。

論理における演繹体系とは、どの論理式の列が有効な証明を構成するかを決定する推論規則と論理公理の集合である。二階述語論理にはいくつかの演繹体系が使用できるが、標準的な意味論（下記参照）に対して完全なものは存在しない。これらの体系はそれぞれ健全であり、つまり、それらを用いて証明できる文は、適切な意味論において論理的に妥当である。

使用できる最も弱い演繹システムは、1 階論理の標準的な演繹システム (自然演繹など) に 2 階項の置換規則を追加したものです。^{[ b ]}この演繹システムは、 2 階算術の研究でよく使用されます。

シャピロ（2000）とヘンキン（1950）が考察した演繹体系は、拡張された一階演繹体系に理解公理と選択公理の両方を追加する。これらの公理は、標準的な二階意味論に対しては健全である。また、理解公理と選択公理を満たすヘンキンモデルに限定されたヘンキン意味論に対しても健全である。^{[ c ]}

完全な二階意味論を持つ実数の二階理論を、次のようにして一階理論に還元することを試みることができる。まず、領域をすべての実数の集合から、すべての実数の集合を含む二項ソート領域に拡張する。言語に新しい二項述語、すなわちメンバーシップ関係を追加する。すると、二階であった文は一階になり、以前は二階量化子であったものが、代わりに二項ソートの範囲をとるようになる。この還元は、要素が数か集合かを示す単項述語を追加し、領域を実数の集合と実数の冪集合の和集合とすることで、一項ソート理論でも試みることができる。

しかし、この領域は実数のすべての集合を含むと主張されていることに注意してください。レーヴェンハイム・スコーレムの定理が示すように、この要件は一階述語論理の文、あるいは一階述語論理の理論に還元することはできません。この定理は、実数の可算無限部分集合（これを内部数と呼びます）と、内部数の集合の可算無限集合（これを内部集合と呼びます）が存在し、内部数と内部集合からなる領域が、実数と実数の集合からなる領域が満たすのと全く同じ一階述語論理の文を満たすことを意味します。特に、それは実質的に次のような一種の最小上界公理を満たします。

すべての内部数の集合が可算であること（それらが稠密な順序集合を形成するという事実と併せて）は、その集合が完全な最小上界公理を満たさないことを意味する。すべての内部集合の集合が可算であることは、それがすべての内部数の集合のすべての部分集合の集合ではないことを意味する（カントールの定理によれば、可算無限集合のすべての部分集合の集合は非可算無限集合となるため）。この構成はスコレムのパラドックスと密接に関連している。

このように、実数および実数集合の1階理論には多くのモデルがあり、その中には可算なものもある。しかし、実数の2階理論にはモデルが1つしかない。これは、アルキメデス完全順序体は1つしか存在しないという古典的な定理と、アルキメデス完全順序体のすべての公理が2階論理で表現できるという事実から導かれる。このことから、実数の2階理論は1階理論に還元できないことがわかる。つまり、実数の2階理論にはモデルが1つしかないのに対し、対応する1階理論には多くのモデルが存在するということである。

標準的な意味論を持つ二階述語論理が一階述語論理よりも表現力に優れていることを示す、より極端な例もある。連続体仮説が成り立つ場合は実数のみをモデルとし、連続体仮説が成り立たない場合はモデルを持たない有限二階述語理論が存在する。^{[ 5 ]}この理論は、実数を完全なアルキメデス的順序体として特徴付ける有限理論と、定義域が第一の非可算濃度であるという公理から構成される。この例は、二階述語論理における文が矛盾しないかどうかという問題が極めて微妙であることを示している。

二階述語論理のその他の制約については、次のセクションで説明します。

ゲーデルの不完全性定理の帰結として、次の 3 つの望ましい属性を同時に満たす 2 階論理式の演繹システム (つまり、証明可能性の概念) は存在しない。 ^{[ d ]}

• （健全性）証明可能なすべての二階述語論理式は普遍的に妥当であり、すなわち、標準的な意味論の下ではすべての領域で真である。
• （完全性）標準的な意味論の下では、普遍的に妥当なすべての二階論理式は証明可能である。
• （有効性）与えられた記号列が証明であるかどうかを正しく判定できる証明チェックアルゴリズムが存在する。

この帰結は、二階述語論理は完全な証明理論を許容しない、という形で表現されることがある。この点において、標準的な意味論を持つ二階述語論理は一階述語論理と異なる。クワインは、完全な証明体系の欠如を、二階述語論理を厳密には論理ではないと考える理由として挙げた。^{[ 6 ]}

前述のように、ヘンキンは、一階述語論理の標準的な演繹体系が、ヘンキン意味論を用いた二階述語論理に対して健全で完全かつ効果的であることを証明し、また、理解原理と選択原理を用いた演繹体系が、これらの原理を満たすモデルのみを用いてヘンキン意味論に対して健全で完全かつ効果的であることを証明した。

コンパクト性定理とレーヴェンハイム・スコレムの定理は、2階述語論理の完全なモデルでは成り立ちません。しかし、ヘンキンモデルでは成り立ちます。^{[ 7 ]}

述語論理は、 C.S. パースによって数学界に導入されました。彼は「二階述語論理」という用語を造語し、その記法は現代の形式に最も近いものです（Putnam 1982）。しかし、今日では、論理学を学ぶ学生の多くは、パースより数年前に著作を発表したものの、バートランド・ラッセルとアルフレッド・ノース・ホワイトヘッドによって有名になるまであまり知られていなかったフレーゲの著作に馴染みがあります。フレーゲは、対象に対する量化と性質や集合に対する量化を区別するために異なる変数を用いましたが、自身は2種類の異なる論理を行っているとは考えていませんでした。ラッセルのパラドックスが発見された後、彼の体系に何か問題があることが認識されました。最終的に、論理学者たちは、フレーゲの論理を様々な方法で制限することで（現在では一階述語論理と呼ばれているもの）、この問題が解消されることを発見しました。つまり、一階述語論理だけでは集合や性質を量化することはできないのです。現在標準となっている論理の階数階層は、この時期に確立されました。

集合論は、一階述語論理の枠組みの中で公理化された体系として定式化できることが発見された（ただし、いくつかの種類の完全性は犠牲になるが、ラッセルのパラドックスほどひどいものではない）。そして、集合は数学にとって不可欠であるため、実際に定式化された（ツェルメロ＝フレンケル集合論を参照）。 算術、部分論、その他さまざまな強力な論理理論は、一階述語論理の量化以上の論理装置に頼ることなく公理的に定式化することができ、このこととゲーデルとスコレムが一階述語論理に固執したことが相まって、二階述語論理（またはそれ以上の階数）の研究は全般的に衰退していった。

この否定は、WV クワインをはじめとする一部の論理学者によって積極的に提唱された。クワインは、 Fxのような述語言語の文では、「x」は対象を表す変数または名前として考えられ、したがって「すべてのものについて、…である」のように量化できるが、「F 」は不完全な文の略語として考えられ、対象の名前（特性のような抽象的な対象の名前でさえも）ではないという見解を提唱した。例えば、「…は犬である」という意味かもしれない。しかし、このようなものに対して量化できると考えるのは意味がない。（このような立場は、概念と対象の区別に関するフレーゲ自身の議論と完全に一致している。）したがって、述語を変数として使用することは、述語が名前の地位を占めることになり、名前の地位は個々の変数のみが占めるべきである。この推論は、ジョージ・ブーロスによって否定されている。  

近年、二階述語論理は、ブーロスが二階述語量化を一階述語量化と同じ対象領域における複数量化と解釈したこと（Boolos 1984）に後押しされ、いくらか復活を遂げている。ブーロスはさらに、「批評家の中には互いにしか賞賛しない者もいる」や「フィアンケットの部下の中には、他の誰にも付き添われずに倉庫に入った者もいた」といった文は一階述語化不可能であると指摘し、これらは二階述語量化の力によってのみ表現できると主張する。しかし、一般化量化や部分順序（または分岐）量化でも、一階述語化不可能とされるある種の文を表現するのに十分であり、これらは二階述語量化を必要としない。

有限構造上のさまざまな形式の二階述語論理の表現力は、計算複雑性理論と密接に結びついています。記述的複雑性の分野では、言語（有限文字列の集合）を表現するために必要な論理の力によって、どの計算複雑性クラスを特徴づけることができるかを研究します。有限アルファベットAの文字列w  = w ₁ ··· w _nは、ドメインD = {1,..., n }、各a ∈ Aに対する単項述語P _a 、 w _i = aとなるインデックスiによって満たされる述語、およびどのインデックスがどれであるかを一意に識別する追加の述語 (通常、 D上の後継関数のグラフまたは順序関係 <、場合によっては他の算術述語) を持つ有限構造で表現できます。逆に、任意の有限構造 (有限シグネチャ上) のケイリー表は、有限文字列でエンコードできます。       

この識別により、有限構造上の二階述語論理の変種について、以下の特徴付けが得られる。

• REG（正規言語）は、単項二階論理式で定義可能な言語の集合である（Büchi-Elgot-Trakhtenbrotの定理、1960年）。
• NPは、存在論理式、二階述語論理式によって定義可能な言語の集合である（フェイギンの定理、1974年）。
• co-NPとは、普遍的な二階述語論理式によって定義可能な言語の集合である。
• PHは、2階述語論理式で定義可能な言語の集合である。
• PSPACEとは、推移閉包演算子を追加した二階述語論理式で定義可能な言語の集合である。
• EXPTIMEは、最小不動点演算子を追加した2階述語論理式で定義可能な言語の集合である。

これらのクラス間の関係は、有限構造上の論理の相対的な表現力に直接影響を与えます。たとえば、PH  = PSPACEの場合、2階論理に推移閉包演算子を追加しても、有限構造上の表現力は向上しません。 

• 一階述語論理
• 高階論理
• レーヴェンハイム番号
• オメガ言語
• 二階命題論理
• 単項二階述語論理

• Andrews, Peter (2002).数理論理学と型理論入門：証明を通して真理へ（第2 版）. Kluwer Academic Publishers.
• ブーロス、ジョージ（1984） 。 「存在するということは、変数の値である（あるいはいくつかの変数の値である）」。哲学ジャーナル。81 （8）：430–50。doi ：10.2307 / 2026308。JSTOR 2026308。 ブーロス著『論理、論理、そして論理』（1998年）に再録。
• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid ; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde; Weinstein, Scott (2007).有限モデル理論とその応用. 理論計算機科学テキストシリーズ. EATCSシリーズ. ベルリン: Springer-Verlag . ISBN 978-3-540-00428-8. Zbl 1133.03001 . 
• Putnam, Hilary (1982). "Peirce the Logician" . Historia Mathematica . 9 (3): 290–301 . doi : 10.1016/0315-0860(82)90123-9 .. ヒラリー・パトナム著『人間味あふれるリアリズム』（ハーバード大学出版局、 1990年、 252 ～ 260ページ ）に再録。
• Rossberg, M. (2004). "一階述語論理、二階述語論理、および完全性" (PDF) . V. Hendricks 他編 『一階述語論理再考』所収. ベルリン: Logos-Verlag.