Language about language

Mathematics without Apologies, by Michael Harris

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…

View original post 1,002 more words