THE U N I V E R S I TY OF M I CHI GAN COLLEGE OF LITERATURE, SCIENCE, AND.THE ARTS Department of Philosophy Technical Report TURING-MACHINES AND THE ENTSCHEIDUNGSPROBLEM J. Richard Buchi ORA Project 03i05 under contract with: DEPARTMENT OF THE NAVY OFFICE OF NAVAL RESEARCH CONTRACT NO. Nonr 1224(21) WASHINGTON, D.C. administered through: OFFICE OF RESEARCH ADMINISTRATION ANN ARBOR December 1961

ciAse //o/

Turing-Machines and the Entscheidungsproblem* by J. Richard Buchi Let Q be the set of all sentences of elementary quantification theory (without equality). In its semantic version Hilbert's Entscheidungsproblem for a class XQ of sentences is: [X]: To find a method which, for every SEX, yields a decision as to whether or not S is satisfiable. Church (1936) showed that [Q] is recursively unsolvable. Shortly thereafter Turing (1936) obtained this result more directly by reducing to [Q] an unsolvable problem on Turing-machines. This reduction, however, is rather involved, and requires much detailed attention of the kind which does not add to one's over-all understanding of the situation. We will show in this paper that the connection between Turing-machines and quantification theory is really a rather simple one. The key to it is lemma 3, which is closely related to the Skolem-Godel-Herbrand work;on quantification theory. As a result we obtain the first really elegant proof of unsolvability of [Q]. It can be outlined thus: Lemma 1: The set Hlt, consisting of all Turing-machines which eventually halt, if started on the empty tape, is not recursive. Lemma 2: To any Turing-machine M, one can construct a matrix M(x,u,y), with *The results of this 'paper were announced in the Notices, Am. Math. Soc., 8 (1961), 354. The work was supported by a grant from the National Science Foundation and contracts with the Office of Naval Research and U. S. Army Signal Corps. 1

individual variables:.,u,y, monadic predicate letters Z,...., and 3 binary predicate letters S, K, and H, such that MfHlt if and only if ZoA(Vxy)M(x,x',y) is satisfiable in the natural number system <No,>. Lemma5 3: For any matrices Z(x) and M(x,u,y), the sentence (Hx)Z(x)/\(Vx)(.:u) (Vy)M(x,u,y) is satisfiable if and only if Z(o)/\(Vxy)M(x,x',y) is satisfiable in <N,,o'>. By lemmas 2 and 3, to any Turing-machine M one can construct a sentence S of form 23AV3V, such that MHlt if and only if S is satisfiable. Therefore, by lemma 1, Theorem 1: The problem [AV\^V ] is not recursively solvable, even if restricted to sentences in which, besides monadic letters, only three binary predicate letters occur. To stress the simplicity of this argument, we wish to claim that the following hints suffice to prove the three lemmas: Lemma 1 is well known and immediately follows from the basic unsolvability result on Turing-machines (machine halting on the tape carrying its description). Proving lemma 2 just means describing the operation of a Turing-machine M on the empty tape in the form C(Q,S,K,o,',x,y), whereby Qy = state at time y, Kxy - position x is scanned at time y, Sxy = tape-symbol at position x and time y. MEHlt then means that no Q, P and S exist such that for all places x and all times y, C(Q,S,o,,x,y). As the functions Q and S are finite-valued, they can be coded as vectors of monadic and binary predicates on natural numbers. It remains to invent some tricks to put the matrix C(o,',x,y) into the form Z(o)/M(x,x',y), by adding auxiliary predicates. Lemma 3 is trivial in the "if-direction". In 2

the other direction one might use the axiom of choice to introduce a monadic Skolem-function fx for (Ju) and a constant c for (ax). It remains to establish that Z(c)A(Vxy)M(x,fx,y) is satisfiable if and only if it is satisfiable by predicates in N and c=o, fx=x'. Our proof has the further advantage of directly yielding unsolvability for the very simple type SAV3V of sentences. By passing to the Skolem-form of VVf, theorem 1 also yields unsolvability of [\^va^VVVf]. Compare this with Bernays' (1958) analysis of Turing's proof, and note that such results are usually obtained by reduction of [Q] [see Suranyi (1959)]. Another feature of our proof is that, with slight modifications, it yields an improved version of Trachtenbrot's (1950) result about satisfiability in finite domains: Theorem 2: There is no recursive set which separates the not-satisfiable sentences from those satisfiable in a finite domain, even if only sentences of form ^AVSV are considered. Corollary: The set of S^AVV sentences, which are finitely satisfiable, is not recursive. Clearly theorem 2 follows from the following stronger versions of lemmas 1, 2, and 3: Lemma I: Let Cyl be the set of all Turing-machines which eventually cycle, if started on the empty tape. The sets Hlt and Cyl are not recursively separable. Lemma II: The construction M+M of lemma 2 has the further property: MECyl if and only if ZoA(Vxy)M(x,x',y) is satisfiable in <N,o, '> by periodic predicates. Lemma III: Add to lemma 3: The sentence (sx)Z(x)A(Vx)(Su)(Vy)M(x,u,y) is satisfiable in a finite domain, if and only if Z(o)A(Vxy)M(x,x',y) is satisfiable 5

in <N,co, > by periodic predicates. We will now indicate the proofs of the lemmas, and add some further discussion at the end of the paper. Proof of lemmas 2 and II: A (Turing-) machine we define to be a system M = <D, A, L, R, P, Q, S> consisting of a finite set D of elements called states; an A'D called the initial state; three binary predicates L[X,Y], R[X,Y], P[X,Y], called commands of left-move, right-move, and print; a binary function Q[X,Y] with values in D, called the new-state-function; and a function S[X,Y] with values in (T,F), called the print-function. All these predicates and functions have arguments XED and YE(T,F); furthermore, L, R, P are to be exclusive and complementary. The tape-symbols are T and F; a tape is a one-way infinite sequence of tape-symbols, i.e., a predicate Ix on N. The tape Ix _ F is called the empty tape. The operation of a machine M, set to work on a tape I, is as follows. M is started in its initial state A, scanning the zero-position of the tape I. If at any time t it is in state X and scans position u of the tape, which now carries the symbol Y, then, if L[X,Y], it moves to scan position u-l; if R[X,Y], it moves to scan position u+l; if P[X,Y], it prints S[X,Y] in place of Y at position u. In all cases it goes into the new state Q[X,Y]. Note that, if u=o and the command is L[X,Y], then M will next scan position -1, i.e., it runs off the tape. In this case we say that the machine halts at time t+l, and that the tape I is accepted by M; in symbols Hi(M,I). The set Hlt consists of all 4

machines M which eventually halt if put to work on the empty tape. Now suppose that M is put to work on the empty tape, and never comes to a halt (i.e., MHHlt). Then the functions Qx = state of M at time x Syx = tape-symbol at time x and position y Kyx _ at time x position y is scanned by M Lx = at time x the command is left-move Rx = at time x the command is right-move Px = at time x the command is print are defined for all x and y in N, and satisfy the conjunction C of the following conditions: Qo A A A -Syo Koo A ~Ky'o Kyx 0. Qx' = Q[Qx,Syx] Lx., Kyx' - Ky'x Kyx / L[Qx,Syx] -. Lx / -Px A -Rx Px in Kyx' Kyx Kyx A P[Qx,Syx].3. Px A -Lx / fx Rx 9, Ky'x' = Kyx Kyx A R[Qx,Syx]. R. Rx /A Lx A -Px Rx ox' [-Kyx A Px]vLx\Rx.0. Syx' _ Syx -[Kox A Lx] KyxAPx. Syx' - S[Qx,Syx] Conversely, the existence of Q, S, K, L, R, and P, which satisfy (Vyx)C, implies that M will not come to a halt if started on the empty tape. Thus (1) M.Hlt.. (Vxy)C is satisfiable in <N, o, '>. Note that the states of a machine may be coded as vectors of truth-values, so that the function-letter Q simply stands for a vector <Q1,..., Qn> of predicate-letters (n depending on the number of states of M), and C therefore is a matrix of quantification 5

theory. With the construction M-C, and the established (1), we thus are pretty close to a proof of lemma 2. All that remains to be done is to note that the following modifications of C do not affect the validity of (1). 1. Introduce an additional binary predicate-letter- H. On the right side of C replace Ky'o by Hyo, Ky'x by Hyx, Ky'x' by Hyx', and conjoin Hxy- Kx'y. The resulting matrix is of form C*(o,x,x',y) 2. Introduce an additional monadic predicate-letter Z. To C* conjoin Zo/OZx' and replace Qo=A A-Syo by Zx D. Qx=AA Syx, KooA-Hyo by Zx z.KxxA-Hyx, -Kox' by Zy:-Kyx', and -[KoxALx] by Zy -[KyxALx]. The resulting formula is of form ZoAM(x,x',y). M+M is the construction required in lemma 2. The same construction also satisfies lemma II, as will now be shown. The machine M, if started on the tape I, goes into a p-cycle at time X, if at the later time (2+p) it is faced with an identical situation, i.e., at times X and (I+p) M is in the same state and scans identical tapes in the same position. We will say that M (eventually) p-cycles on I, in symbols Cyp(M,I), if at some time it goes into a p-cycle. (It may be shown that for some p, Cyp(M,I) holds if and only if M never runs off the tape and scans only in a bounded part of the tape.) The set Cyl is defined to consist of all those machines M which eventually cycle, if put to work on the empty tape. A predicate Ux on N is called periodic with phase 3 and period p>o, if U(x+p) = Ux for all x_;. A relation Vxy on N is called periodic with phase 3 and period p>o, if V(x+p)y _ Vxy for all x_> and all y, and Vx(y+p) - Vxy for all x and all y-_. (Note that the entire line VxZ has to repeat at Vx(Z+p), and not just from x=~ on!) 6

Suppose now that M~Cyl, that is, M goes into a p-cycle at time,' if started on the empty tape. Then clearly the functions Q, L, R, P are periodic and Syx and Kyx are periodic in the time-argument x, all of them with phase d3 and period p. Furthermyre, if d is the maximum of all positions scanned by M before time (I+p), then at no time t a position y>d will be scanned. It follows that Kyx - F, for all x and all y>d, and because Syo - F and M never scans beyond d, also Syx - F for all x and all y>d. Thus, also K and S are periodic (with phase _I,d and period p). In other words, the implication from left to right of (2) is valid. (2) MECyl.-. (Vyx)C is satisfiable by periodic predicates in <N,o,'>. In the other direction (2) is trivially valid because the only solution of (Vyx)C are the predicates Q, S, K, L, R, P describing the operation of M; and to say that Q, S, K are periodic (in the time argument) just means that M eventually cycles. Because the modifications 1. and 2. of C to C* to ZoAM clearly do not affect the validity of (2), this ends the proof of lemma II. Proof of lemma I: We omit giving a direct proof of lemma 1, since it is well known from the literature. Of the proof of lemma I we present an intuitive sketch: The block of length r i.s the tape given by Iy (y<T). It is clear that one can effectively set up a coding function cd(M) which maps one-to-one all machines onto all blocks. A set X of blocks is called recursive if there are machines M1 and M2 such that for all blocks I, I X.-e Hi(M2,I) 7

A set Y of machines is called recursive if the set cd(Y) of blocks is recursive. As to the equivalence of this to other definitions of "recursive sets, we remark: 1. It is well known that the restriction to two tape-symbols (one of them the blank) and one-way infinite tapes is not a serious one. 2. Machines which print and move at the same time can, by adding new states, easily be modified so as either only to print or only to move in each atomic act. 3. We might have added another command predicate H[X,Y], to obtain haltsituations in addition to "running off the tape." But these can be eliminated by adding an additional state B, such that H[X,Y] implies that the next state is B, and B requires M to stay in B and move left. Note that for a machine M to 1-cycle simply means that it keeps scanning at the same position. Thus, one can find a predicate C1[X,Y] such that M at time t goes into a 1-cycle just in case C1[XY] holds for the state X and scanned symbol Y. Let now M' be obtained by adding a new state B with Q[B,Y] = B, and conjoining C1 to the right-move condition R. Then clearly Hl(MI) = Hl(M',I), but M' never 1-cycles. Similarly, one can modify a machine M to M' such that H1(MI) = Cyl(M',I) and M' does not halt on any block I. Thus in the definition of recursive sets of blocks one may replace (a) by I E. X.-. Cyl(Ml,I), M1 does not halt on blocks (b) I B X.-. Hi(M.2,I) M2 never 1-cycles It now is possible to combine M1 and M2 into one machine M which I-cycles on I EX and halts on IPX. Thus, to every recursive set X of blocks there is a machine Mo such that for all blocks I, 8

(c) I X._. Hl(MoI) By the usual diagonal-argument we now can prove lemma I: Suppose that Y is a recursive set of machines and separates the sets of machines for which Hl(M,cdM) respectively Cyl(M,cdM), i.e., Hi (M,cdM) D M Y Cyl(M,cdM) 2 M Y. By (c) there is a machine Mo, such that MjY _ Cyl(Mo,cdM) M Y - HI (Mo,cdM). Now Mo Y implies Cyl(MO,cdMO) implies Mof Y, and Mo Y implies Hl(Mo,cdMo) implies Mo0 Y. This is contradictory, and therefore (d) The sets A = (M; Hl(M,cdM)) and B = (M; Cyl(M,cdM)) are not separable by a recursive set. Because there is a recursive mapping f from machines to machines such that Hi (M,cdM) ~ fM E Hlt Cyl(M,cdM) D fM E Cyll it follows from (d) that also Hlt and Cyll are not separable. Finally, because CyllC Cyl, we conclude that Hlt and Cyl are inseparable. Proof of lemma 3 and III: We will assume that the matrices Z and M contain only one predicate-letter R, which is binary. The general case does not present any new problems. Let Z(R) stand for the sentence (Sx)Z(x)A (Vx)(3u) (Vy)M(x,u,y), and Z*(a,f,R) for its Skolem-transform Z(a).A(Vxy)M(x,fx,y). 9

Now suppose that.(R) is satisfiable, i.e., has a model <D1, R1>. By the axiom of choice it follows that there is an alED1 and a function f1: D1-D2, such that D1 = <D1, al, fl, R1> is a model of E*(a, f, R). Let D2 be the smallest subset of D1 which contains al and is closed under fl, let a2 = al, f2 = restriction of f1 to D2, R2 = restriction of R1 to D2. Because Z* is a universal sentence it follows that D2 = <D2, a2, f2, R2> still is a model of Z*. Next we note that <N,o,'> is the free algebra with one generator and one monadic function. Because <D2, a2, f2> is generated-by a2 and f2, it follows that there is a homomorphism h from <N,o,'> onto <D2, a2, f2_>. If we now define R3xy R2(hx)(hy), then it is.clear that D2 is homomorphic image of <N,o,,R3>. Again because Z* is universal it therefore follows that <N,o, ',R> is still a model of Z*(a, f, R). Thus, (1) Z is satisfiable.0. E is satisfiable in <N,o,'>. Suppose now further that the model <D1,Rl> of Z is finite. Then clearly the algebra <D2, a2, f2> is finite. It follows that the congruence relation hx = hy on <N, o, '> is of finite index, and therefore must be of form hx = hy a-. x = yv[x = _Iy > /\ x - y (modp)] for some 3 and p>o. It follows that the relation Rsxy is periodic with phase f and period p. Thus we have shown (2) Z finitely satisfiable. 3. Z periodically satisfiable in <N,o,'> The converse to (1) is trivial, so that lemma 3 is established. To establish lemma III it remains only to prove the converse to (2). This goes as follows: Suppose D = <N,o,',R> is a model of Z (a, f, R), whereby R1 is periodic, say of phase ~ and period p>o. The relation 10

x xy.. x = y v[x y A yAx - y(modp)] is clearly a congruence relation of <N, o, '>, and because R1 has phase a and period p, it is also a congruence relation of R1. Consequently one can form the factor D/i of the relational system D. Because Z is universal and D/% is homomorphic image of D, it follows that D/, is still a model of. Furthermore D/- is finite, because - is of finite index. But from any model of.(a, f, R) one obtains a model of Z(R), if one just omits the interpretations of a and f. Thus Z has a finite model. This concludes the proof of the lemmas. We add some further discussion of the results. General form of lemma III: Without any essential change in the presented proof, one can establish the result for general sentences of Q. In place of <N,o, '> appear the totally free algebras Fml' ' mk = <N, ol,.. On, fl,..,fk> with n generators and k operations, fi having mi arguments. A periodic relation on F is one which admits a congruence of F of finite index. A Skolem-transform *(o1,....,o, fl,...,fkR) of an arbitrary sentence Z(R) in Q is obtained by first writing E as a conjunction of prenex sentences, and next replacing existential quantifiers by individual-letters and function letters, in the well-known manner (suggested by the axiom of choice). The general form of lemma III now is Lemma III: Let 7(R1,...,Rs) be any sentence of Q, let Z (ol,... on, f,...fk, R1,...,Rs) be a Skolem-transform of E. (a) Z is satisfiable if and only if Z is satisfiable in the totally free algebra Fnml', 'mk. 11

(b) Z is satisfiable in a finite domain if and only if E is satisfiable in m Fn l'' mk by periodic relations. The proof we gave (using the axiom of choice) simply carries one step further Skolem's first proof of Lowenheim's theorem. A more elementary proof of part (a) actually is contained in Skolem's second proof. It may be outlined thus. The free algebra F can be built up by levels: Lo = (o1,.. On,) Lk+l is obtained by adding to Lk the elements fx...y whereby x,...,y Lk and f is one of fi... fm Let Z be a sentence. Its Skolem-transform E is a universal sentence, say (Vx...y)A(x,...,y). For any k we define k to be the conjunction of all A(u,...,v) whereby u,...,v range over Lk. By a quite elementary argument one shows: (c) If Z is satisfiable, then for every k, Z is satisfiable in Lk. Furthermore, by Konig's infinity lemma, (d) If for every k, Ek is satisfiable in Lk, then Z is satisfiable in F. Because the "if-part" is trivial, this yields a new proof of (a). It makes use of the infinity lemma, while the first proof uses the axiom of choice! We have not analyzed whether (b) also can be obtained in this second way. Syntactic version of the Entscheidungsproblem: If in the statement of problem [X] one replaces "satisfiable" by "formally consistent," one obtains the syntatic version [X]o. By Godel's completeness theorem it follows that [X] and [X]o are equivalent, so that also [SAVHV]0 is not recursively solvable. However, one can prove this more directly by using Herbrand's theorem. It can be stated thus: 12

(c') Z is formally consistent if and only if for any k, Zk is satisfiable in Lk. Now (c') and the infinity lemma (d) yield (a') E is formally consistent if and only if E is satisfiable in F. From lemmas 1, 2, and (a') the unsolvability of [3AVHV]0 follows. Reduction: If one does not accept Church's thesis, theorem 1 is of less interest. But our method also yields that SAV2V is a reduction-type, i.e., the problem [Q] is effectively reducible (in fact l-l-reducible) to the problem [SrAVV]. This can be seen by using Myhill's theorem, because our proof clearly shows that [3AVEV] is of unsolvability degree 1. More directly one can obtain a reduction from [Q] to [.AV3V] as follows. To the sentence E in Q construct a Turing-machine M which, if started on the empty tape, begins by checking Eo for satisfiability in Lo. M halts if it finds Zk not to be satisfiable in Lk, and it proceeds to Zk+l in case it has found a model of E. Thus by (c), satisfiable.-. M Hlt The construction of lemma 2 now yields a matrix M(x,u,y), which by lemma 2 and 3 is such that M ~ Hlt.-. A satisfiable, whereby A is the sentence ([x)Zx A (VX)-(Su)(Vy)M. Thus, the effective construction E + A reduces [Q] to [SAVVN]. Prefix of length four: The unsolvability of [VVV] does not follow from theorem 1, but it can be proved by the same method. (However, to obtain the necessary modified version of lemma 2, the author had to make use of ternary 13

predicate letters.) We note that all prenex-types with prefix of length 4 are now settled; all except V3VW and those falling under ^aVHV and Suranyi's (1959) W/\VVV have a solvable decision problem. There remains the question whether [S'VVV] is unsolvable if one admits, besides monadic letters, only two (only one) binary predicate letters. The prefix V/V: The really important outstanding question is to prove [VeV] unsolvable. For the first time there now is hope of obtaining this result. All that is missing is the following stronger form of lemma 2. Problem: To any Turing-machine M to construct a matrix M(x,u,y), with individual variables x,u,y, monadic predicate letters, and binary predicate letters, such that M Hlt if and only if (Vxy)M(x,x',y) is satisfiable in the natural number system <N, '>. In our proof of lemma 2 we fell short of obtaining this stronger result, because in describing the action of M on the empty tape we used special constraints on two axes, namely, the tape-axis and the time-axis.. It is important to realize that also in conditions of form (Vxy)M(x,x',y) one still has use of one axis, namely, one can formulate special restraints on the diagonal! In September, 1961, the author explained this situation to Hao Wang. He now claims, in collaboration with A. S. Kahr and E. F. Moore, to have found a construction M + M as required in the above problem. Thus, even '[VV] seems to be unsolvable, and the unsolvability of [vsAVVw] follows by passing to Skolem-form. These results would settle (up to detailed questions, like number of binary predicate-letters) the Entscheidungsproblem for all generalized prenex types (conjunctions of prenex sentences). It is easy to see that for 14

every generalized prenex type X either one of the following four alternatives holds: Al: Every conjunct of X is of form 3,m A2: Every conjunct of X is of form SWV?3 BI: There is a conjunct of form.... V..*.. V o.. in X. B2: There are conjuncts..o V..o V... and V.. V... V. e V... in Xo Thus, there are just two cases: A: [X] trivially reduces to [n:Vm] or [anv2] B: Either [V3 or [V[AVVV] trivially reduces to [X]. It is well known (see Ackermann, 1954) that [VVm] and [ V ] are solvable. Thus, in case A, [X] is solvable, while in case B, depending on the result of Kahr, Moore, and Wang, [X] is unsolvableo Let us say that a set X of sentences has property X, if every sentence of X which is satisfiable also is finitely satisfiableo In other words FAX means that X contains an "infinity-axiom." It is well known (see Ackermann, 1954) that a V 2 and 9rVm both have property A, while V2V and V^AVVV do not. The trivial reductions mentioned preserve property n, so that the cases A and B. also divide those generalized prenex types X having property 0 from those which do not. Matrices of special form: We will show now that if in theorem 1 one drops the remark concerning the number of binary predicate-letters, one can in turn add very strong restrictions on the form of the matrices in the S.AVIV sentences. We note that monadic letters can be eliminated (replace Sv by Svw) without changing satisfiability of a sentence. In the following discussion R, S,... 15

will stand for vectors of binary predicate-letters. By lemmas 1 and 2 the following is an undecidable problem, (D) For any matrices Z[Roo] and M[Rxx, Rxx', Rxy; Rx'x, R'x', Rx'y; Ryx, Ryx', Ryy] to decide whether Z(o)/ (Vxy)M(x,y) is satisfiable in < N,o,'>. The following modifications of M do clearly not affect satisfiability of Z(o)A (Vxy)M(x,y): 1. To M conjoin Sxy - Ryx and make the proper substitutions in M to obtain a new matrix of form A[Rxx, Rx'x, Rx'x', Rxy, Rx'y, Ryy]l\B[Rxy, Ryx]. 2. To AAB conjoin Sxy = Rx'y and make the proper substitutions in A to obtain a new matrix of form A[Rxx, Rxx', Rxy, Ryy]AB[Rxy, Ryx]AC[Rxy, Rx'y]. 3. To AA BAC conjoin [Rxy - Syx]/ [Sx'y - Txy] and make the proper substitutions in A to obtain the new matrix of form A[Rxx, Rxy, Ryy]A B[Rxy, Ryx]/ C[Rxy, Rx'y]. 4. To A BA C conjoin [Sxx = Rxx]/ [Sxty = Sxy] and in A substitute Syx for Rxx, and Sxy for Ryy to obtain a new matrix of form W[Rxx]A B[Rxy, Ryx]AC[Rxy, Rx'y]. It therefore follows that the following is still an undecidable problem, (D') For any matrices Z[Roo], W[Rxx], B[Rxy, Ryx] and C[Rxy, Rx'y] to decide whether Z(o)/ (Vx)W(x)\ (Vxy)B(x,y)/\(Vxy)C(x, x', y) is satisfiable in < N, o,. By lemma 3 one now obtains, Theorem 11: There is no recursive method for deciding satisfiability of sentences of form (gv)Z[Rwvv] (Vx)W[Rxx]/A(Vxy)B[Rxy, Ryx]/\(Vx)(2u)(Vy)C[Rxy, Ruy], whereby R is a vector of binary predicate letterso 16

Depending on the mentioned result of Kahr, Moore, and Wang the initial condition Z[Roo] may be dropped without making (D) decidable. Correspondingly theorem 1' remains true if "(Iv)Z[Rvv]" is dropped. The question, whether in addition the axial restraint W[Rxx] can be avoided, remains unanswered. Domino problems: The reduction (D) to (D') discussed in the previous section can be carried one step further by the following observation, Suppose that the predicates Rxy on N satisfy (1) (Vxy)D[Rxy, Ryx, Rx'y]. Then clearly the predicates Pxy - Rxy and Qxy = Ryx satisfy (2) (Vx)[Qxx Pxx]A (Vxy) xD_[Pxy, Qxy, Pxy]A (Vxy)x>_D[Qxy, Pxy, Qxy ] Conversely, if Q and P satisfy (2) then the predicates R defined by Rxy = Pxy, if x=y and Rxy = Qyx, if x-y satisfy (1). Thus, (1) is satisfiable if and only if (2) is satisfiable. Note furthermore that the following formula uniquely defines the predicates x>y and x>y: (3) x^-xA -.[x>x] [x'>y] [x] - [X>Y][xiy]0[x~y] Thus, in case D[Rxy, Ryx, Rx'y] is of form B[Rxy, Ryx]/ C[Rxy, Rx'y] one obtains an (as to satisfiability) equivalent formula of form W[Rxx]AU[Rxy, Rx'y]A V[Rxy, Rxy'], by conjoining (3) to (2). Consequently the problem (D') reduces to the following, (D"') For any matrices Z[Roo], W[Rxx], U[Rxy, Rx'y], V[Rxy, Rxy']-to decide whether Z(o)/ (Vx)W(x)A(Vxy). U(x,x',y)/\V(x,y,y') is satisfiable in < N,o,'>. It therefore follows that also this problem is unsolvable, and by lemma 3, Theorem I ": There is no recursive method for deciding satisfiability of sentences of form (.v)Z[Rw]l (Vx)W[Rxx]A(Vx)(a[u)(Vy). U[Rxy, Ruy]/ V[Ryx, Ryu]. 17

Depending on the result of Kahr, Moore and Wang the conjunct Z can be dropped. However, the question whether in this theorem both restraints on (Sv)Z(v) and (Vx)W(x) may be dropped is a challenging unsolved problem. It can be stated thus, Problem 1: Is there an effective method which applies to any < S, U, V >, U and V binary relations on the finite set S, and decides whether or not there is a valuation R: NxN-+S which satisfies the condition (Vxy)o U[Rxy, Rx'y]A\ V[Rxy, Rxy']. In a slightly different form this was first stated by Wang (1961), and called the domino problem. U and V may be interpreted as sets of bars of length one, whose ends are marked with colors from a finite set So The problem then takes the following rather appealing form: To decide whether the lattice NN, can be filled with bars from U along the x-direction and bars from V along the y-direction, such that the ends of all bars meeting at any lattice point carry the same color. The domino problem 1 is distinguished from other decision-problems by the complete lack of "initial restraints." This seems to make it very hard to reduce to it any one of the standard unsolvable problems, which all contain initial conditions of one kind or another (empty or finite initial tapes, initial states, axioms = initial theorems). In contrast, such a reduction was possible in the case (D''), which is the domino problem 1 with initial restraints Z[Roo] and W[Rxx] added. In fact, the claim of Kahr, Moore and Wang is that the domino problem becomes unsolvable even in case only the axial-restraint W[Rxx] is added. 18

Related to the domino problem is the following, also unanswered, question: Problem 2: Is there a finite set S and binary relations U and V on S such that (Vxy). U[Rxy, Rx'y]/ V[Rxy, Rxy'] has a solution R, but none which is periodic? By lemma III this is simply the question whether or not there still is an infinity-axiom of form (vx)(gu)(vy). U[Rxy, Ruy]A V[Ryx, Ryu], ioeo, whether the set VVo0, consisting of all these sentences, has property 0. As noted by Wang (1961), a negative answer to problem 2 would mean solvability of the domino problem 1. (This corresponds to the well known fact that OX implies solvability of [X].) However, we rather expect problem 1 to be unsolvable (possibly not of maximal degree 1, which would explain the mentioned difficulties in setting up reductions of standard unsolvable problems). An unsolved problem on Turing-machines: We will now present a very natural halting problem on Turing-machines. It came up in connection with [V~V], but seems to be of interest in its own righto (T2) To find an effective method, which for every Turing-machine M decides whether or not, for all tapes I (finite and infinite) and all states B, M will eventually halt if started in state B on the tape I. This problem also displays the feature of lack of initial restraints, Stanley Tennenbaum has shown to the author that (T2) becomes unsolvable if either one of the following initial restraints is added: 1. Distinguished initial state A, 2. Initially the tape is empty. 19

References A. Church, "A note on the Entscheidungsproblem," Journal of Symbolic Logic, 1 (1936), 40-41, 101-102. A M. Turing, "On computable numbers, with an application to the Entscheidungsproblem," Proc. London Math. Soc., ser. 2, 42 (1936-37), 230-265; 43 (1937), 544-546. J. Suranyi, Reduktionstheorie des Entscheidungsproblems, Budapest, 1959. W. Ackermann, Solvable cases of the decision problem, North-Holland, Amsterdam, 1954. B. A. Trachtenbrot, "Nevozmoznost' algorifma dla problemy razresimosti na kone~nyh klassah," Doklady Akademii Nauk SSSR, n.s., 70 (1950), 569-572. P. Bernays, "Remarques sur les probleme de la decision en logique elementaire, Edition de centre nat. de la rech. scient., 13 (1958), Paris, 39-44. H. Wang, "Proving theorems by pattern recognition II," Bell System Technical Journal, 40 (1961), 1-41. 20

DISTRIBUTION LIST (One copy unless otherwise noted) Assto Sec. of Def. for Res. 2 Bureau of Ships and Eng. Department of the Navy Information Office Library Br. Washington 25, D.C. Pentagon Building Attn: Code 671 NTDS Washington 25, D. C. Bureau of Naval Weapons Armed Services Tech. Infor. Agcy. 10 Depar~tment of the Navy Arlington Hall Station Washington 25, D C. Arlington 12, Virginia Attn: RAAV Avionics Division Chief of Naval Research 2 Bureau of Ships Department of the Navy Department of the Navy Washington 25, D.C. Washington 25, D oC Attn: Code 437, Inf. Syst. Br. Attn: Communications Bro Code 686 Chief of Naval Operations Naval Ordnance Laboratory OP-07T-12 White Oaks Navy Department Silver Spring 19, Maryland Washington 25, D.C. Attn: Technical Library Director, Naval Res. Lab. 6 David Taylor Model Basin Tech. Inf. Officer/Code 2000 Washington 7, D oC Washington 25, D.C. Attn: Technical Library Commanding Officer, Officer of 10 Naval Electronics Laboratory Naval Research San Diego 52, California Navy. No. 100, Fleet P. O. Attn: Technical Library. New York, New York University of Illinois Commanding Officer, ONR Br. Office Control Systems Laboratory 346 Broadway Urbana, Illinois New York 13, New York Attn~ D. Alpert Commanding Officer, ONR Br. Office University of Illinois 495 Summer St. Digital Computer Laboratory Boston 10, Massachusetts Urbana, Illinois Attn: Dr. J. Eo Robertson Office of Technical Services Technical Reports Section National Security Agency 3 Department of Commerce Fort Geo. Go Meade, Maryland Washington 25, D.C. Attn: Howard Campaigne 21

Technical Information Officer Massachusetts Inst. of Technology US Army Signal Research and Dev. Lab. Cambridge, Massachusetts Fort Monmouth, New Jersey Attn: D. W. Baumann Attn: Data Equipment Branch Dynamic Analysis and Control Lab. U. S. Naval Weapons Laboratory Burroughs Corporation Dahlgren, Virginia Research Center Attn: Head, Compution Div., Paoli, Pennsylvania G. H. Gleissner Attn: R. Ao Tracey National Bureau of Standards Hermes Incorporated Washington 25, DoC. 75 Cambridge Parkway Attn: Dr. So No Alexander Cambridge 42, Massachusetts Attn: Mr. Reuben Wasserman Aberdeen Proving Ground, BRL Aberdeen Proving Ground, Maryland Lockheed Missiles and Space Div. Attn: J. H. Giese, Chief Compution Lab. 3251 Hanover Street Palo Alto, California Office of Naval Research Attn Do Go Willis Resident Representative University of Michigan University of Michigan 146-B Temporary Classroom Bldg. Ann Arbor, Michigan Ann Arbor, Michigan Attn: Depto of Philosophy, Prof. A Wo Burks Commanding Officer ONR, Branch Office Census Bureau John Crerar Library Bldg. Washington 25, DoC. 86 East Randolph St. Attn: Office of Assto Director for Chicago 1, Illinois Statistical Services, Mr. J. L. McPherson Commanding Officer ONR, Branch Office National Science Foundation 1030 E. Green Street Program Dir. for Documentation Res. Pasadena, California Washington 25, D.C. Attn: Helen L. Brownson Commanding Officer ONR, Branch Office University of California 1000 Geary Street Los Angeles 24, California San Francisco 9, California Attn: Depto of Engo, Prof. Gerald Estrin National Bureau of Standards Washington 25, DQC. Columbia University Attn: Mr. R. D. Elbourn New York 27, New York Attn: Dept. of Physics, Naval Ordnance Laboratory Profo Lo Brillouin Corona, California Attn: H. H. Weider 22

Hebrew University Wright Air Development Division Jerusalem, Israel Electronic Technology Laboratory Attn: Prof. Y. Bar-Hillel Wright Patterson Air Force Base, Ohio Attn WWRNEB Computer and Bionics Br. Massachusetts Insto of Tech. Cambridge, Massachusetts Laboratory for Electronics, Inco Attn: Prof. W. McCulloch 1079 Commonwealth Aveo Boston 15, Massachusetts Atomic Energy Commission Attn~ Dro H. Fuller Washington 25, D.C. Attn: Div. of Research, John R. Pasta Stanford Research Institute Computer Laboratory Naval Research Laboratory Menlo Park, California Washington 25, D.C. Attno H. D. Crane Attn: Security Systems Code 5266, Mr. G. Abraham General Electric Company Schnectady 5, New York Cornell University Attn~ Library, LoMoE. Depto, Dept. of Mathematics Bldgo 28-501 Ithaca. New York Attno Profo Mark Kac The Rand Corporation 1700 Main Street Dr. A. M. Uttley Santa Monica, California National Physical Laboratory Attn:. Numerical Analysis Dept. Teddington, Middlesex Willis H. Ware England Hunter College Diamond Ordnance Fuze Laboratory New York 21, New York Connecticut Ave. and Van Ness St. Attn~ Dean Mina Reeso Washington 25, D.C. ORDTL-012, E. W. Channel General Electric Research Laboratory P. 0. Box 1088 U.S. Army Signal Res. and Dev. Lab. Schenectady, New York Fort Monmouth, New Jersey Attn: Information Studies Section Attn: M. Tenzer R. L. Shuey, Manager Harvard University Radio Corporation of America Cambridge, Massachusetts Moorestown, New Jersey Attn: School of Applied Science Attn: Missile and Surface Radar Div. Dean Harvey Brook Sidney, Caplan The University of Chicago University of Pennsylvania Institute for Computer Research Institute of Cooperative Research Chicago 37, Illinois Philadelphia, Pennsylvania Attn: Mro Nicholas Co Metropolis, Diro Attn: Dr. John O'Conner 23

Stanford Research Institute National Biomedical Reso Found. Inco Menlo Park, California 8600 16th St., Suite 310 Attno Dr. Charles Rosen Silver Spring, Maryland Applied Physics Group Attn~ Dr. R. So Ledley Northeastern University National Bureau of Standards 360 Huntington Avenue Washington 25, Do Co Boston, Massachusetts Attn~ Mrs. Frances Neeland Attn: Prof. Lo O Dolansky University of Pennsylvania Marquardt Aircraft Company Moore School of Elec. Eng. 16555 Saticoy Street 200 South 33rd Street P. O0 Box 2013 - South Annex Philadelphia 4, Pennsylvania Van Nuys, California Attn: Miss Anna Louise Campion Attn: Dr. Basun Chang, Res. Sci. Texas Technological College Varo Manufacturing Company Lubbock, Texas 2201 Walnut Street Attn: Paul G. Griffith Garland, Texas Dept. of Electrical Engineering Attno Fred Po Granger, Jr. IBM Corporation Data Processing Systems Staff Military Products Division Department of State Owego, New York Washington 25, DoC. Attno Dr. So Winkler Attn: F. P. Diblasi Post Office Department Dr. Saul Gorn, Director Office of Res. and Engo Computer Center 12th and Pennsylvania Avenue University of Pennsylvania Washington 25, Do Co Philadelphia 4, Pennsylvania Attn: Mr. R. Kopp, Res. and Develo Div. Applied Physics Laboratory Air Force Research Division, ARDC Johns Hopkins University Computer and Mathemathical Sci. Lab., ARCRC 8621 Georgia Avenue L. G. Hanscom Field, CRBB, Bedford, Mass. Silver Spring, Maryland Attn: Dro H. H. Zschirnt Attn: Supervisor of Tech. Rpts. Office of Chief Signal Officer Chief, Bureau of Supplies and Department of the Army Accounts, Navy Department Washington D.C. Washington, DoCo Attn: R and D. Div. SIGRO-6D Attn: CDR. Jo C. Busby, Code W3 Mr Lo H. Geiger Auerbach Electronics Corporation Bell Telephone Laboratories 1634 Arch Sto Murray Hill Laboratory Philadelphia 3, Pennsylvania Murray Hill, New Jersey Attn: Dr. Edward Fo Moore 24

National Aeronautics and Space Lincoln Laboratory Administration Massachusetts Institute of Technology Goddard Space Flight Center Lexington 73, Massachusetts Greenbelt, Maryland Attn: Library Attn: Chief, Data Systems, Divo CXV.L. Smith Dr. C. Ro Porter Psychology Department Federal Aviation Agency Howard University Bureau of Research and Development' Washington 1, Do C. Washington 25, D.C. Attn: RD-375, Mr. Harry Hayman Electronics Research Laboratory University of California Mr. Donald Fo Wilson Berkeley 4, California Code 5144 Attn: Director Naval Research Laboratory Washington 25, D. C. Institute for Defense Analysis Communications Research Division David Taylor Model Basin Von Neumann Hall Washington 7, D.C. Princeton, New Jersey Attn: Aerodynamics Laboratory, Code 628, Miss Cravens 25

UNIVERSITY OF MICHIGAN 3 9015 02651 5034