[logic-ml] modal homotopy type theory

[logic]

少し面白い本を
reviewしたので、
ご案内しておきます。


https://zbmath.org/?q=an%3A07162136


Homotopy type theoryというのは
Martin Lofのtype theoryの延長上に
あるもので、既に本も出版されていて
無償で手に入ります。

https://homotopytypetheory.org/book/
http://www.kurims.kyoto-u.ac.jp/~uemura/files/hott-intro-ja.pdf
http://pantodon.shinshu-u.ac.jp/topology/literature/homotopy_type_theory.html

Voevodsky達のideaは壮大で、
ZFCではなく、このHoTTを数学の基礎付けに
使おうという話です。ZFCはUndecidableですが、
HoTTはDecidableです。Type theoryだから
Godelの不完全性定理が適用されないのです。
この提案はずっとPracticalな側面をもっていて、
遠くない将来には数学の論文を雑誌に投稿するに
当たってはこのHoTTの中での完全無欠な証明の
Fileを必ず付けなくならず、そのFileは人間と
機械のInteractiveな作業で作成されます。例えて
言えば、現在論文は必ずTexで作成しなければいけないことに
なっていますが、そのような話です。
こうなってくると
証明に論理的Gapがあるなんて話は過去のものになります。
投稿した段階で既にその論文は少なくとも論理的には完璧であることが
担保されているからです。

にしむら
https://www.researchgate.net/profile/Hirokazu_Nishimura