Monday, March 25th, 2013 | Author: Konrad Voelkel
This question is not suitable for MathOverflow, as it is inherently vague.
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+!