数理論理学と数学の基礎

数学の基礎については, この 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

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.

[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.