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 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.

Handling unlimited objects

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.

Tree of possible relations

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

For M_0 = {1}, before we add any constraints, our possibilities are:

A: {(1, 1)}
B: ∅

For M_1 = {1, 7} with constraints ¬1E1 and 1E7 we have these possibilities:

BA: {(1, 7)}
BB: {(1, 7), (7, 1)}
BC: {(1, 7), (7, 7)}
BD: {(1, 7), (7, 1), (7, 7)}

For M_2 = {1, 7, 4} with constraints ¬1E1, 1E7, ¬7E1, 7E4, and ¬4E1, these are our possibilities:

BAA: {(1, 7), (7, 4)}
BAB: {(1, 7), (7, 4), (4, 4)}
BAC: {(1, 7), (7, 4), (4, 7)}
BAD: {(1, 7), (7, 4), (4, 4), (4, 7)}
BCA: {(1, 7), (7, 7), (7, 4)}
BCB: {(1, 7), (7, 7), (7, 4), (4, 4)}
BCC: {(1, 7), (7, 7), (7, 4), (4, 7)}
BCD: {(1, 7), (7, 7), (7, 4), (4, 4), (4, 7)}

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.

Completeness and model existence

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

First direction

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:

(¬1E1 ∧ 1E7 ∧ ¬7E1 ∧ 7E4 ∧ ¬4E1 ∧ 9E1 ∧ ¬9E1) → 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) axioms which begin with a forall, such as ∀y ¬yE1. By using the introduction rule for forall, we can transform every conjunct created directly by such a (partial) axiom, such as ¬9E1, directly back into ∀y ¬yE1. This is the result of applying this procedure in our example:

(∀y ¬yE1 ∧ 1E7 ∧ ∀y ¬yE1 ∧ 7E4 ∧ ∀y ¬yE1 ∧ 9E1 ∧ ∀y ¬yE1) → false

Since multiple conjuncts are identical, they can be combined into one by the idempotent law of conjunction:

(∀y ¬yE1 ∧ 1E7 ∧ 7E4 ∧ 9E1) → false

Now, if not all objects have been eliminated (as in our example), there must exist at least one object which appears in exactly one conjunct, and for which the conjunct was created by the same (partial) axiom as this object. In our example, 7E4 is the only conjunct which contains 4, and both the conjunct and 4 itself were created by the same partial axiom ∃y 7Ey, so 4 is a valid choice. 9 would also be a valid choice.

There must always exist such a choice, because the objects can be given a partial order based on which ones were used to create which ones, where "used to create" means "appears in the partial axiom that created it". So, in our example, the partial order would have 1 > 7 > 4, and 1 > 9. This partial order must always have a minimal element, since we have only finitely many objects and there can be no loop.

Such a minimal element does not necessarily appear in just one conjunct at first. For example, originally 9 appeared in two conjuncts in our example. But it can only appear in another conjunct if it was substituted into another (partial) axiom, in which case it must have been eliminated in our previous step, when we looked at all (partial) axioms starting with forall.

By the existential instantiation rule, we can transform either of these choices into existential quantifiers. To save time, we now do both 4 and 9 at once:

(∀y ¬yE1 ∧ 1E7 ∧ ∃y 7Ey ∧ ∃y yE1) → false

Now the procedure is just to repeat the same steps we did earlier, until all objects have been eliminated. So first, using the introduction rule for forall, we obtain the following:

(∀y ¬yE1 ∧ 1E7 ∧ ∀x ∃y xEy ∧ ∀x ∃y yEx) → false

Now 7 occurs in exactly one conjunct (and was created by the same partial axiom as that conjunct), so we can eliminate it using existential instantiation:

(∀y ¬yE1 ∧ ∃y 1Ey ∧ ∀x ∃y xEy ∧ ∀x ∃y yEx) → false

Now we apply the forall rule yet again and eliminate duplicate conjuncts:

(∀y ¬yE1 ∧ ∀x ∃y xEy ∧ ∀x ∃y yEx) → false

And with one final application of existential instantiation, we get a proof that the axioms are contradictory:

(∃x ∀y ¬yEx ∧ ∀x ∃y xEy ∧ ∀x ∃y yEx) → false

This shows that if there is no infinite path, we can find a proof of contradiction using the axioms.

Second direction

For the other direction, we assume that there is an infinite path, and show that in this case there cannot be a contradiction in the axioms. To do this, we will show that the limit of any infinite path must be a model of the axioms.

Our approach will be to do induction on the number of quantifiers in (partial) axioms, to show that all the axioms must be true for any (M, E) obtained as the limit of an infinite path.

First, let us consider the base case, when n=0 (there are no quantifiers). In this case, we have a propositional constraint φ. Choose the step i where the constraint φ was added. Every E_j with j>=i must satisfy φ, because otherwise it would have been ruled out by φ. And no E_k k<i can disagree about φ, because by the definition of a path in the tree, every step must either agree with every other step, or say nothing if the objects involved hadn't been created yet. Therefore φ must be true in (M, E).

Second, we will show that any (partial) axiom ∃y φ(y) must be true if every partial axiom with fewer quantifiers is true. Since ∃y φ(y) is a (partial) axiom, we must have created some object O and constraint φ(O) at some point in our procedure. For example, earlier we created 7 from the partial axiom ∃y 1Ey, which produced the constraint 1E7. Since φ(O) is a (partial) axiom with fewer quantifiers, by hypothesis it must be true, and therefore ∃y φ(y) must also be true in (M, E).

Third, for any (partial) axiom ∀x φ(x) which starts with a forall, we will show that it must be true if every partial axiom with fewer quantifiers is also true. A forall is true if all its substitutions instances are true. For example, ∀x ∃y xEy is true if and only if ∃y 1Ey, ∃y 7Ey, etc, are all true. Since these are all partial axioms with fewer quantifiers, by hypothesis they are all true, and therefore ∀x φ(x) must also be true in (M, E).

This completes the induction, showing that all the axioms must be true in (M, E).

To fully complete this proof, it would be necessary to show that the existence of a model implies that the axioms are consistent. This can be done by checking that the axioms of predicate logic are true in any model, and that the rules of inference preserve truth, thereby allowing us to conclude that the axioms cannot prove a contradiction. We leave it to the reader to check such things if they so desire, using their preferred axiomatization of predicate logic.

Almost-computable models

As was stated earlier, 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.

As it goes down the tree, it must be programmed to output xEy or ¬xEy whenever the branch it's on says so. Whenever it backtracks, it must go back and correct any output which has changed in the new branch.

As the program goes down the tree, at each step i, it is given finitely many branches to choose from. When the program backtracks to i, that must mean that one of the branches of i were cut, because it always backtracks as little as possible. But since i has only finitely many branches, they cannot all be cut down unless the axioms are inconsistent. Therefore, the program will backtrack to i at most finitely many times.

Since the first n pairs of the output can only include finitely many objects N ⊆ M, there must exist an M_i such that N ⊆ M_i. When the program reaches the point where it will never backtrack to M_i again, it will never change the first n pairs again.

This completes the proof.

Generalizing to other first-order languages

It is a standard fact that any recursively enumerable first-order language can be converted into one where all functions and constant symbols are replaced with predicates. We will not show how to do so here. If the language treats equality specially, equality can be turned into just another relation by adding the required equality axioms.

After the language has been transformed in these ways, the procedures in this post can be adapted straightforwardly to work on these relations instead of E.

Equality

It should be noted that the models created using this procedure may have more than one copy of the "same" object. For example, there might be more than one object encoding the empty set. These objects, however, will be indistinguishible to the language, and, if an equality predicate with the appropriate equality axioms is included, they will be considered equal by that predicate.

Nonstandard models

It should also be mentioned that for any set of axioms at least as strong as peano arithmetic, every almost-computable model will have nonstandard natural numbers. We will not give a thorough proof of this, but it follows from the fact that the truth predicate of every almost-computable model of PA is definable in PA. Using this, one can construct a sentence similar to the liar sentence, which in this instance forces the model to be nonstandard.

Philosophy

Existence of models

People often talk about models of theories like ZFC as though they are very far away things that only perhaps exist in the platonic realm. Given that it is possible to write a program that approximates a model to arbitrary precision, it seems to us that so long as ZFC is consistent, models of ZFC are in fact very real, even if we take a physicalist point of view.

Reasoning about infinities

When using our procedure on the axioms of ZFC, the axiom of infinity creates an object which in the final model will be the set of all natural numbers, and when we substitute this object into the axiom of powerset we create an object which in the final model will be the powerset of the set of natural numbers.

Even though in ZFC these objects are infinite, and in the latter case, uncountable, at every step of our procedure, they will only ever contain finitely many objects.

We observe that when we, the authors, reason about things such as the powerset of the natural numbers, we do something quite similar to what our procedure does. We imagine an object which we say is the powerset, but which at any point will only ever contain a finite amount of other objects. From this we conjecture that when humans reason about infinities, we do so by creating finite approximations of models of those infinities.

Prior Work

Not much, and probably none, of what is in this post is really new.

Notes

The term "almost-computable" was made for the purpose of this post, and is (probably) not the same thing as other notions of "almost computable" which might be found in the literature.