I’m cutting loose the “internal language” strand of the Gordian knot of the “No Comment” comment section. Here is David Corfield’s last contribution:
Regarding this ‘internal language’ issue, Michael, did you read nLab’s page ‘internal logic’ (http://ncatlab.org/nlab/show/internal+logic). It’s far from perfect, but hopefully it conveys the gist of the idea that inference systems come in different strengths, that to a system there corresponds settings which ‘support’ that reasoning, and so that inferences within a given system can be interpreted in any example of the corresponding setting.
So, for example, if you have a rich enough logic in which to define the concept of the reals, symmetric matrices and diagonalization, and to prove some result about diagonalization, you could look for suitable interpretations. Someone (I think Scedrov here http://www.sciencedirect.com/science/article/pii/0168007286900060) showed you could do something of this sort constructively, so in the kind of language that is internal to toposes. He could then interpret his argument in any topos, such as the topos of sheaves over the reals where it gives a result about diagonalizing matrices of continuous functions.
Now If HoTT is the internal language of infinity-toposes, any proof in HoTT has an interpretation in any infinity-topos.
Indeed I tried to read the section on “internal logic” at nLab, and had my usual experience: after at most 3 lines I am referred to another page for a term I don’t know, the same thing happens on the second page, and so on until I either reach a dead end or return to my starting point. I have very rarely learned anything at nLab and I draw the conclusion that it was not designed for people with my basic understanding of mathematics.
Before I continue, I want to build on the “linguistic” metaphor I used in an earlier comment. Although the architectural imagery underlying the “Foundations” metaphor persists in Bourbaki’s Architecture of Mathematics text, the imagery of communications is more appropriate to account for Bourbaki’s actual accomplishment, which was to provide a common language for most central branches of mathematics. For a variety of historical reasons, Bourbaki chose to base the common language on the dialect of algebra, just as the national language of Italian unity was based on the Florentine dialect. Until David’s comment, I was under the impression that nLab was written in a completely different language (Albanian, for example), but having read his explanation, I now recognize it as (a logically-inflected variant of) the dialect of homotopy theory. In this optic, the proposal to adopt HOTT/UF as a new foundation for mathematics is analogous to the proposal to replace the Florentine dialect by the Neapolitan dialect as the national language of Italy. This would be disorienting in the short term — imagine the BBC instructing its news anchors that they are henceforth to speak in Glasgow dialect — but might bring benefits (preserving the Union, say, in the BBC example).
(Here is a traditional Neapolitan song about the natural numbers. Giuseppe Peano, however, was Piemontese.)
The nLab page on infinity topoi is not very informative, but I found Jacob Lurie’s 2003 article on the subject on the arxiv, and I’m pretty sure I could make sense of that if I needed to (with the help of a pidgin). As a number theorist I have never actually had to use a topos as such, except when I wanted to look inside the black box of some theory of cohomology of schemes, which is practically never. This may well change in the near future, because of the work of Peter Scholze and his collaborators, and especially the introduction of the proétale topology by Scholze and Bhargav Bhatt.
This represents the highest level of topos-theoretic sophistication attained by (large groups of) number theorists in quite some time, but the following excerpt from the notes to Scholze’s course last fall in Berkeley may come as a revelation to those who assume mathematics is not divided into dialects.
We are going to use the fact that in a topos, taking fibre products commutes withcolimits .
Jacob’s latest, extremely helpful, comment arrived as I was finishing the above nonsense and is copied below, in order to keep the thread separate. I’ll probably comment on this later, but in the meantime I’ll return to my planned weekend with my family.
Regarding the meaning of the term “internal language”: I’d prefer to phrase it as a distinction between “syntactic” and “semantic” ways of thinking, and it’s a distinction that one could make for reasoning about much more familiar objects.
So, for example, suppose I wanted to prove a theorem about groups. Let me distinguish between two “styles” in which such a proof could be understood:
a) In the “syntactic” style of first-order logic. A proof in this sense consists of a sequence of sentences in the first-order language of groups (meaning they are formal expressions built out of “and”, “or”, “for all”, etcetera), each of which is required to either be an axiom of group theory or to obtained from previous elements of the sequence using a rule of inference.
b) In the “semantic” style, the way that mathematics is usually practiced. Here we imagine that we have a group and we use whatever tools we like in order to study it and draw the conclusion that we want. So we might use concepts that can’t be formulated in the first-order language of groups: for example, we might draw conclusions about G by studying subgroups of G, or linear representations of G, or ideals in the group ring Z[G].
Godel’s completeness theorem asserts that any first-order statement about groups is provable in the syntactic sense if and only if it is true in all groups. So for such statements, any theorem that can be proven “semantically” can also be proven “syntactically” (the fine print, of course, is that this applies only to statements which can be formulated in the first-order language of groups. So, for example, it tells you nothing about theorems which concern -finite- groups, since the finiteness of a group is not a hypothesis that can be formulated in the first-order language of groups).
I think that the debate that Mike and I were having above was about the utility of these two different approaches for thinking about a different sort of mathematical structure (an “elementary infinity topos”). Homotopy type theory can be viewed (and I think Mike will endorse this?) as an approach to formulating and proving theorems about these objects in the “syntactic” style (with the caveat that it is not the syntax of first order logic, but of type theory). My skepticism is about whether this approach can really have substantive advantages over the “semantic” style for the purpose of proving theorems (ignoring issues related to computer verification of proofs or philosophical objections to using transcendental methods to study something that is supposed to be foundational).