高階論理

数学と論理学において、高階論理（高階論理、略してHOL ）は、追加の量指定子と、場合によってはより強力な意味論によって一階論理と区別される論理形式です。標準的な意味論を持つ高階論理は表現力が豊かですが、モデル理論的特性は一階論理ほど適切ではありません。

「高階論理」という用語は、一般的には高階の単純述語論理の意味で使用されます。ここで「単純」とは、基礎となる型理論が単純型の理論、つまり単純型理論であることを示します。レオン・クウィステックとフランク・P・ラムゼイは、アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルの『プリンキピア・マセマティカ』で規定された複雑で扱いにくい分岐型理論を単純化するものとしてこれを提案しました。単純型は、多態型や依存型を除外することを意味する場合もあります。^[1]

定量化の範囲

第一階述語論理は、個体にわたる変数のみを数量化します。第二階述語論理は、集合についても数量化します。第三階述語論理は、集合の集合についても数量化します、などとなります。

高階論理は、第 1 次、第 2 次、第 3 次、...、 n次論理の結合です。つまり、高階論理では、任意の深さにネストされた集合に対する量化が認められます。

セマンティクス

高階論理には 2 つのセマンティクスが考えられます。

標準または完全な意味論では、高次の型のオブジェクトに対する量指定子は、その型の可能なすべてのオブジェクトに及ぶ。たとえば、個体の集合に対する量指定子は、個体の集合のべき集合全体に及ぶ。したがって、標準意味論では、個体の集合を一度指定すれば、量指定子をすべて指定するだけで十分である。標準意味論のHOLは、一階述語論理よりも表現力に富んでいる。たとえば、HOLでは、一階述語論理では不可能な、自然数、および実数のカテゴリカルな公理化が可能である。しかし、クルト・ゲーデルの結果により、標準意味論のHOLでは、有効で健全で完全な証明計算が不可能である。^[2]標準意味論のHOLのモデル理論的特性も、一階述語論理よりも複雑である。たとえば、二階述語論理のレーヴェンハイム数は、そのような基数が存在する場合、最初の測定可能な基数よりも既に大きい。^[3]対照的に、第一階述語論理のレーヴェンハイム数はℵ ₀であり、最小の無限基数である。

ヘンキン意味論では、各高階型に対する各解釈に個別のドメインが含まれます。したがって、たとえば、個体の集合に対する量指定子は、個体の集合のべき集合のサブセットのみに及ぶ可能性があります。これらの意味論を持つ HOL は、一階述語論理よりも強力というよりは、多ソート一階述語論理と同等です。特に、ヘンキン意味論を持つ HOL は、一階述語論理のモデル理論的特性をすべて備えており、一階述語論理から継承された完全で健全で効果的な証明システムを備えています。

プロパティ

高階論理には、チャーチの単純な型理論^{[4]の派生や、}直観主義型理論のさまざまな形式が含まれます。ジェラール・ユエは、三階論理の型理論的な風味では、統一可能性は決定不可能であることを示しました。 ^[5]^[6]^[7]^[8]つまり、任意の二階項（ましてや任意の高階項）間の方程式に解があるかどうかを決定するアルゴリズムは存在し得ません。

同型性という特定の概念までは、冪集合演算は二階論理で定義可能である。この観察を用いて、ヤッコ・ヒンティッカは1955年に、高階論理のあらゆる式に対して二階論理でそれに対する等充足式を見つけることができるという意味で、二階論理が高階論理をシミュレートできることを確立した。^[9]

「高階論理」という用語は、ある文脈では古典的な高階論理を指すものと想定されている。しかし、様相高階論理も研究されてきた。数人の論理学者によると、ゲーデルの存在論的証明は、（技術的な観点から）そのような文脈で最もよく研究される。^[10]

参照

注記

^ ジェイコブス、1999年、第5章
^ シャピロ1991、87ページ。
^ メナヘム・マジドールとヨーコ・ヴァナネン。「一次論理の拡張のためのレーヴェンハイム・スコレム・タルスキー数について」、ミタグ・レフラー研究所のレポート第 15 号 (2009/2010)。
^ アロンゾ・チャーチ、「単純な型理論の定式化」、シンボリック・ロジック誌5(2):56–68 (1940)
^ Huet, Gérard P. (1973). 「第3階述語論理における統一の決定不可能性」.情報と制御. 22 (3): 257–267. doi :10.1016/s0019-9958(73)90301-x.
^ ジェラール、ユエ (1976 年 9 月)。 Resolution d'Equations dans des Lagages d'Ordre 1,2,...ω (Ph.D.) (フランス語)。パリ第 7 大学。
^ Warren D. Goldfarb (1981). 「第2次統一問題の決定不可能性」(PDF) .理論計算機科学. 13 : 225–230.
^ Huet, Gérard (2002). 「30年後の高次統一」(PDF)。Carreño, V.、Muñoz, C.、Tahar, S. (編)。議事録、第15回国際会議TPHOL。LNCS。第2410巻。Springer。pp. 3–12。
^ HOLのエントリ
^ フィッティング、メルビン（2002年）。タイプ、タブロー、ゲーデルの神。シュプリンガーサイエンス＆ビジネスメディア。p.139。ISBN 978-1-4020-0604-3ゲーデルの議論は様相的であり、少なくとも2次のものである。なぜなら、彼の神の定義には、性質に対する明示的な量化があるからである。[...] [AG96]は、議論の一部を2次的ではなく3次的と見なすことができることを示した。

参考文献

アンドリュース、ピーター B. (2002)。『数理論理学と型理論入門：証明を通して真実へ』第 2 版、Kluwer Academic Publishers、ISBN 1-4020-0763-9
スチュワート・シャピロ、1991年、「基礎主義のない基礎：第二階論理の事例」オックスフォード大学出版局、ISBN 0-19-825029-0
スチュワート・シャピロ、2001年、「古典論理学 II: 高階論理学」、ルー・ゴーブル編『ブラックウェル哲学論理学ガイド』、ブラックウェル、ISBN 0-631-20693-0
ラムベック、J.およびスコット、PJ、1986年。高階カテゴリカル論理入門、ケンブリッジ大学出版局、ISBN 0-521-35653-9
ジェイコブス、バート (1999)。カテゴリカル論理と型理論。論理学と数学の基礎研究 141。ノースホランド、エルゼビア。ISBN 0-444-50170-3。
Benzmüller, Christoph; Miller, Dale (2014)。「高階論理の自動化」。Gabbay, Dov M.、Siekmann, Jörg H.、Woods, John (編)。論理の歴史ハンドブック、第 9 巻: 計算論理。Elsevier。ISBN 978-0-08-093067-1。

外部リンク

アンドリュース、ピーター B、チャーチのタイプ理論、スタンフォード哲学百科事典。
ミラー、デール、1991、「ロジック: 高次」、人工知能百科事典、第 2 版。
ハーバート・B・エンダートン、「第二階および高階論理」、スタンフォード哲学百科事典、2007 年 12 月 20 日発行、2009 年 3 月 4 日実質的改訂。

[1] ジェイコブス、1999年、第5章

[2] シャピロ1991、87ページ。

[3] メナヘム・マジドールとヨーコ・ヴァナネン。「一次論理の拡張のためのレーヴェンハイム・スコレム・タルスキー数について」、ミタグ・レフラー研究所のレポート第 15 号 (2009/2010)。

[church-4] アロンゾ・チャーチ、「単純な型理論の定式化」、シンボリック・ロジック誌5(2):56–68 (1940)

[5] Huet, Gérard P. (1973). 「第3階述語論理における統一の決定不可能性」.情報と制御. 22 (3): 257–267. doi :10.1016/s0019-9958(73)90301-x.

[6] ジェラール、ユエ (1976 年 9 月)。 Resolution d'Equations dans des Lagages d'Ordre 1,2,...ω (Ph.D.) (フランス語)。パリ第 7 大学。

[7] Warren D. Goldfarb (1981). 「第2次統一問題の決定不可能性」(PDF) .理論計算機科学. 13 : 225–230.

[8] Huet, Gérard (2002). 「30年後の高次統一」(PDF)。Carreño, V.、Muñoz, C.、Tahar, S. (編)。議事録、第15回国際会議TPHOL。LNCS。第2410巻。Springer。pp. 3–12。

[9] HOLのエントリ

[Fitting2002-10] フィッティング、メルビン（2002年）。タイプ、タブロー、ゲーデルの神。シュプリンガーサイエンス＆ビジネスメディア。p.139。ISBN 978-1-4020-0604-3ゲーデルの議論は様相的であり、少なくとも2次のものである。なぜなら、彼の神の定義には、性質に対する明示的な量化があるからである。[...] [AG96]は、議論の一部を2次的ではなく3次的と見なすことができることを示した。