What is the world of mathematics? (Q598279)

This very short paper asks ``What is the world of mathematics'' -- by which is meant \textit{elementary mathematics}, which includes arithmetic and analysis but not metamathematics and category theory. The world of mathematics is taken to be a model of the language of mathematics. The latter might be the category of sets, preferably the Gödel-Bernays variant. But for Lambek it's rather a type theory as defined in the book [\textit{J. Lambek} and \textit{P. J. Scott}, Introduction to higher order categorical logic. Cambridge etc.: Cambridge University Press (1986; Zbl 0596.03002)]. Types, like toposes, form a category: to each topos \(\mathcal{T}\) is associated a type theory \(\text{L}(\mathcal{T})\), its internal language being intuitionistic generally. Conversely, with each type theory (language) \(\mathcal{L}\) is associated a topos \(\text{T}(\mathcal{L})\), the Tarski-Lindenbaum category of \(\mathcal{L}\) (the topos generated by \(\mathcal{L})\). \(\text{L}\) and \(\text{T}\) are a pair of adjoint functors between the category of type theories and the category of toposes. The pure intuitionistic type theory \({\mathcal L}_0\) is the one where types, terms and theorems are freely generated. The free topos \(\text{T}({\mathcal L}_0)\) generated by pure intuitionistic type theory is, in the author's opinion, a suitable candidate for \textit{the} world of mathematics acceptable to members of different philosophical schools, who do not insist on the principle of the excluded middle and who are willing to compromise. One can now formulate Gödel's incompleteness theorem as: Assuming that \(\mathcal{L}\) is consistent and that the set of theorems is recursively enumerable, then it does not suffice to look at \(\omega\)-complete models only.