Thu Nov 29, 2012, 02:07 AM
bananas (27,509 posts)
Freedom From Logichttp://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html
November 9, 2012 Freedom From Logic Posted by Mike Shulman One of the most interesting things being discussed at IAS this year is the idea of developing a language for informal homotopy type theory. What does that mean? Well, traditional mathematics is usually written in natural language (with some additional helpful symbols), but in a way that all mathematicians can nevertheless recognize as “sufficiently rigorous” — and it’s generally understood that anyone willing to undertake the tedium could fully formalize it in a formal system like material set theory, structural set theory, or extensional type theory. By analogy, therefore, we would like an “informal” way to write mathematics in natural language which we can all agree could be fully formalized in homotopy type theory, by anyone willing to undertake the tedium. Peter Aczel was the initial advocate of such a thing here, and I think it’s a great idea. Given that computer proof assistants are not really yet sufficiently automated to make formalization of nontrivial arguments palatable to the average mathematician — a situation which I think it will probably take a few decades to overcome, at least — in order for homotopy type theory to make real headway as a foundation for mathematics in the near future, we need a way to do it without computers. <snip> Finally, in everyday mathematics, not all the “propositions” we prove are naturally (1)truncated! Once my eyes were opened to this, I started to see it everywhere. Most classical mathematicians are deeply programmed to think of proofs as containing no content, in the sense that once you prove a theorem it doesn’t matter what the proof was (a type theorist calls this “proof irrelevance”). But actually, in doing ordinary mathematics it happens to me all the time that I end up writing “by the proof of Lemma 9.3”, because what matters is not just the statement of Lemma 9.3 but the particular proof of it that I gave. <snip> Just as intuitionistic logic is more expressive than classical logic because it doesn’t force us to assume the law of excluded middle (but allows us to assume it as an additional hypothesis like any other hypothesis), type theory is allowing us to see a further distinction which was invisible to the classical mind: we aren’t forced to (1)truncate all theorems (but we are allowed to, if we so desire, by simply applying the truncation operator). <snip> With all the above in mind, I think what I would really like to do is to make a clean break by expunging the notion of “proposition” from the language. In other words, there are only types. Some types are (1)truncated. Some types are ntruncated. Some types belong to other modalities. Sometimes we can construct a term in a given type as it stands. Other times we can only construct a term in some truncation of it, or in its reflection into some other modality. (For instance, this is quite a common occurrence for the “classical logic” modality.) <snip>

4 replies, 1209 views
Always highlight: 10 newest replies  Replies posted after I mark a forum
Replies to this discussion thread
4 replies  Author  Time  Post 
Freedom From Logic (Original post) 
bananas  Nov 2012  OP 
Warpy  Nov 2012  #1  
bananas  Dec 2012  #3  
DetlefK  Nov 2012  #2  
tama  Dec 2012  #4 
Response to bananas (Original post)
Thu Nov 29, 2012, 02:25 AM
Warpy (106,542 posts)
1. This looks like something else written using LISP
which was a gag program in the early 80s that you'd plug a few keywords into and then let it generate page after page of bafflegab that looked like it should make sense but didn't.

Response to Warpy (Reply #1)
Wed Dec 5, 2012, 01:56 AM
bananas (27,509 posts)
3. Nah, it was written by a human
He's one of the hosts of the nCategory Cafe,
here's his webpage: http://www.math.ias.edu/~mshulman/ 
Response to bananas (Original post)
Thu Nov 29, 2012, 09:54 AM
DetlefK (16,376 posts)
2. He wants to invent a new mathematical language that can be translated into everydaylanguage...
I think that's a bad idea. Our natural languages aren't very precise. For example there are numerous exceptions to any rule in the grammar/algebra of a natural language.
Take chinese for example. (A chinese coworker explained this to me.) The chinese language is very old, but rigid in terms of structure. Short sentences are ambiguous (due to an underdeveloped grammar) and have to be explained by context. Additionally, there are many words that sound almost alike, which makes it sometimes necessary to "write" the word with a gesture to make clear what you are meaning. 
Response to DetlefK (Reply #2)
Wed Dec 5, 2012, 04:03 AM
tama (9,137 posts)
4. This belongs to category theory approach to math
Which is alternative to set theory as foundation of math. There is informal language to describe set theory (shorts for theory dependent settheoretical mathematical structures). And the want to depelope functionally similar informal language to discuss homotopy type theory /(∞,1)categorytheoretical mathematical structures. See also http://golem.ph.utexas.edu/category/2011/03/homotopy_type_theory_i.html
http://plato.stanford.edu/entries/categorytheory/ 