# Decidability of a set of universal $\mathcal{L}$-tautologies

The following is a problem from an old qualifying exam in logic:

Let $$\mathcal{L}$$ be a finite language consisting only of function symbols. Show that then the set of universal $$\mathcal{L}$$-sentences $$\sigma$$ such that $$\models \sigma$$ is decidable.

An earlier part of the same problem asked for a proof of the following result: If $$\Sigma$$ is a decidable set of $$\mathcal{L}$$-sentences such that, for each $$\sigma \in \Sigma$$, we have $$\models \sigma$$ if and only if $$\mathcal{A} \models \sigma$$ for each finite $$\mathcal{L}$$-structure $$\mathcal{A}$$, then $$\left\{\sigma \in \Sigma : \, \models \sigma \right\}$$ is decidable. My plan of attack is to use this result by defining $$\Sigma$$ to be the set of universal $$\mathcal{L}$$-sentences (in which case $$\Sigma$$ is decidable) and showing that, if $$\mathcal{A} \models \sigma$$ for each finite $$\mathcal{L}$$-structure $$\mathcal{A}$$, then $$\models \sigma$$. However, I have not been able to prove that $$\mathcal{A} \models \sigma$$ for each finite $$\mathcal{A}$$ implies $$\models \sigma$$. Assuming there are arbitrarily large finite $$\mathcal{L}$$-structures, I know from the compactness theorem that there is at least one infinite $$\mathcal{L}$$-structure satisfying $$\sigma$$; why must all infinite $$\mathcal{L}$$-structures satisfy $$\sigma$$? And, what is the importance of the assumption that $$\mathcal{L}$$ consists only of function symbols?

I would argue contrapositively. Assume that a universal statement $$\sigma=\forall x_1\ldots\forall x_n\psi(x_1,\ldots,x_n)$$ fails in some structure $$M$$. We want to show that $$\sigma$$ fails in a finite structure. Pick elements $$m_1,\ldots,m_n$$ such that $$\psi(m_1,\ldots,m_n)$$ fails in $$M$$, and consider the finite set $$M'$$ of $$M$$-interpretations of all terms occuring in $$\psi$$, where $$x_i$$ is assigned value $$m_i$$ (these terms may be the variables $$x_i$$ themselves, but also things like $$f(g(x_k))$$). We want to take this as domain of our desired finite structure. What is left is to define the functions on $$M'$$. If $$f$$ is a function symbol (for simplicity, say a unary one), define $$f$$ in $$M'$$ as in $$M$$ if possible; if the value that the $$M$$-interpretation $$f$$ gives to some argument $$a\in M'$$ lies outside $$M'$$, redefine it arbitrarily. Then $$\psi(m_1,\ldots,m_n)$$ fails in $$M'$$, and therefore $$M'$$ is a countermodel to $$\sigma$$.
Another solution is proof-theoretical: A universal statement $$\sigma=\forall x_1\ldots\forall x_n\psi(x_1,\ldots,x_n)$$ is valid iff $$\psi(a_1,\ldots,a_n)$$ is provable in some proof system such as $$LK$$ ($$a_1,\ldots,a_n$$ are new variables). By cut-elimination, there must be a proof of $$\psi(a_1,\ldots,a_n)$$ without quantifier inferences. But this is then essentially a propositional proof, and proof search in the propositional fragment of $$LK$$ terminates.