Let $\mathcal C$ be an $\infty$-category. We can ask:
Q: Is $\mathcal C$ a 1-category?
That is, are the hom-spaces of $\mathcal C$ essentially discrete?
Roughly, my question is:
Proto-Question: Is Q decidable?
Presumably the answer is going to depend a lot on how we make Q precise. I am not a computability theorist, so I’m not sure what is the best way to approach making it precise.
First pass: We might encode $\mathcal C$ as a quasi-category — a simplicial set satisfying certain “lifting conditions”. We might assume for simplicity that $\mathcal C$ has countably many simplices, and assume we are given an algorithm which enumerates a list of names for the $n$-dimensional simplices of $\mathcal C$ for each $n \in \mathbb N$, and an algorithm which computes the face and degeneracy maps between them. It then appears to be a well-posed question to ask: is $\mathcal C$ (presented in this way) a 1-category?
Answer: Clearly (and uninterestingly) no -- for instance let $\mathcal C$ have two objects $a,b$, with $Hom(a,a) = \{id_a\}$, $Hom(b,b) = \{id_b\}$, $Hom(b,a) = \emptyset$, and $Hom(a,b) = BG$ where $G$ is a group defined by a presentation for which it’s undecidable if $G$ is trivial. Then we can’t decide whether $\mathcal C$ is a 1-category, since that would mean deciding whether $BG$ is contractible, which would mean deciding whether $G$ is trivial.
Question: Is there a reasonable way to “precisify” the Proto-Question into a precise question with an interesting answer? Are there many such ways? If so, are the answers in each case fundamnetally similar? Or is the answer fundamentally dependent on the precisification?
My guess would be that basically, in order to turn the proto-question into something with an interesting answer, you need to drastically restrict the class of $\infty$-categories $\mathcal C$ under consideration, to the point where you can build up a theory tailored to your set of restrictions. At any rate, I believe this is how things work in group theory or number theory or manifold theory — once the central decision problem of the field is shown to be undecidable, we really must give up on the idea of “general” approaches to the decision problem, and instead explore one class of special cases after another, each with a different set of tools that resist generalizatoin. My sense is that this is a universal fact about undecidable problems — they cannot be approximated by decidable ones.