Algorithmically deciding existence of finite limits in a category

Question

Given $\Sigma$ a consistent finite first order theory in vocabulary $L$, one can consider the category of its models $\mathcal{M}(\Sigma)$, its objects are the models of $\Sigma$ and arrows are exactly $L$-structure homomorphisms.

After fixing a finite index category $J$ we define a decision problem $$P(J)=\{\Sigma \text{ a finite theory}\mid \forall D\in\mathrm{Func}(J,\mathcal{M}(\Sigma))\: \lim D \text{ exists}\}.$$

I want to ask if it's known for which (if for any) $J$ is $P(J)$ decidable (for all consistent $\Sigma$ to avoid Gödel's theorem). E.g. $P(\text{empty category})$ is exactly deciding whether $\mathcal{M}(\Sigma)$ has a terminal object.

(Of course one could also define something as $P^{op}(J)$ which would be deciding if every functor from J to $\mathcal{M}(\Sigma)$ has a colimit, as I don't have much insight into this, I'm not sure if it's important to also consider this dual decision problem.)

Answer 1

No - the undecidability of first-order logic makes it very hard to algorithmically decide anything about the class of models of an arbitrary first-order sentence. In this case, you can reduce the consistency problem for first-order sentences to a family of instances of your problem, just involving consistent sentences.

For simplicity, let's just consider the case of the existence of a terminal object. Let $L$ be any finite relational language with at least one binary relation symbol (so the consistency problem for $L$-sentences is undecidable). Let $L'$ be $L$ together with two new unary relation symbols, $P$ and $Q$.

Now for any $L$-sentence $\varphi$, consider the following $L'$-sentence $\varphi'$: $$(\varphi\land \forall x\, (P(x)\land \lnot Q(x))) \lor (\chi_L\land \forall x\, (Q(x)\land \lnot P(x)))$$ where $\chi_L$ is the sentence asserting that all of the relation symbols in $L$ have trivial interpretation: $\bigwedge_{R\in L} \forall x_1\dots \forall x_{\text{ar}(R)} \lnot R(x_1,\dots,x_{\text{ar}(R)})$.

Now $\varphi'$ is always consistent: for every set $A$, there is a model $M_A$ with domain $A$ in which all of the relation symbols in $L$ are trivial, every element satisfies $Q$, and no element satisfies $P$.

If $\varphi$ is inconsistent, the models above are the only ones, and $\mathcal{M}(\{\varphi'\})$ is isomorphic to the category of sets. In particular, $\mathcal{M}(\{\varphi'\})$ has a terminal object, namely $M_A$ where $A$ is any singleton set. But if $\varphi$ is consistent, $\varphi'$ has more models: take any model of $\varphi$, and expand it so that every element satisfies $P$ and no element satisfies $Q$. In this case, $\mathcal{M}(\{\varphi'\})$ has no terminal object, since there are no morphisms between the two kinds of models. This reduces the problem of consistency of $\varphi$ to the problem of the existence of a terminal object for $\mathcal{M}(\{\varphi'\})$, uniformly for all $L$-sentences $\varphi$.

Very similar arguments will work to show that instances of this problem for other kinds of limits and colimits are also undecidable. For example, the exact same construction works for initial objects, products, and coproducts, but you'd need to use a slightly different argument for equalizers and coequalizers.