Undecidability of contractibility

In the last post, we discussed Voevodsky’s homotopy type theory. One of the important notions is whether a space is contractible, this being the base case for the inductive definition of homotopy levels. It turns out that the algorithmic undecidability of whether a finite simplicial complex is contractible appears not to have been discussed much, the result instead buried in Appendix A of an arXiv paper. The strongest version of the result is:

• It is undecidable to determine whether a finite 4-dimensional simplicial complex is contractible or not.

An analogous result about fundamental groups, also worth mentioning, can be proved immediately from the undecidability of the word problem in groups:

• It is undecidable to determine whether a finite 2-dimensional simplicial complex is simply-connected or not.

(Proof: we can consider the presentation complex of any finitely-presented group G, where we take a single point, together with a loop for every generator, and a disc for every relator. This has fundamental group isomorphic to G. After two successive applications of barycentric subdivision, we obtain an abstract simplicial complex homotopy-equivalent to the original presentation complex.)

Clearly, the ‘2’ in the second theorem cannot be lowered; a 1-dimensional simplicial complex is a graph, and it is easy to verify whether or not it is a tree (equivalent to both contractibility and simply-connectedness). I believe it is unknown as to whether the ‘4’ in the first theorem can be lowered to 3 or even 2.