What is the world of mathematics?

详细信息	查看全文 | 推荐本文 |

• 作者：Lambek ; J.
• 关键词：03B15 ; 03G30 ; 18B05 ; 18B25 ; Type theory ; Categorical logic ; Category of sets ; Topos theory
• 刊名：Annals of Pure and Applied Logic
• 出版年：2004
• 期刊代码：4_01680072
• 类别：cp
• 出版时间：April, 2004
• 卷：126
• 期：1-3
• 页码：149-158
• 文件大小：207 K

摘要

It may be argued that the language of mathematics is about the category of sets, although the definite article requires some justification. As possible worlds of mathematics we may admit all models of type theory, by which we mean all local toposes. For an intuitionist, there is a distinguished local topos, namely the so-called free topos, which may be constructed as the Tarski–Lindenbaum category of intuitionistic type theory. However, for a classical mathematician, to pick a distinguished model may be as difficult as to define the notion of truth in classical type theory, which Tarski has shown to be impossible.