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?
Best Answer
This is a good example of a situation where Ehrenfeucht-Fraisse games are quite useful. I claim that in fact the general satisfiability problem for this language - that is, the problem of whether an arbitrary sentence in the language is satisfiable - is decidable; since your theory is finitely axiomatized, its decidability also follows since your theory proves a sentence $\theta$ iff the sentence $\psi\wedge\neg\theta$ is unsatisfiable where $\psi$ is the conjunction of the axioms in your theory.
Note that if $\mathcal{M}$ is a structure in your language, then $\mathcal{M}$ is completely determined by $2^n$ numbers, namely how many elements satisfy each of the Boolean combinations of the $P_i$s. Put another way, an element $a$ of $\mathcal{M}$ is determined up to "automorphism orbit" by $\{i: P^\mathcal{M}_i(a)\}$, and there are only $2^n$ many possible such sets.
This suggests that something like your equality-only analysis might also work here: that since there are only a fixed number of "possible behaviors," for every sentence $\sigma$ we can effectively find a number $n$ such that if $\sigma$ is satisfiable then it has a model of cardinality $\le n$. We can prove this with some syntactic work, or - much more slickly - via EF-games:
Let $Struc(m_1,..., m_{2^n})$ denote the unique-up-to-isomorphism structure with $m_k$-many elements in the $k$th Boolean combination of the $P_i$s. (Here the $m_k$s are allowed to be infinite.) Note that every structure in your language is isomorphic to exactly one of this form.
Given a structure $\mathcal{M}$ and a number $k$, let $\mathcal{M}[n]=Struc(\max\{k, m_1\}, ..., \max\{k, m_{2^n}\})$ where $\mathcal{M}=Struc(m_1,..., m_{2^n})$.
Now show that regardless of what $k$ is, Duplicator wins the game $EF_k(\mathcal{M},\mathcal{M}[k])$.
Finally, show that the previous bulletpoint implies that any satisfiable $k$-quantifier sentence has a model of size at most $k2^n$.