?
Trakhtenbrot theorem for classical languages with three individual variables
Ch. 19. P. 1–7.
Rybakov M., Shkatov D.
We present a simple proof of Thrakhtenbrot's theorem for the classical predicate logic in the language with only three individual variables. Both forms of Thrakhtenbrot's theorem are established: we prove that the classical predicate logic QCL over finite domains is not recursively enumerable in the language with only three individual variables and that the set of theorems of QCL over arbitrary domains and the set of non-theorems of QCL over finite domains, in the language with only three individual variables, form a recursively inseparable pair of recursively enumerable sets. The techniques used here can be generalised to obtain similar results for non-classical predicate logics with further restrictions on their vocabularies.