Loading article…
数学や論理学において、高階論理（略称HOL ）は、一階論理とは異なる量化子、場合によってはより強い意味論を持つ論理形式である。高階論理は、その標準的な意味論によって表現力は高いが、モデル理論的な性質は一階論理に比べて劣る。
「高階論理」という用語は、一般的に高階単純述語論理を意味する。ここで「単純」とは、基礎となる型理論が単純型の理論、または単純型理論と呼ばれるものであることを示している。レオン・チュヴィステックとフランク・P・ラムジーは、アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルによる『プリンキピア・マテマティカ』で規定された分岐型理論の単純化としてこれを提案した。単純型は、多相型や依存型を除外することを意味する場合もある。[ 1 ]
一階述語論理は個体を対象とする変数のみを量化し、二階述語論理は集合も対象とし、三階述語論理は集合の集合も対象とする、といった具合に量化していく。
高階論理は、一階、二階、三階、…、 n階論理の和集合です。つまり、高階論理では、任意の深さまで入れ子になった集合に対する量化が可能です。
高階論理には2つの意味論が存在する。
標準意味論または完全意味論では、高次の型オブジェクトに対する量化子は、その型の可能なすべてのオブジェクトを範囲とします。たとえば、個体の集合に対する量化子は、個体の集合の冪集合全体を範囲とします。したがって、標準意味論では、個体の集合が指定されれば、すべての量化子を指定するのに十分です。標準意味論を用いた HOL は、一階述語論理よりも表現力に優れています。たとえば、HOL は、一階述語論理では不可能な自然数および実数のカテゴリカルな公理化を許容します。ただし、クルト・ゲーデルの結果により、標準意味論を用いた HOL は、有効で健全かつ完全な証明計算を許容しません。[ 2 ]標準意味論を用いた HOL のモデル理論的性質も、一階述語論理のそれよりも複雑です。たとえば、二階述語論理のレーヴェンハイム数は、そのような基数が存在する場合、最初の測定可能な基数よりもすでに大きくなっています。[ 3 ]一方、一階述語論理のレーヴェンハイム数は、最小の無限基数であるℵ 0である。
ヘンキン意味論では、各高階型ごとに、それぞれの解釈に個別の領域が含まれます。したがって、例えば、個体の集合に対する量化子は、個体の集合の冪集合の部分集合のみを対象とすることができます。このような意味論を用いたHOLは、一階述語論理よりも強力というよりは、多ソート一階述語論理と同等です。特に、ヘンキン意味論を用いたHOLは、一階述語論理のモデル理論的特性をすべて備えており、一階述語論理から継承された完全で健全かつ有効な証明体系を有しています。
高階論理には、チャーチの単純な型理論[ 4 ]の派生や、さまざまな形式の直観主義型理論が含まれます。ジェラール・ユエは、型理論的な三階論理では単一化可能性が決定不能であることを示しました[ 5 ] [ 6 ] [ 7 ] [ 8 ]。つまり、任意の二階（ましてや任意の高階）項間の方程式に解があるかどうかを判定するアルゴリズムは存在しません。
同型性に関するある概念を除けば、冪集合演算は二階述語論理で定義可能である。この観察に基づき、ヤーッコ・ヒンティッカは1955年に、高階述語論理のあらゆる論理式に対して、二階述語論理で同等充足可能な論理式を見つけることができるという意味で、二階述語論理は高階述語論理をシミュレートできることを確立した。[ 9 ]
「高階論理」という用語は、ある文脈では古典的な高階論理を指すものと想定されている。しかし、様相高階論理も研究されている。複数の論理学者によれば、ゲーデルの存在論的証明は（技術的な観点から）そのような文脈で研究するのが最適である。[ 10 ]
ゲーデルの議論は様相論理であり、少なくとも2階論理である。なぜなら、彼の神の定義には性質に関する明示的な量化が含まれているからである。[...] [AG96]は、議論の一部を2階論理ではなく3階論理と見なすことができることを示した。