幾何論理

数理論理学において、幾何論理は、証明理論的に扱いやすいスコーレムによる一階述語論理の制限であるコヒーレント論理の無限一般化である。幾何論理は、多くの数学理論を表現することができ、トポス理論と密接な関係がある。

一階述語論理の理論は、 I と J が互いに素な式インデックスの集合（それぞれが無限でもよい）であり、式 φ が原子または原子の否定であるような形式の公理のみを使用して公理化できる場合、幾何的である。^[要出典]すべての公理が有限である場合（つまり、各公理について、I と J の両方が有限である場合）、理論は首尾一貫している。 ${\displaystyle \bigwedge _{i\in I}\phi _{i,1}\vee \dots \vee \phi _{i,n_{i}}\implies \bigvee _{j\in J}\phi _{j,1}\vee \dots \vee \phi _{j,m_{j}}}$

すべての第一階理論には一貫した保守的な拡張がある。^[要出典]

ディクホフとネグリ（2015）は、上記の定理の重要性を説明する8つの帰結を挙げている（脚注とほとんどの参考文献は省略）。^[1]

1. G3c のようなシーケント計算のコンテキストでは、公理としての特別なコヒーレント含意は、構造規則 (弱化、収縮、カット) の許容性に影響を与えることなく、推論規則に直接変換できます。
2. 同様に、首尾一貫した理論とは、「原子式のみが重要な役割を果たす、ある単純な形式での自然演繹規則によって表現できる理論」です。
3. 首尾一貫した含意は、グリベンコ類を与えるシークエントを形成します。この場合、第一階のバールの定理として知られる結果は、各I i: 0≤i≤n が首尾一貫した含意であり、シークエントI 1, . . . , I n ⇒ I 0 が古典的に証明可能であれば、直観的に証明可能であることを述べています。
4. 首尾一貫した/幾何学的な理論の例は数多くあります。群論や環論などのすべての代数理論、圏論、体論、局所環論、格子理論、射影幾何学、可分閉局所環論（別名「厳密なヘンゼル局所環」）、および捩れアーベル群の無限理論などの本質的に代数的な理論すべて。
5. 首尾一貫した幾何学的理論は、トポイ間の幾何学的射に沿った引き戻しによって保存されます (Maclane & Moerdijk 1992、第 10 章)。
6. コヒーレント理論 T のモデルのセット内のフィルターされた余極限も T のモデルです。
7. 特別な首尾一貫した含意 ∀x. C ⊃ D は、論理プログラミングのホーン節を一般化します。ここで、D はアトムである必要があります。実際、これらは選言論理プログラムの「節」を一般化します。ここで、D はアトムの選言であることが許可されます。
8. 首尾一貫した理論の有効な定理証明は、（解決に関して）比較的容易かつ明瞭に自動化できます。Bezem らが指摘しているように、スコレム化（新しい関数記号の導入）がなくても実際には困難ではなく、節形式に変換しないことで、通常の数学的議論の構造をより適切に保持できます。

• ディクホフ、ロイ; ネグリ、サラ (2015)、「一階述語論理の幾何化」、記号論理学会誌、21 (2): 123–163、doi :10.1017/bsl.2015.7、hdl : 10023/6818
• ジョンストン、ピーター（2002）『象のスケッチ：トポス理論大全』オックスフォード大学出版局、ISBN 978-0-19-852496-0、Zbl  1071.18002（2巻、オックスフォード ロジック ガイド 43 および 44、第 3 巻準備中）
• Maclane, Saunders Mac; Moerdijk, Ieke (1992)、Sheaves in Geometry and Logic、Springer: Berlin、doi :10.1007/978-1-4612-0927-0、ISBN 978-1-4612-0927-0

• 「なぜ幾何学理論は「幾何学的」と呼ばれるのか？」Stack Exchange。2020年11月15日。