Freedom From Logic

http://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 n-truncated. 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>