natural metrics for proof length

I am trying to make my way into Homotopy Type Theory(HoTT) where a mathematician may view proofs as paths. Intuitively, this leads me to the idea of a metric on the space of mathematical propositions. Has this been developed?

Specifically, is there a way to analyse short proofs as geodesics within the space of mathematical propositions from the perspective of HoTT? If so, might this metric be formulated using Kolmogorov Complexity?

• Usually logicians analyze mathematical propositions by their equivalence classes instead, sometimes coarsely (eg the five subsystems of second-order arithmetic in reverse mathematics), sometimes more finely (eg the hierarchy of consistency strength in set theory). Aug 11 '20 at 20:31

The notion of length is related to distance and metric, and these are all concepts that topology obliterates, let alone homotopy theory. The popular explanations of homotopy type theory in terms of topological paths (continuous maps $$[0,1] \to X$$) are meant to help the intuition, but should not be and cannot be understood literally. Topological spaces do not form a model of homotopy type theory.

Since you are trying to make your way into homotopy type theory, you could draw your intuition from several places, depending on your background, in decreasing order of abstraction and correctness:

1. Higher category theory: an $$(\infty,1)$$-topos is more or less a model of homotopy type theory, while an $$\infty$$-groupoid is like a single type.

2. Homotopy theory: Simplicial sets, and more precisely Kan complexes form a model of homotopy type theory, so you can think of a type as a Kan complex. In general, certain kinds of model categories can be used to interpret (parts of) homotopy type theory.

3. Groupoids: a groupoid is like a 1-type in homotopy type theory. You can think of $$\mathsf{Id}_A(a,b)$$ as the collection of all isomorphisms from $$a$$ to $$b$$ in a groupoid $$A$$.

In all cases, the "paths" are of an abstract nature. For instance, the isomorphisms in a groupoid need not be paths, just like morphisms in a category need not be functions.

There are adaptations of homotopy type theory that do relate the abstract homotopy-theoretic models with topological, and even smooth models. These go under the name cohesive homotopy type theory, but I am not sure that's the best starting point for learning homotopy type theory.

Let me attempt a longer answer. (@Andrej Bauer 's answer is mostly about learning homotopy type theory, as opposed to delving deeper into your question.)

Unsurprisingly, the answer is still no. One could try to define the length of a path by the size of the smallest of its witnesses. But that definition relies on syntax, i.e. you need to have a 'language' in which you express your witnesses. The thing is, while HoTT does give rise to programming languages rather naturally (see my work with Amr Sabry), they still are not really 'canonical'. While $$\left(\infty,1\right)$$-topos certainly point in the right direction, it's not settled yet if we don't in fact want a bit more structure (see the work of Shulman, Riehl, etc if you want to dive in the really deep end of that). So we don't even know what outer structure to work in, never mind the internal language that we'll end up having inside that structure.

Even if all of that settled down, why would you expect the internal language to be Turing-complete? That is one of the cornerstones of the validity of Kolmogorov Complexity. Without it, length becomes a rather whimsical notion. Even with Kolmogorov Complexity, length remains a 'fuzzy' notion, because it's only defined up to a constant. So even if it existed, it would not tell you much about 'short' proofs, it only really tells you something interesting when you have one proof which is significantly shorter than the others. Certainly there is no hope that such a length notion would be a metric, never mind carve out geodesics.

Nevertheless, I do hold out some hope that there will be some notion of 'size' that will turn out to be informative and meaningful. It's just not going to be simple, or as informative as one would like.

• “Without it, length becomes a rather whimsical notion.” I don’t think that’s true. Take the problems of minimizing DFAs, NFAs, and regular expressions, which are certainly valid problems that are studied in the literature. Aug 12 '20 at 19:41
• @user76284 That would be because when analysing DFAs, etc, there is a fixed and adequate meta-language in which length is measured. There is a kind of shift that happens as the computing power gets larger, and some things become undecidable. Size becomes an unstable measure. Aug 13 '20 at 13:16
• I think the binary lambda calculus could play that role. Indeed it was invented for that reason (concrete AIT). Aug 13 '20 at 19:34
• @user One problem with using a coding of the lambda calculus is that 'coding' arithmetic is usually very inefficient, even from the point of view program length. Adding binary-coded naturals makes some programs exponentially shorter. So Kolmogorov-short programs will inevitably end up re-inventing such things for brevity. Aug 14 '20 at 15:08