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.

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.

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:

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 it inside our model. So now M_0 = {1}.

Let us consider, then, the set of all possible binary relations on M_0. Since M_0 has only one element, there are exactly two possible relations: the relation {(1, 1)}, where 1E1 is true, and the empty relation ∅, where instead ¬1E1.

We would like to choose between the two possible relations. To achieve this, we observe that the axiom doesn't only say that 1 exists: it also says that if we substitute 1 for x in the formula ∀y ¬yEx, the resulting formula, ∀y ¬yE1, must be true. This formula, ∀y ¬yE1, we will call a "partial axiom".

Since ∀y refers to every y in M_0, and 1 is in M_0, let us substitute 1 for y, and get the formula ¬1E1. We call such a partial axiom, where all the quantifiers have been eliminated, a "propositional constraint", or just a "constraint" for short.

Having obtained a propositional constraint, we can use it to filter out the relations for which the constraint is false. In this case, the first of the possible relations, {(1, 1)}, does not satisfy the constraint ¬1E1, and therefore we can rule it out. This leaves us with the empty relation as the only possible relation, giving us as model ({1}, ∅).

We are now done with this simple case, having found a model of the axiom of empty set.

The axiom of empty set asserts only the existence of a single object. What if we have an axiom in the form ∀x ∃y ..., for example ∀x ∃y xEy?

Starting where we left off, with M_0 = {1}, we can substitute 1 into ∀x ∃y xEy, getting the partial axiom ∃y 1Ey, and then give a name to the y, choosing 7 arbitrarily. This gives us as propositional constraint 1E7. Now we have M_1 = {1, 7}, and we can substitute into the partial axiom ∀y ¬yE1, giving as result the constraint ¬7E1.

Now we can substitute 7 into our second axiom ∀x ∃y xEy, and we get the partial axiom ∃y 7Ey, which creates a new object which we arbitrarily name 4, and gives us the propostional constraint 7E4. Now M_2 = {1, 7, 4}, and we must now also substitute 4 into every (partial) axiom. We can keep going like this indefinitely, creating objects and partial axioms.

Now, which (partial) axiom we chose to substitute into might have seemed arbitrary. In general, the only hard rule is that we must ensure that for every (partial) axiom which starts with a forall, we must substitute every object we create into it eventually, and for every (partial) axiom which starts with an existential, we must create an object for it eventually.

If we have a countable infinity of axioms, the way to handle it is to only consider the first n axioms at each step n.

Every time we add an object or propositional constraint, we can list all the possible relations on M_i which satisfies all the constraints.

Notice that BA "agrees" with every BA* about every pair of elements taken from M_1, and BC "agrees" with every every BC* for every such pair as well. More precisely, we say that a possible relation E_i agrees with an E_j (where j>=i) if, for any pair p taken from M_i ⨯ M_i, p ∈ E_i if and only if p ∈ E_j.

If j=i+1, then we say that E_i is the "parent" of E_j, and E_j is a "child" of E_i. For example, BA is the "parent" of BAA. Some possible relations have no children: in this case, they are A, BB, and BD, which are incompatible with the constraints ¬1E1 and ¬7E1.

As suggested by the names "parent" and "child", the possible relations for each M_i form a tree. Every time we add an object, new possible relations are created, which are always children of previous relations. And when we add constraints, we eliminate possible relations, cutting branches from the tree.

As it turns out, there exists an infinite path down this tree if and only if the axioms are consistent. What's more, given any infinite path (E_0, E_1, ...) down the tree, if we define M and E as the union of all M_i and E_i respectively, then (M, E) is a model of the axioms.

Knowing this, to program an almost-computable model, it suffices to write a program which chooses an arbitrary path down the tree, and, whenever the branch it's on gets cut, goes back up the tree to the nearest remaining branch and then chooses a new arbitrary path.

Proofs of these assertions are given in the following sections.

We shall now prove that an infinite path exists if and only if the axioms are consistent.

First, we assume that there is no infinite path, and show how to prove a contradiction from the axioms. We will use our example from the previous section to illustrate the procedure.

First, we will add a new axiom, ∀x ∃y yEx, which contradicts the axiom of empty set, in order for our axioms to actually be contradictory. Substituting 1 for x and creating the newly required object which we name 9, we get the partial axiom ∃y yE1 and the constraint 9E1. Then, substituting 9 in the partial axiom of empty set, we get the constraint ¬9E1.

Now M equals {1, 7, 4, 9}, and our constraints are ¬1E1, 1E7, ¬7E1, 7E4, ¬4E1, 9E1, and ¬9E1. These last two constraints are clearly contradictory, so by the completeness of propositional logic, there must exist a proof that their conjunction is false:

(More generally, if there is no infinite path down the tree, there must be some finite step i at which all the possible relations on M_i are eliminated by the constraints. Since the constraints are strictly propositional, and there are only finitely many of them at step i, by the completeness of propositional logic, we can prove that their conjunction is false.)

Now, our objective is to convert the constraints on the left hand side of the implication back into partial axioms, and then those partial axioms back into full axioms. To do this, we start by looking at all the (partial)