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

Question

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?

Answer 1

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.