数理論理学と数学の基礎

数学の基礎については, この Stanford の site が良いように思う。Gödel の不完全性定理などについても, 詳しく書いてある。

数理論理学では, 圏と関手の言葉がよく用いられる。 高次の圏も用いられている。例えば, Lumsdaine の [Lum] では, Leinster の weak \(\omega \)-category [Lei04] が用いられている。Garner と van den Berg [BG11] も独立に同様のことを考えている。

何と モデル圏とも関係がある。例えば, Awodey と Warren の [AW09] など。Gambino と Garner の [GG08] もある。Awodey と Hofstra と Warren の [AHW13] の Introduction を読むと概要が分かるかもしれない。Awodey による解説 [Awo12] もある。van den Berg と Garner の [BG12] を見ると, もはやホモトピー論の論文なのか数理論理学の論文なのか分からない感じである。

これらの元になっているのは, Hofmann と Streicher [HS98] による type theory の groupoid model のようである。

• Martin-Löf constructive type theory [Mar75]
• Hofmann-Streicher groupoid model

Simplicial set や モデル圏などの, ホモトピー論的概念を用いた Martin-Löf type theory の解釈や一般化などは, 最近では homotopy type theory と呼ばれている。

• homotopy type theory

Combinatorial model category で使われている accessible category の概念を用いて, logical system 全体の成す category を考えようというのは, Arndt らの [Arn+07] である。

圏にいくつかの構造を付加した institution というもの [GB92] も用いられている。Diaconescu [Dia02] は, Grothendieck construction の institution への一般化を考えている。

数理論理学の最近の影響としては, Hrushovsky による model theory の応用を挙げないわけにはいかないだろう。

• model theory

Bouscaren の本 [Bou98] をまずみてみるのがよいかもしれない。 Breiner の thesis [Bre] によると, modern model theory は「代数幾何学 \(-\) 体」と呼ばれているらしい。Breiner は Hodges の本 [Hod97] を参照している。

Breiner はこのthesis で logical theory の \(\mathrm {Spec}\) を定義している。

• logical scheme

数学の基礎としては, 既存の数学の正しさを確認することはとても重要である。 最近では, Lean のような 証明を支援するソフトウェアが使えるようになり, そのような作業もかなり楽になった。 数学の定義や命題をこのようなソフトウェアが読める形にすることを formalization という。

• formalization

そのような formalization の過程で, 既存の数学に関する疑問がいくつも出てきても不思議ではない。 例えば Buzzard は [Buz25] で, 数学における「等しい」ことの意味について議論している。

References

[AHW13]

Steve Awodey, Pieter Hofstra, and Michael A. Warren. “Martin-Löf complexes”. In: Ann. Pure Appl. Logic 164.10 (2013), pp. 928–956. arXiv: 0906.4521. url: http://dx.doi.org/10.1016/j.apal.2013.05.001.

[Arn+07]

Peter Arndt, Rodrigo de Alvarenga Freire, Odilon Otavio Luciano, and Hugo Luiz Mariano. “A global glance on categories in logic”. In: Log. Univers. 1.1 (2007), pp. 3–39. url: http://dx.doi.org/10.1007/s11787-006-0002-7.

[AW09]

Steve Awodey and Michael A. Warren. “Homotopy theoretic models of identity types”. In: Math. Proc. Cambridge Philos. Soc. 146.1 (2009), pp. 45–55. arXiv: 0709.0248. url: http://dx.doi.org/10.1017/S0305004108001783.

[Awo12]

Steve Awodey. “Type theory and homotopy”. In: Epistemology versus ontology. Vol. 27. Log. Epistemol. Unity Sci. Dordrecht: Springer, 2012, pp. 183–201. arXiv: 1010.1810. url: http://dx.doi.org/10.1007/978-94-007-4435-6_9.

[BG11]

Benno van den Berg and Richard Garner. “Types are weak \(\omega \)-groupoids”. In: Proc. Lond. Math. Soc. (3) 102.2 (2011), pp. 370–394. arXiv: 0812.0298. url: http://dx.doi.org/10.1112/plms/pdq026.

[BG12]

Benno van den Berg and Richard Garner. “Topological and simplicial models of identity types”. In: ACM Trans. Comput. Log. 13.1 (2012), Art. 3, 44. arXiv: 1007.4638. url: http://dx.doi.org/10.1145/2071368.2071371.

[Bou98]

Elisabeth Bouscaren, ed. Model theory and algebraic geometry. Vol. 1696. Lecture Notes in Mathematics. An introduction to E. Hrushovski’s proof of the geometric Mordell-Lang conjecture. Berlin: Springer-Verlag, 1998, pp. xvi+211. isbn: 3-540-64863-1. url: http://dx.doi.org/10.1007/978-3-540-68521-0.

[Bre]

Spencer Breiner. Scheme representation for first-order logic. arXiv: 1402.2600.

[Buz25]

Kevin Buzzard. “Grothendieck’s use of equality”. In: The mathematical and philosophical legacy of Alexander Grothendieck. Chapman Math. Notes. Birkhäuser/Springer, Cham, [2025] ©2025, pp. 337–354. arXiv: 2405.10387. url: https://doi.org/10.1007/978-3-031-68934-5_13.

[Dia02]

Răzvan Diaconescu. “Grothendieck institutions”. In: Appl. Categ. Structures 10.4 (2002), pp. 383–402. url: http://dx.doi.org/10.1023/A:1016330812768.

[GB92]

Joseph A. Goguen and Rod M. Burstall. “Institutions: abstract model theory for specification and programming”. In: J. Assoc. Comput. Mach. 39.1 (1992), pp. 95–146. url: http://dx.doi.org/10.1145/147508.147524.

[GG08]

Nicola Gambino and Richard Garner. “The identity type weak factorisation system”. In: Theoret. Comput. Sci. 409.1 (2008), pp. 94–109. arXiv: 0803.4349. url: http://dx.doi.org/10.1016/j.tcs.2008.08.030.

[Hod97]

Wilfrid Hodges. A shorter model theory. Cambridge University Press, Cambridge, 1997, pp. x+310. isbn: 0-521-58713-1.

[HS98]

Martin Hofmann and Thomas Streicher. “The groupoid interpretation of type theory”. In: Twenty-five years of constructive type theory (Venice, 1995). Vol. 36. Oxford Logic Guides. New York: Oxford Univ. Press, 1998, pp. 83–111.

[Lei04]

Tom Leinster. Higher operads, higher categories. Vol. 298. London Mathematical Society Lecture Note Series. Cambridge: Cambridge University Press, 2004, pp. xiv+433. isbn: 0-521-53215-9. arXiv: math/0305049. url: http://dx.doi.org/10.1017/CBO9780511525896.

[Lum]

Peter LeFanu Lumsdaine. Weak \(\omega \)-categories from intensional type theory. arXiv: 0812.0409.

[Mar75]

Per Martin-Löf. “An intuitionistic theory of types: predicative part”. In: Logic Colloquium ’73 (Bristol, 1973). Amsterdam: North-Holland, 1975, 73–118. Studies in Logic and the Foundations of Mathematics, Vol. 80.