Let the signature have $n$ unary predicate symbols $P_1, \dots, P_n$ and a single binary predicate $=$. Consider the theory of equality with the following axioms:
- $\forall x (x = x)$
- $\forall x \forall y (x = y \rightarrow y = x)$
- $\forall x \forall y \forall z (x = y \land y = z \rightarrow x = z)$
- For each $i$, $\forall x \forall y (x = y \land P_i(x) \rightarrow P_i(y))$.
Is the set of formulas of this theory decidable?
The solution is somewhat intuitive if the predicates are omitted. In this case it's fairly easy to show that
- all [normal] models with domains of the same power are equivalent, and,
- for a closed formula that is $k$ quantifiers deep, all models having more than $k$ elements are equivalent.
Given this, for a formula that is $k$ quantifiers deep it's sufficient to check some $k + 1$ normal models with domains of $1, \dots, k + 1$ elements respectively. If the formula is true in all of those, then it's true in every model of the theory, then it's deducible, otherwise it's not. So, we got an algorithm, and thus the set in question is decidable!
But how to prove this considering the unary predicates?