What is the world of mathematics?
type: Item
instance of: scholarly article
title: What is the world of mathematics?
zbMATH Open document ID: 1076.03044
published in: Annals of Pure and Applied Logic
publication date: 2004-08-06T00:00:00Z
review text: 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.
reviewed by: Michel Eytan
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18B25
Mathematics Subject Classification ID: 03E30
Mathematics Subject Classification ID: 03F55
zbMATH DE Number: 2083178
zbMATH Keywords: language of mathematics
zbMATH Keywords: category of sets
zbMATH Keywords: local toposes
zbMATH Keywords: free topos
zbMATH Keywords: intuitionistic type theory
zbMATH Keywords: elementary mathematics
MaRDI profile type: Publication
full work available at URL: j.apal.2003.10.014
OpenAlex ID: W2033086528
cites work: Sheaf representation for topoi
cites work: Q5571677
cites work: Q5812175
cites work: Are the traditional philosophies of mathematics really incompatible?
cites work: Q4749837
cites work: Q3727946
cites work: Q4003736
cites work: Q3240239
cites work: Q4231666
cites work: Q5573940
DOI: 10.1016/J.APAL.2003.10.014
author: J. Lambek
description: scientific article; zbMATH DE number 2083178