Computational models of first-order theories

Most practical first-order theories have no computable models. However, we can relax the definition of "computable" a little bit by allowing the program to backtrack and change its previous output, so long as for each finite subset of its output, it eventually settles on an answer. It turns out that every consistent recursively enumerable first-order theory has "almost-computable" models of this sort, and in this post we will show how such a model can be programmed. Preliminaries For simplicity,...