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, we will restrict ourselves to models of first-order set theories without equality, and later show how to generalize the approach to arbitrary (recursively enumerable) first-order theories. The language of set theory includes quantifiers ∀ (forall), ∃ (exists), logical connectives ∧ (and), ∨ (or), and ¬ (not), any countable number of variables, and a single binary predicate E. All axioms are assumed to have been rewritten in prenex normal form (in other words, with all the quantifiers at the start of the sentence). We restrict ourselves to models (M, E) where M is a subset of the natural numbers, and E is a subset of M ⨯ M. A computable model is a computable set of natural numbers M and a program which prints out, for every pair of elements x,y ∈ M, either xEy or ¬xEy. An almost-computable model is the same as a computable model, except that the program is allowed to go back and change what it has printed, so long as for every n, there exists a finite number of steps t such that the first n pairs in its output will never be changed again after t steps have passed. A simple case Since we are trying to build an almost-computable model of some axioms, we shall start by looking at an axiom. Here is the axiom of empty set, commonly found in many set theories: ∃x ∀y ¬yEx Let us look at what the axiom says: there exists an x such that for every y, the pair (y, x) is not in E. Since this says that there exists something, let us give that something a name. We will call it 1, and put i