Homotopy Theory of Proofs?
Monday, March 25th, 2013 | Author: Konrad Voelkel
This question is not suitable for MathOverflow, as it is inherently vague.
In short:
Is there a Homotopy Theory of Proofs?
Suppose you take two sets of statements A and B, for example A says that some set X and a product on X satisfies the axioms of a group, and B says something about X and the product which is satisfied for any group. There are many ways to prove 
, though we might be inclined to see many of them (if not all) somewhat equivalent. Suppose two proofs are considered equivalent, can you image that there are two different ways to see that/how they are equivalent? This is, very roughly, what I think should a homotopy theory of proofs be.
Statement sets (or just statements?) would be points (0-cells), proofs the arrows/morphisms (1-cells) and equivalences of proofs (whatever that may be) the 2-morphisms (2-cells) and so on, with higher homotopies.
One way to get that rigorous might lie in the syntax: take as statements syntactic statements and as proofs full syntactic proofs. Then one can at least assign to two proofs the Hamming distance, which gives us the structure of a (pseudo)metric space.
My question is: is there anyone out there already working on such stuff? Is there any hope or can you give an argument why that is inherently nonsensical?
My next steps would be to seek more examples of different proofs for the same elementary implications to get some feeling for how the transformations between proofs might look like.
Another idea was to look at Turing machines instead, and take reductions as 2-morphisms. Can you think of anything that goes in that direction?
Why this question isn't suitable for MO:
I didn't even try to do an extensive search in the literature (as I don't really know where to start, not being a logician), I can give no good answer to the question "what would you expect from such a theory to prove/do?" and I don't know what would qualify as acceptable answer(s). Maybe in 1-2 years I will have thought enough about this topic to distill a MO-level question. Up to then, this will have to suffice.
I'll be happy with any input (and I know there are at least 2 people who also like this idea)!
[UPDATE 2013-03-29] Thank you for the comments so far, also on Google+!
2013-03-25 (25. March 2013)
This is something that people do discuss. Tim Gowers speculates about it here and as I recall I think there might have been a few other math blogs talking about this about the same time...
I also have the sense that people interested in homotopy type theory are interested in / partly motivated by this sort of thing, but as far as I've seen (as a bystander), nobody's gone so far as, say, to try to calculate the homotopy groups of the collection of all proofs of Theorem X (except maybe in really trivial cases?). Probably this has to do with the fact that up until now they've still been nailing down the foundations.
In HTT, a boolean-valued proposition like
m =_Z n
(where m and n are integers, say) gets "fibrantly replaced" by a "path space" of "identity paths" from m to n
id_Z(m,n)
The points of this space (= the paths from m to n) are, essentially, the different proofs that m=n. The question, I guess, is what the homotopical structure making it non-discrete consists of. I tentatively believe that this structure essentially amounts to the different notions of proof / similarities between them that one would intuitively want to have in a homotopy theory of proofs, but I'm not an expert and I don't really recall seeing this made explicit anywhere.
Let me say a bit more to substantiate this. The basic thing you talk about in type theory are types, which can basically be thought of as objects in a very nice category like, say, a topos. You also want to talk about propositions, but under the Curry-Howard correspondence, propositions are already types. Under this correspondence, the basic rules of logic out of which you construct proofs of propositions are just instances of basic rules for reasoning with types. For example, conjunction ("and") is seen as an instance of product types, and the basic logical rule "from a & b deduce b" is just an instance of applying the projection map A * B -> B.
So to some extent, the relation of the higher homotopies in HTT to proofs will be like the relation of higher homootpies in homotopy theory to basic categorical operations like products. Of course, in homotopy theory, not every categorical operation works well -- you have to take fibrant / cofibrant replacements to get homotopy pullbacks and pushouts. But the way that the identity types Id_X(x,y) as above are made to behave homotopically (beyond very formal senses, like the ability to concatenate them) is via Voevodsky's Univalence Axiom, which is omplicated enough that it doesn't become obvious to me that everything works out...
I'm clearly well past my limits of knowledgeability, but there's a lot of places online to learn more, including a whole list of them here--I can personally recommend the 3rd one down by Mike Shulman at the nCategory Cafe.
2013-03-25 (25. March 2013)
Thanks to bring the Gowers' article to mind, I very much enjoyed reading it when it was fresh, and I would also recommend it, especially the comment section.
About HTT: I've not yet found time to really learn how it works, and I wasn't sure they really do "homotopy theory of proofs". At least, I was under the impression that such a thing wasn't the motivation behind HTT.
If HTT is the answer to my question, I'll have to learn some type theory now :-)
2013-03-25 (25. March 2013)
In an email from 2011 I wrote myself (apparently) I found these two links:
http://profs.sci.univr.it/~bellin/philo.html
http://www.logic.at/people/hetzl/research/index.html
and the note that the thesis of Stefan Hetzl might be interesting with regards to a homotopy theory of proofs.
2013-03-26 (26. March 2013)
My memory of other blogs talking about this was right: a commenter on the Gowers blog entry links to 3 other blogs talking about this at the same time. I'll reproduce them here:Week 227 of This Week’s Finds
Neighborhood of Infinity
Orange Juice Files
They seem to have been occasioned by this conference on the "geometry of computation".
Interesting -- in the TWF entry, Baez makes the same complaint -- he says he thinks that Voevodsky's work is supposed to be about homotopy of proofs, but nobody's actually said that to him. This was back in 2006.
Baez talks about the basic idea of a "category of proofs" where a morphism is a deduction, which goes back to Lambek in the 1960's. He also links to a couple of papers by Seely which look at extending this to a 2-category. But as far as I can see, the HTT people only reference Seely for his seemingly unrelated work on locally cartesian closed categories and extensive type theory...
The thing is, say that P is a proposition and p is a term inhabiting type P. Then p carries essentially all the information of its derivation/proof. So then if you consider the type \sum_{x:P} Id_P(p,x), it's hard to think what else the homotopy of this type could be encoding besides the sort of "homotopy between proofs"...
2013-03-29 (29. March 2013)
OK, now that I read more about HTT, it really looks like what I asked for, in some sense.
@Tim Campion, thank you!
I would still love to see completely different approaches or ideas, though :-)
2015-06-21 (21. June 2015)
I do not know of any Homotopy Theory of proofs ( and HoTT is not about that!) but I have much more interesting alternative! Homology theory considers objects which has the same borders ( and properties following from homology class - that is basically "number of holes" of dimension d). Sa we start with Hilbert proof system. Proof is taken by carrying modus poens (mp), and in such rule two of sentences gives You third one. So every mp defines a triangle. Then every proof - may be "triangulated" by connecting sentences connected by mp. different triangles - means different uses of mp, but sentences are partially the same ( axioms, proved theorems etc).
So You have functor from "space of proofs" of given theory into triangulable graph space ( use imagination, I know it is vague!).
Given such functor You may ask if two proofs are border of the same "set of holes" of dimension d. And that is precisely - homology structure.
I am thinking about that since a year - and as I am too stupid - without success, but it is striking analogy...
https://fiksacie.wordpress.com/2015/03/08/od-logiki-do-homologii-homologia-odczepiona-oraz-nietrywialne-przyklady/
https://fiksacie.wordpress.com/2015/01/29/co-ma-wieloscian-do-logiki/
2015-06-25 (25. June 2015)
I wish I'd speak your language!
I have some ideas similar to yours, though I'm mostly interested to look at homotopy theory of proofs as a subset of homotopy theory of computation. One day I hope I'll find some time to write up some of these ideas ... but there are more serious projects I also want to pursue.