Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof / 2 / e

By part (c), $T$ has a first-order model, so it is consistent. By part (d), every first-order sentence is equivalent modulo $T$ to a quantifier-free sentence. In the first-order signature consisting only of $E$ and first-order equality, there are no constant symbols, no ground first-order terms, and no nullary predicates. Thus a closed quantifier-free formula reduces to true or false, using the logical truth constants. All first-order models of $T$ therefore agree on every first-order sentence:

The construction in part (d) is effective. Conversion to disjunctive normal form, enumeration of finite equality partitions and adjacency patterns, and testing the finitely many witness cases are all terminating operations. Apply them recursively to a given first-order sentence and evaluate the final truth constant. This decides whether the first-order sentence belongs to $T$, givingNo useful bound on the running time is needed for decidability; the potentially large enumeration still always terminates.