Theorems of Church and Trakhtenbrot

Stephen G. Simpson

First draft: November 5, 2001 This draft: April 8, 2011

1 Describing a Run of a Program

Let P be a register machine program. Let R_{1}, …, R_{s} be the registers that are used in P. We imagine the registers as boxes which hold a finite number of marbles. Let I_{1}, …, I_{l} be the instructions of P. Each of I_{1}, …, I_{l} is either an increment instruction (add one marble) or a decrement instruction (branch on empty, remove one marble). We assume that P starts by executing instruction I_{1} at time zero. We assume that time is discrete and linearly ordered. Let I_{0} be a stop instruction. We assume that time stops if and when I_{0} is reached.

We are going to write a predicate calculus sentence A_{P} which describes a run of P. To write our sentence, we use a language with the following s + l + 7 predicates:

Ixy: x is identical to y

T x: x is a time instant

Zx: x is time instant zero

Lxy: x and y are time instants and y is later than x

Nxy: x and y are time instants and y is immediately after x

Mx: x is a marble

R_{i}xy: marble x is in box R_{i} at time y, for 1 ≤ i ≤ s

I_{m}x: instruction I_{m} is executed at time x, for 0 ≤ m ≤ l

Let A_{P} be the conjunction of the following axioms:

1. identity axioms:

(a) ∀x Ixx

(b) ∀x ∀y (Ixy ⇒ ∀z (Ixz ⇔ Iyz))

(c) ∀x ∀y (Ixy ⇒ ∀z (Izx ⇔ Izy))

(d) ∀x ∀y (Ixy ⇒ (T x ⇔ T y))

(e) ∀x ∀y (Ixy ⇒ (Zx ⇔ Zy))

(f) ∀x ∀y (Ixy ⇒ ∀z (Nxz ⇔ Nyz))

(g) ∀x ∀y (Ixy ⇒ ∀z (Nzx ⇔ Nzy))

(h) ∀x ∀y (Ixy ⇒ ∀z (Lxz ⇔ Lyz))

(i) ∀x ∀y (Ixy ⇒ ∀z (Lzx ⇔ Lzy))

(j) ∀x ∀y (Ixy ⇒ (Mx ⇔ My))

(k) ∀x ∀y (Ixy ⇒ ∀z (R_{i}xz ⇔ R_{i}yz)) , for 1 ≤ i ≤ s

(l) ∀x ∀y (Ixy ⇒ ∀z (R_{i}zx ⇔ R_{i}zy)) , for 1 ≤ i ≤ s

(m) ∀x ∀y (Ixy ⇒ (I_{m}x ⇔ I_{m}y)) , for 0 ≤ m ≤ l

2. structural axioms:

(a) ∀x (Mx ∨ T x)

(b) ¬ ∃x (Mx ∧ T x)

(c) ∀x ∀u (R_{i}ux ⇒ (Mu ∧ T x)) , for 1 ≤ i ≤ s

(d) ¬ ∃x ∃u (R_{i}ux ∧ R_{j}ux) , for 1 ≤ i < j ≤ s

(e) ∀x ∀y ((T x ∧ T y ∧ ¬ Ixy) ⇔ (Lxy ∨ Lyx))

(f) ∀x ∀y ∀z ((Lxy ∧ Lyz) ⇒ Lxz)

(g) ∀x ∀y (Nxy ⇔ (Lxy ∧ ¬ ∃z (Lxz ∧ Lzy)))

(h) ∀x (T x ⇔ (I_{0}x ∨ I_{1}x ∨ ⋯ ∨ I_{l}x))

(i) ¬ ∃x (I_{m}x ∧ I_{n}x) , for 0 ≤ m < n ≤ l

(j) ∃x Zx

(k) ∀x (Zx ⇒ (I_{1}x ∧ ¬ ∃y Lyx))

(l) ∀x (I_{m}x ⇒ ∃y Nxy) , for 1 ≤ m ≤ l

(m) ∀x (I_{0}x ⇒ ¬ ∃y Lxy)

3. axioms describing increment instructions: For each m in the range 1 ≤ m ≤ l, if I_{m} is an increment instruction then it is of the form

increment register R_{i} and go to instruction I_{n}

where 1 ≤ i ≤ s and 0 ≤ n ≤ l, and we have:

(a) ∀x ∀y ((I_{m}x ∧ Nxy) ⇒ I_{n}y)

(b) ∀x ∀y ((I_{m}x ∧ Nxy) ⇒ ∀u (R_{i}ux ⇒ R_{i}uy))

(c) ∀x ∀y ((I_{m}x ∧ Nxy) ⇒ ∃u (R_{i}uy ∧ ¬ R_{i}ux))

(d) ∀x ∀y ((I_{m}x ∧ Nxy) ⇒ ∀u ∀v ((R_{i}uy ∧ ¬ R_{i}ux ∧ R_{i}vy ∧ ¬ R_{i}vx) ⇒ Iuv))

(e) ∀x ∀y ((I_{m}x ∧ Nxy) ⇒ ∀u (R_{j}ux ⇔ R_{j}uy)) , for 1 ≤ j ≤ s, j ≠ i

4. axioms describing decrement instructions: For each m in the range 1 ≤ m ≤ l, if I_{m} is a decrement instruction then it is of the form

if R_{i} empty go to I_{n_{0}}, otherwise decrement R_{i} and go to I_{n_{1}}

where 1 ≤ i ≤ s and 0 ≤ n_{0} ≤ l and 0 ≤ n_{1} ≤ l, and we have:

(a) ∀x ∀y ((I_{m}x ∧ Nxy ∧ ¬ ∃u R_{i}ux) ⇒ I_{n_{0}}y)

(b) ∀x ∀y ((I_{m}x ∧ Nxy ∧ ∃u R_{i}ux) ⇒ I_{n_{1}}y)

(c) ∀x ∀y ((I_{m}x ∧ Nxy) ⇒ ∀u (R_{i}uy ⇒ R_{i}ux))

(d) ∀x ∀y ((I_{m}x ∧ Nxy ∧ ∃u R_{i}ux) ⇒ ∃u (R_{i}ux ∧ ¬ R_{i}uy))

(e) ∀x ∀y ((I_{m}x ∧ Nxy) ⇒ ∀u ∀v ((R_{i}ux ∧ ¬ R_{i}uy ∧ R_{i}vx ∧ ¬ R_{i}vy) ⇒ Iuv))

(f) ∀x ∀y ((I_{m}x ∧ Nxy) ⇒ ∀u (R_{j}ux ⇔ R_{j}uy)) , for 1 ≤ j ≤ s, j ≠ i Note that A_{P} describes a run of the program P, but we have not specified the initial contents of the registers.

2 Unsolvability

The Halting Problem is the problem of deciding whether a given register machine program started with all registers empty eventually stops. It is well known that the Halting Problem is unsolvable.

The Validity Problem is the problem of deciding whether a given predicate calculus sentence is valid. The Satisfiability Problem is the problem of deciding whether a given predicate calculus sentence is satisfiable. We are going to show that the Validity Problem and the Satisfiability Problem are unsolvable. This will be accomplished by reducing the Halting Problem to them. In other words, we shall show that if either of them were solvable, then the Halting Problem would be solvable.

Given a register machine program P, let P(0) be the unique run of P starting with all registers empty. Let A_{P} be as in Section 1, and let A_{P}(0) be A_{P} conjuncted with

∀x (Zx ⇒ ¬ ∃u (R_{1}ux ∨ ⋯ ∨ R_{s}ux)) .

Thus A_{P}(0) describes P(0).

Let B be the sentence ∃x I_{0}x. If P(0) eventually stops, then clearly A_{P}(0) is satisfiable in a finite domain, and any domain satisfying A_{P}(0) is necessarily finite and satisfies B. Hence in this case A_{P}(0) ⇒ B is valid.

On the other hand, if P(0) does not eventually stop, then A_{P}(0) is not satisfiable in any finite domain, but A_{P}(0) ∧ ¬ B is satisfiable in an infinite domain. Thus in this case A_{P}(0) ⇒ B is not valid.

We have proved:

Theorem 1 (Church’s Theorem) The Satisfiability Problem and the Validity Problem are unsolvable.

Theorem 2 (Trakhtenbrot’s Theorem) The problem of satisfiability in a finite domain is unsolvable. The problem of validity in finite domains is unsolvable.

3 Recursive Inseparability

Let V be the set of Gödel numbers of valid sentences, and let V_{fin} be the set of Gödel numbers of sentences which are valid in all finite domains. Note that V ⊆ V_{fin}. Theorems 1 and 2 can be rephrased by saying that neither V nor V_{fin} is recursive.

We shall now prove the following stronger result, also due to Trakhtenbrot.

Theorem 3 There is no recursive set X such that V ⊆ X ⊆ V_{fin}.

Remark. By the Gödel Completeness Theorem, V is recursively enumerable, i.e., Σ_{1}^{0}. It can also be shown that V_{fin} is co-recursively enumerable, i.e., Π_{1}^{0} (this is straightforward). Thus Theorem 3 implies that V and the complement of V_{fin} form a recursively inseparable pair of recursively enumerable sets.

In general, a pair of recursively enumerable sets I and J is said to be recursively inseparable if I ∩ J = ∅ and there is no recursive set X such that I ⊆ X and X ∩ J = ∅. The existence of a recursively inseparable pair of recursively enumerable sets is easily proved by a diagonal argument. For example, we may take I = {e | φ_{e}^{(1)}(e) ≃ 0} and J = {e | φ_{e}^{(1)}(e) ≃ 1}. If X were a recursive set separating I from J, then letting e be an index of the characteristic function of X we would have e ∈ X if and only if e ∉ X, a contradiction.

In order to prove Theorem 3, we shall slightly modify the construction of Section 2.

Let I and J be a recursively inseparable pair of recursively enumerable sets. Let ψ be the partial recursive function defined by

ψ(n) ≃ \{ \begin{matrix}0 if n ∈ I , \\ 1 if n ∈ J , \\ undefined otherwise . \end{matrix}

Let P be a register machine program which computes ψ. Let P(n) be the unique run of P starting with n in R_{1} and all other registers empty. Let A_{P} be as before, and let A_{P}(n) be A_{P} conjuncted with

∀x (Zx ⇒ ∃ exactly n u such that R_{1}ux)

conjuncted with

∀x (Zx ⇒ ¬ ∃u (R_{2}ux ∨ ⋯ ∨ R_{s}ux)).

Thus A_{P}(n) describes P(n).

Let B_{0} be the sentence ∃x (I_{0}x ∧ ¬ ∃u R_{2}ux). If n ∈ I then P(n) eventually stops with 0 in R_{2}, hence A_{P}(n) ⇒ B_{0} is valid, hence the Gödel number of A_{P}(n) ⇒ B_{0} belongs to V. If n ∈ J, then P(n) eventually stops with 1 in R_{2}, hence A_{P}(n) ∧ ¬ B_{0} is satisfiable in a finite domain, hence the Gödel number of A_{P}(n) ⇒ B_{0} does not belong to V_{fin}.

We can now complete the proof of Theorem 3. If there were a recursive set X such that V ⊆ X ⊆ V_{fin}, then

{n | the Gödel number of A_{P}(n) ⇒ B_{0} belongs to X}

would be a recursive set which separates I from J. Since I and J are recursively inseparable, Theorem 3 follows.