THE UNIVERSITY OF MI CHIGAN COLLEGE OF LITERATURE, SCIENCE, AND THE ARTS Logic of Computers Group Technical Report WEAK SECOND-ORDER ARITHMETIC AND FINITE AUTOMATA J. Richard B'uchi administered by: THE UNIVERSITY OF MICHIGAN RESEARCH INSTITUTE ANN ARBOR September 1959

j/to^ 3 The work reported and discussed in this paper has been carried on under the listed grant and contracts with the following agencies: National Science Foundation Washington, D.C. NSF Grant - G-4790 Office of Naval Research Washington, D.C. Contract NONR-1224(21), Project NR 049-114 U.S. Army Office of Ordnance Research through Detroit Ordnance District Detroit, Michigan Contract DA-20-018-ORD-16971 U.S. Army Signal Supply Agency Laboratory Procurement Support Office Fort Monmouth, New Jersey Contract DA-36-039-sc-78057

INTRODUCTION* The formalism of regular expressions was introduced by S. C. Kleene [6] to obtain the following basic theorems. Synthesis: To every regular expression E one can effectively obtain a finite automata A with binary output U such that E denotes the behavior of <A,U>. Analysis: To every finite automaton A with binary output U one can effectively construct a regular expression E such that the behavior of <A,U> is denoted by E. For simplified expositions of Kleene's theory see Copi-Elgot-Wright [4], Rabin-Scott [13], and Myhill [8]. It will be shown here that a more conventional formalism, a weak secondorder arithmetic, can be used in place of the formalism of regular expressions. Our theorems 1, 2 section 4 are equivalent to Kleene's synthesis and analysis theorems. This result is of interest for automata theory because formulas of weak second-order arithmetic seem to be more convenient than regular expressions for formalizing conditions on the behavior of automata. In addition, our synthesis and analysis theorems yield rather complete information on the strength of weak second-order arithmetic (see Section 5), thus providing an example of applying automata theory to logic. *The author wishes to thank Dr. J. B. Wright for many stimulating discussions. Some of the results were announced in the Notices, American Mathematical Society. ("Decision Problems of Weak Second-Order Arithmetics and Finite Automata. Prelim. Report, Part I," Vol. 5, No. 7, December 1958). 1

1. NOTATIONS AND TERMINOLOGY The following letters (possibly with subscripts) will be used as syntactic variables with range as indicated, x, y, z, t denote individual variables X, Y, Z denote propositional variables i, j, r, s, u denote monadic predicate variables A, B, C, D,... denote formulas of propositional calculus A, B, C, D denote formulas. Besides the already mentioned (countable) lists of variables our formalism contains the primitive symbols-.V,, A, V,, D,, [, ], V, 3, (, ),o '. The formulas of propositional calculus (p.f.'s) are obtained in the conventional manner from.A-, 'V and propositional variables by means of the connectives and [, ]. Examples of atomic formulas are i(o"), i(x), r2(tf '). Matrices are obtained by replacing all propositional variables in a p.fo A by atomic formulas. Formulas (of restricted, i.e. monadic, second-order-predicate calculus) are obtained in the conventional manner from matrices by applying individual-and predicate-quantifiers, and propositional connectives. A sentence is a formula without free variables~ A method for indicating occurrences of free variables is explained by the following examples. "D[X,Y,Z]" denotes a p.f. in which the indicated propositional variables but no others may occur. "D[i(o"), i(x), s(t')]" denotes the matrix obtained by making the obvious substitutions in D[X,Y,Z], and may be ab2

breviated as "D(o,x,t)". "C(il,i2,t)" denotes a formula in which the variables l1i2,t but no others may have free occurrences~ We will also abbreviate "[-A]" by "A", and "[AAB]" by "AB" We will often deal with n-tuples of objects. The symbol ",, denotes concatenation of n-tuples. Thus for example "H1 H2 HI" and "i1 1i 13 14 denote respectively a 3-tuple of matrices and a 4-tuple of propositional variables. The second component of the 3-tuple a b c is b. The n-tuple 2 2 2.e. 2 will also be denoted by "n". We next explain the use of a vector-notation which will considerably condense the presentation and make it more comprehensible. Xn, yn, Zn denote n-tuples of propositional variables in jn, rn sn denote n-tuples of monadic predicate variables An, Bn, denote n-tuples of propositional formulas For example, "rm(t') - Hm[rm(t), in(t)]" stands for the m-tuples of matrices whose components are rl(t') Hl[rl(t),....rm(t), i l(t),....in(t)],....,rm(t) Hm[rl(t),....,rm(t), i(tl),....,in(t' )]. "xn'Y" stand for the (n+l)-tuple ^,1 "-> ^\ 6>' X1 X2... Xn Y. At some places a notation for an n-tuple of propositional formulas is used ambiguously to denote the conjunction of the p.f. 's occurring in the n-tupleo Furthermore the superscripts on notation for n-tuples are often omitted; in such cases it is clear from the context how they are to be restored. Interpretation: We will not make use of any deductive structure on the syntactic frame. However, propositional formulas and formulas will be interpreted. Because the interpretations are quite conventional we will not state rigorous definitions. Furthermore, we will make ambiguous use of the syntactic notations, using them at times also for reference to the interpretation. The following list 35

will explain additional notations and terminology. -A., V truth values false, true '^'n the n-tuple A2^... -A._ predicate function from natural numbers to (J^_,V- ) (set of natural numbers) special predicate predicate which is ultimately false (finite set of natural numbers) n-predicate n-tuple of predicates special n-predicates n-predicate with special components (n-predicate which is ultimately.^ n) Further notations are introduced in the various sections. 2. WEAK SECOND-ORDER ARITHMETIC We now consider the following interpretation of the primitive symbols of the restricted second-order system described in 1..A.,, V true, false A, V ~ D, 2 = the usual truth functions o, ' the natural number zero, the successor-function on natural numbers individual variables range over natural numbers predicate variables range over special predicates (finite sets of natural numbers) (3x), (Vx) there is a n.n.x, for all n.n.'s x (3i), (Vi) there is a special predicate i, for all special predicates i. 4

This leads in a conventional manner to a definition of satisfaction for formulas, and truth for sentences. The resulting interpreted system will be called weak second-order arithmetic (Wo2.A). The notation "i C(i)" will be used for the set of all special predicates i on natural numbers which satisfy the formula C(i)o The notations "x C(x)", C(in) are used similarly. The formula C(i) defines the set i C(i) in Wo2.A. C(i,x) is equivalent to B(i,x) if xC(i,x) = 4xC(i,x), i.e., if (Vi) (Vx). C(i,x)= B(i,x) holds in W.2.A. Lemma 1: In W.2.A., to every formula C(in) one can effectively construct a formula C(in) such that C*(in) = i C(in) and C*(in) is of the form (j) K[j(o)] A (Vt) B[i(t),j(t),(t')], whereby j is a r-tuple jl2- rj r of predicate variables and (j) is a prefix of quantifiers (j v) and (Vj ). Proof: It is clear that one can construct a formula Z(x) such that o is the only number satisfying Z(x). Now if o occurs in C(i) and D(i,x) is obtained by substituting x for o in C(i), then C(i).-O (3x) [Z(x) A D(i,x)] holds for i. Thus we have obtained a formula Cl(i) equivalent to C(i) in which o does not occur. The next step is to construct from Cl(i) an equivalent formula C2(i) in which no iterations of ' occur and no ' occurs in argument places of i. This is easily accomplished by introduction of new predicate variables which are appropriately quantified. Then C3(i) is obtained by passing to prenex form. Next we repeatedly apply to C3(i) identities of the form (prefix 1) (3x) (prefix 2) A(x,.oo).=o (prefix 1) (3j) (Vx) (prefix 2) (3y) [j(y) A j(x)= A(x,o...)] and their duals, to obtain a formula C4(i) equivalent to C(i) which is of the form C4(i): (predicate prefix) (individual prefix) [Matrix]. Because the matrices are constructed from monadic predicate variables only we can make 5

use of Behmann's [1] device of moving individual quantifiers into the matrix of C4(i). The result is a formula C5(i) equivalent to C(i), and of form C5(i): (predicate prefix) A [(3t)Dv(t) V (Vt)EV,l (t) V...... V (Vt)E,n(t)]. Now we note that predicate quantification is over special predicates, and therefore identities of the form (Vt)E(t)..-.. (Vj) ~ J(o) V (3t)[j(t) 3(t')E(t)] hold in W.2.A. If we accordingly replace each constituent (3 t)Ev (t) in C5(i), making use of different j's, and then move the newly introduced predicate-quantifiers into the prefix, the result is a formula C6(i) equivalent to C(i) and of the form, C6(i): (predicate prefix) ' [Av(o) V (3 t)Bv(t)]. Now we remark again that predicate quantification is over special predicates, and therefore identities of the form A(o) V (3t)B(t)..=.. (3j) ~ [A() (o) A j(o) (t)[j(t) A j(t'):B(t)] hold in W.2.A. Accordingly we replace each Av(o) V (3t)Bv(t) in C6(i), making use of different j's, and then move the new predicate quantifiers into the prefix. The result is a formula C*(i) equivalent to C(i) and of the form required in lemma 1. 3. FINITE AUTOMATA We will now define automata as syntactic entities. We refer to Section 6 for motivation. In Section 6, our concept also is compared with other definitions of "finite automaton." Definition 1. A (finite n/m-automaton with input Xn and transit Ym is a 2m-tuple EmIH4m[ym,Xn] of propositional formulas. (Note that no propositional variables occur in Em). A (binary) output of a n/m-automaton with transit ym is a propositional formula U[Ym]. 6

The transition-resursion of an automaton EmnlHm is the 2m-tuple of matrices rm(o) Em rm(t) Hm[rm(t),in(t)] it defines recursively a functional which will be denoted by r =:(E,H,i). The output-recursion of an automaton with output Em'Hm`'U, is obtained by adding the matrix u(t) - U[r (t)] to the transition-recursion. It defines recursively a functional which will be denoted by u = *(E,H,U,i). The "input to output" functional u = t(E,H,U,i) might be defined to be the behavior of the automaton with output. However, this is inconvenient for establishing relations to W.2.A., because in general u = V(i) will not be special even for special i. We therefore will deal with a special sort of output only. It will be seen in Section 6 that this is not essentially a restriction. Definition 2. U[Ym] is a special output of the automaton E"m'Hm if U[] U[H[Y,J]]. It is easy to see that in case U is special the output recursion defines an operator? such that ((i) or (j(i) is special whenever i is special. This makes the operator definition of behavior manageable in W.2.A. However, it is more convenient to work with the set 3 consisting of all special i for which -^(i) is special, rather than with I directly. This leads to the following definition of behavior, which is closely related to Kleene's [6] (see Section 7). Definition 3. The behavior 5(Em,Hm,U) of a n/m-automaton with special output is the set of all special n-predicates in for which the predicate u = _(E,H,U,i), 7

determined by the output-recursion, is ultimately true, i.e., (3 x) (Vt)xu(t). By the length of a special n-predicate in we mean the smallest number x such that in(t) — In for t > x. By definitions 2,3 one easily proves, (*) If U is a special output of the automaton Em^Hm, and if in is a n-predicate of length I, then i e B(E,H,U).-. U[r(X+l)] whereby r = t(E,H) is given by the transition-recursion of E H. Lemma 2: If U is a special output of the n/m-automaton Em'Hm then so is 4U. Furthermore the behaviors P(E,H,U) and P(E,H,-U) are complementary subsets of the set of all special n-predicates. Proof: That -U again is special follows directly by definition 2. That the behaviors of U and MU are complementary is best seen by referring to (*). Definition 4: An n/m-automaton with output, E mH mU, is in expanded form if Hm and U are of the form Hm[Yi,...^Ymxn]: YlKn[Xn]V....... VYm_[Xn] U [Yi,...,Ym]: YV Y2 V.... V Yk Lemma 3: To every n/m-automaton Em'eHm U one can construct a n/k-automaton Gk'Lk/^W which is in expanded form, and such that if U is special output of Em'Hm then W is special output of Gk Lk and the behavior P(G,LW) is equal to P(E,HU)o Proof: We indicate the construction of G, L, W in case m=2 2, and U[Y1,Y2] = Y1. The given automaton then consists of p.f's El, E2, H1[Y1,Y2,Xn], H2[Yl,Y2,Xn]. The first step in the construction is to obtain disjunctive forms for H1,H2, and U. Let this be, 8

H1[Y1,Y2,X].*. Y1Y2A11[X] V Y1Y2A12[X] V Y1Y2A13[X] \Y1Yi2A14[X] (1) H2[Y1,Y2,X].. Y1Y2A21X] [X] V Y1Y2A22[X] "v1Y2A23[X] VYly2A24[X] (2) U[Y1,Y2].. Y1Y2 ' Y1Y2 Now we let k = 2 2 2 2 and construct Gk, Hk, W as follows, G1: E1E2 G3: E1E2 (3) G2 E1E2 G4 E1E2 L1[Z1,Z2,Z3,Z4,X] ] Z1A1[X]A21[X] V Z2A12[X]A22[X] V Z3A13[X]A23[X] V Z4A14[X]A24[X] L2[Z1,Z3,ZZ4,X] ZlAll[X]A21[X] V Z2A12[X]A22[X] V Z3A13[X]A23[X] V Z4A14[X]A24[X] (4) L3[ZlZ2,z3,Z4,x] Z11[X]A21[X] vZ2iL2[X]A22[X] V Z3i3[X]A23[X] V Z44[X]A24[X] L4[Z1,Z2,Z3,Z4,X] Z~11[X]21[] VZ2Al2[X]A'22[X] \ Z313[X]~23[X] / Z14[X]A24[X] (5) W[Z1,Z2,23,Z4]: 1 ZZ2 By definition 4, and (3), (4), (5) it is clear that G' L/ W is in expanded form. Next we obtain from (1) the identities Hv[Y1,Y2,X].. YiY2Av1[X] /Yi2A~v2[X] V YiY2Av3[X] \/ 1Y2Av4[X]. Together with (1) and (4) this yields, L1[Y1Y2, YY2, Y1Y2i Y1Y2, X].. H1[Y1,Y2,X] H2[Y1,Y2,X] L2[Y1Y2, Y1Y2, I1Y2, Y1Y2, X] Hj[Y1PY2,X] H2[Y1,Y2,X] (6) s[YiY2, YI.^, 7lY~, 7l, X].=. H.[Yi,Y2,x] H[YlYPx] L4[Y1Y2, Y1Y, Y2 Y1Y2, X].-. H1[Yy,Y2,X] H2[Y1,Y2,X] and from (2) and (5) we get, (7) W[Y1Y2, Y1Y2, Y1Y2, Y1Y2].=. U[Y1Y2] 9

Now assume that U is a special output of E H. Let C[Y1,Y2] stand for YIY2 YIY2 YiY2 Y1Y2. Then using in order (7), definition 2, (7), (6) one obtains W[C[Y1,Y2]] W[L[C[Y1Y2],A]]. This means that W[Z] - W[L[Z,-]] holds for the values/VAJ\J, AVJN,AAV, A, andAAAV of Z. Because of the particular form (5) of W the restriction of the range of Z can be omitted, which by definition 2 means that W is special output of G L. Next let i be any n-predicate and let rl r2 = (E,H,i), s1 s2 s s 4 = (GLi), so that r(o) - E s(o) G (8) (9) r(t') - H[r(t),i(t)1] s(t' ) L[s(t),i(t)] Using (3), (6), (8), (9) one shows by an induction on t that sl(t) = r1(t) r2(t), s2(t) rl(t) r2(t), S3(t) -r~(t) r2(t), s4(t) - l(t) p2(t) hold for all t. Because of (7) this yields, (Vt)-W[s(t)] - U[r(t)]. By definition 3 it follows that P(G,L,W) = P(K,H,U). f F' Lemma 4. Let Em Hm be an n 2/m-automaton in expanded form and let Lm be defined by, Lm[, Xn]: H[Y, X V] V Hm[ym X_ ]. (a) If i j is any n 2-predicate and if r = S(E,H,i j), and s = (EL,in), then (t) [r(t) D s(t)]. (b) If in is any n-predicate, and sm = _(E,L,in), and sv(x') -, then there exists a special predicate j of length < x such that also rv(x') -V, in case rm = (E,Hi-j). Proofs By assumption H is of form (1 ) HmYt, x Z] ] YK[ Z] V.... V m[Xnn Z]. 10

Now let i j be any n 2-predicate and let r = ~(E,H,i j), s = ~(E,L,i). Then by definition 3 and the construction of L, r(o) E (2) r(t') = H[r(t),i(t) j(t)] s(o) E (3) (t = _H[s(t),i(tr-V] VH[s(t),l(t)] hold for all t. Making use of (1), (2), (3) it follows by induction on t that (Vt)[r(t)D s(t)]. Thus part (a) of the lemma is established. Next let i be any n-predicate, let s = f(E,Li), and suppose that sv(x') \f. Then by definition 3 the predicates i and s satisfy (3) for all t, so that by (1) we obtain sp(o) Ep p = l,.....,m (4) sp(t) V Sv(t)KpIV[i(t) Y],p = l,..,m v=l,..,m Y= A, V Now we stepwise choose a sequence of truth values j(x),....,j(o) and a sequence of indices Vx+l.....Ivo according to the following specifications. I. Let vx+l be v. II. If Vy+l has already been obtained choose vy,j(y) such that svy(y) and Kvy+l,V [in(y) j(y)] hold. That these choices are possible clearly follows by the assumption Sy(x) - Vand (4). Let now the values r(o),.....r(x') be defined from i(o),....,i(x), j(o),.....,j(x) by the recursions (2), so that by (1), rp(o) Ep; rp(t') =-=lv.,m r(t)Kp, [i(t) j(t)] for t < x. Then by using II one stepwise obtains rvO(o) KvIvO[l(o Cj(o)]...rvX(x), Kvx+lx[(i(x) (x)], rvx+l(X+l). Therefore by I, rv(x') - V. Thus by extend11

ing the sequence j(o),....,j(x) letting j(t) - ^Afor t > x, we obtain a special predicate j such that j is of length < x, and rv(x') = NVin case r S(E,Hin). Therefore also part (b) of the lemma is established. Lemma 5. For every n/m-automaton with output Em Hm U one can construct a number h and an output W such that (a) U[Y]DW[Y] (b) Z1 YAZ2 H[Z1,p_] A....^ h H[Z_[l,__] 0.)- U[Z] V-....V U[Zh (c) If U[Y]DU[H[Y,Aj]] then W is special output of E H. Proof: The construction of h and W[ym] from Hm[ym,Xm] and U[Y ] proceeds by the following rules, I. Let UO[Y] be-V, let U1[Y] be U[Y]. II. If Uk[Y] = Uk+l[Y] is not tautologous, let Uk+2[Y] be Uk+l[Y]VUk+l[H[Y,A]] III. If Uk[Y] Uk+l[Y] is tautologous, let h be k, let W be Uk, and stop. From this construction it is clear that Uo[Y] U1[Y], U1[Y]D U2[XY,. Because there are only a=2(2m) truth-functions on m arguments the construction must reach a stage k<a such that Uk and Uk+l denote the same truth function, i.e., such that Uk[Y] Uk+l[Y]. The next step in the construction then clearly must use the stoprule III. Thus the construction always ends in k<a steps, yielding an h and a W. Suppose now for example that h turns out to be 3, so that W is U3 and U3 - U4. Letting K[Y] stand for H[Y,A] it follows from the construction, (1) U2[Y] U[Y]VU[K[Y]], and (2) U3[Y] - U2[Y] V. Uz[K[Y]], and (3) U4[Y] - Us-[Y]VU3[K[L]]. By (1), U[_Y]DU2[_] and by (2), U2[Y]DU3[_]. Therefore U[_Y]DUs[Y]. Because W is U3 this established part (a) of the lemma. 12

Next suppose Z1 - Y1, Z2 K[Z1], Z3 - K[Z2], and U3[Y1]. Then by (2), U2[Z1]VU2[Z2]. This yields by (1), U[Z1]VU[Z2]VU[Z3]. Because U3 is W and K[ ] is H[-,/A]- this established part (b) of the lemma. Now suppose U[Y]3U[K[Y]]. Then by (1), U2[Y]PU[K[Y]], and also by (1), U[K[Y]]DU2[K[Y]]o Therefore U2[Y]iU2[K[Y]]. From this, by using (2), U3[Y]D U3[K[Y]] is similarly obtained. But also U3[K[Y]]D U3[Y], because of (3) and U3 - U4. Thus, U3[Y] - U3[K[Y]]. Because U3 is W and K[Y] is H[Y,V] this means that W is a special output of E H. This establishes part (c) of the lemma. Lemma 6: To every n -/m-automaton with special output Em Hm U in expanded form one can construct a n/m-automaton with special output Em Lm W such that for every special n-predicate in, ie(G,L,W) - ( j)[i je(E,H,U)] and E_ L W is again in expanded form. Proof: The construction of Lm, W is as follows, (1) L[Y,X]: H[Y,X -V]VH[Y,X.\.] (2) h, W[Y]: apply construction of lemma 4 to E L U. Assume now that E H U is in expanded form and U is special. Then by definitions 2, 4, (3) U[Y]: Y VY2V.-OV Yk (4) U[Y] - U[H[Y,J A t]] By using (4),), (, (1), (3) in this order one shows U[Y]DU[L,[Y,J]]. Therefore, by (2) and lemma 5 (c), W is a special output of E L. Next assume i jeD(E,H,U), and let r = ~(E,H,i j) and _s = ~(E,L,i). Then by definition 3, (3x) (Vt)x U [r(t)], and by (1), lemma 4(a), (Vt) [r(t)Ds(t)]. 13

Therefore it follows by (3) that (3x) (Vt)x U[s(t)]. By (2) and lemma 5(a) this yields (3 x) (V't)x W[s(t)]. Therefore, by definition 3, ice(E,L,W). Thus we have shown that (3 j)[i jS(E,HU)] D iEc(E,L,W). Assume now that icP(E,L,W), and let s = (E,L,i). Then if ~ is the length of i it follows by (*) that W[s(+l)]. Because of (3) and lemma 5(b) this implies that U[s(y+l)]V.....VU[s(%+h+l)], and by (3), there are v,p < h such that sv(%+p+l) - E o Because E H is in expanded form and because of (1) we therefore can apply lemma 4(b) to conclude that there is a j of length < l+p such that rv(1+p+l) -V, for r = ~(E,H,i j). Using (3) we obtain U[r(X+p+l)]. Now observe that i(t) =-, and j(t) =-, for t>l+p. Because U is special output of E H it therefore follows that (Vt)'+p+l U[r(t)]. By definition 3 this means that i j~e(E,H,U). Thus we have concluded the proof of lemma 6 by showing that ice(E,L,W) D (3j)[i jE(E,HU)]. 4. ANALYSIS AND SYNTHESIS We begin by establishing a synthesis result for formulas of W.2.A. which do not contain predicate-quantifiers. Using the lemmas of Sections 2 and 3 one then easily extends the result. Lemma 7: To every formula C(in) of the form K[i(o)]A(Vt)B[i(t),i(t')] one can construct a n/m-automaton Em Hm and a special output U[Ym] such that P(E,H,U) 1C(1). Proof: We first determine whether or not B[~A,YA]. In case B[-A,A-], we take for E H any automaton and for U the output A. Then clearly U is special out14

put and P(EH,U) = iC(i) are both empty. Thus in this case Lemma 7 is established. Let us next consider the case B[A_,A-]. Then we take m to be n+2, and Em to be Vm. Hm we define as follows. Xn HV[Yn Z1 Z2, Xn]: Xv for v = 1,....., n Hn+l[Yn Zi Z2, Xn] Hn+2[Yn 1 Z2, Xn] Z1K[Xn]V Z1Z2B[yn,Xn]. As output we choose the formula U[yn Zi Z]: Z1K[n]V A1Z2B[Yn, n]. Noting that B[AYV], and using definition 2, one easily checks that U is a special output of Eo. Furthermore, the transition-recursion of E H is clearly equivalent to the recursion rv(o), v = l,....,n+2 rn+2(l) - K[i(o)] rv(t') - iv(t), v = l,....,n rn+l(t') - A rn+2(t'') rn+2(t') B[i(t),i(t')] and therefore the operator rm = (EIH,in) can also be defined by rv(o) - V, v = 1,....,n+2 r(t') - iv(t) v = l...,n rn+l(t') = rn+2(t') - K[i(o)]A(Vx) B[i(x),i(x')] Consequently, the output-operator u = v(E,H,U) is defined by u(o) - K[JA] u(t') = K[i(o)]A(V x)o B[i(x),i(x')]AB[i(t),1]. 15

Because B[A,A] it follows that for any special i, u = _(E,H,U) is ultimately V just in case K[i(o)] A(Vt)B[i(t),i(t')]. I.e., by definition 3, 5(E,H,U) AC(i). Theorem 1: (synthesis) For every formula C(in) of W.2.A. one can construct a n/m-automaton E_ Hm with special output U[Ym] such that P(E,H,U) = 1C(i), i.e., such that the behavior of E H U is just the set of special n-predicates which satisfy C(i). Proof: Using Lemma 1 we first construct the formula C*(i) equivalent to C(i). Let us for example assume that C*(i) is as follows, C*(i): (Vr) (3 s) K[r(o),s(o)] A(Vt) B[i(t),r(t),s(t),r(t'),s(t')]. Next we use the construction of Lemma 7 to obtain an automaton El H1 with special output U1 such that for special i, r, s, (1) i r s cS(EzlHiU). —. K(o) A(Vt)B(t). Using Lemma 3 we next construct E2 H2 U2 in expanded form and such that (2) (E2,H2,U2) = D(El,_,U1). By repeated application of the construction of Lemma 6 starting with E2 H2 U one obtains E3 H3 U3 such that for special i, r, i r eP(E3,H3,U3).. (3 s)[i r s e6(E2,H2,U2z] and therefore by Lemma 2, (3) i -r e(E3,H3,U3).-. (3 )[ s e(E2,H2,U2)] Because the complementation destroys the expanded form we are forced to use Lemma 3 again to obtain E4 _4 U4 in expanded form and such that (4) B(E4,H4,U4) = (E3,H3,U3) By repeatedly applying Lemma 6 we next construct E5 H5 U5 such that for every 16

special i, i Ec(E5,H5,U5). — ( r).i r E(E4,H4,U4) and therefore by Lemma 2, (5) EH r) (E4,H4,U4) From (1),......(5) it clearly follows that i E(E5,H5,U5).-. C*(i). Because C* is equivalent to C this shows that the behavior of Es 15 U5 is \C(i). We next obtain a rather strong converse to Theorem 1. Theorem 2: (analysis) To every n/m-automaton with special output Em Hm U one can construct a formula C(in) of W.2.A. such that iC(i) = ((E,H,U), and such that furthermore C(i) is of the form (3 jP).K[j(o)] A(Vt)B[i(t),j(t),j(t')]. Proof: By definition 3 it is clear that for every special i, i e~(E,H,U). ( r)[r(o)-EA('Vt)[r(t')=H[r(t),i(t)]] A (x)(Vt) U[r(t)]]. However, the range of (3r) in this formula may not be restricted to special predicates. On the other hand, because U is assumed to be special, the formula may be slightly modified so that the range of (e r) can be restricted to special predicates. Namely, it is clear that for any special i, (1) i 6 (E,H,U)..=..( r)(_x). r(o)-E (Vt)o[r(t')_ H(t)]A(Vt)x[i(t)=AU r(t)]]. It remains to change this definition of P in W.2.A. to one of the simple form required in Theorem 2. This is accomplished by using the following device for changing the individual quantification (3 x) to a quantification ( j) over restricted predicates, (2) i E(E,H,U)....( r)(3j). (Vt)[j(t')D j(t)] A r(o)mE A(Vt) j(t)ID [r(t')=H(t)]] A ( t)[j(t) r) [i(t)=A U[r ( t)]]]. To see that (2) is correct in case (3r)(3j) is interpreted as ranging over special predicates we observe that the right sides of (1) and (2) are equivalent 17

because of an obvious one-to-one relationship between numbers x and restricted predicates j satisfying (Vt)[j(t')D j(t)]. Thus the right side of (2) is a formula C(i) as required in Theorem 2. 5. DEFINABILITY IN W.2.A. We will use the notation "[0, x+l, 30i]" to denote W.2.A. This is intended to indicate that we are dealing with an interpreted system which besides first-order quantification over natural numbers contains 0, the function x+l, and quantification over special predicates. Similar notations for other interpreted systems, all containing first-order quantification over natural numbers, are used below. "o30" indicates quantification over eventually constant monadic functions from natural numbers to natural numbers. The following systems are known to be very strong in the sense that all recursively enumerable predicates are definable in each. [0, =, x+l,_ %ot] Go'del [5] [0, =, x+y, x.y] Godel [5] [0, x+l, 2x, 0oi] Robinson [14] (In fact these systems are equivalent in the sense that the same predicates on natural numbers can be defined in each.) In contrast we will now show that [0, x+l, 3oi] is much weaker, in particular the only monadic predicates on natural numbers definable in W.2.A. are those which are ultimately periodic. Definition 5: A formula of W.2.A is said to be in normal form if it is of the following type, C(im, xl,..., Xp): (3 m)[K[j(o)] A (\t)B[i(t), j(t), J(t')]A Ai[j(xz)] A..oA Ap[j(Xp)] 18

Theorem 3: For every formula C(in, xl,...,Xp) of W.2.A. one can construct an equivalent formula C*(in, xj,...,Xp) which is in normal form, i.e., every predicate on numbers and special predicates definable in W.2.A. is definable by a formula in normal form. Proof: Suppose first that A(in) is a formula without free individual variables. Then by Theorem 1 one can construct an automaton E H with special output U such that ((E,H,U) = 4A(i). Next, by Theorem 2 one can construct a formula A*(i) in normal form such that "A*(i) = P(E,H,U). It follows, iA(i) = 4iA*(i). Thus, (1) If A(i) does not contain free individual variables one can construct a normal A*(i) equivalent to A(i). Let us next start with a formula C which contains free individual variables, say for example C(i,xi,x2). Let A be defined thus, A(i,sl,s2): sl(o) A s2(o)A (A t)[sl(t') D sl(t)] ( t)[s2(t'D S2(t)]A Wtit2)[si(t1);tl)2~(t2)2( ) D C(itl,t2)]. It is then easy to see that A(i,sl,s2) C(i,xl,x2), in case xl+l, x2+l are respectively the length of the special predicates slS2*. Re-stating this we obtain C(ixl1x2).- (3 ss2) [A(i,sls2) /^ si(x1)l'(xl) A S2(X2)s2(x>)], and therefore, (2) C(i,x1,x2)..-.. (3sls2rlr2).A(i,ss2) / (Vt)[r(t )-s[(t) )] /N (Vt)[r2(t)=s2(t') ] Sl(xl)'1(xi) / S2(X2)r2(X2). Finally we use (1) to obtain a A*(i,si,s2) in normal form and equivalent to A. Replacing in the right side of (2) A by A* and performing some obvious shifts of quantifiers will then yield a C* equivalent to C such that C* is in normal form. 19

Corollary 1: There is a procedure for deciding whether or not a sentence of 2 W.2.A. is true. Proof: Because of Theorem 3 it is sufficient to indicate a procedure which decides the truth of sentences C of form (3I) K[j(o)]A (Vt) B[j(t), j(t')]. We may furthermore assume that B[A,-], because otherwise the sentence C is clearly false in W.2.A. C then is equivalent to the assertion, (1) There is an x and a sequence of states Yo -....,x such that K[YO], B[Yo,Yl],... *~*, B[..,Y] L -Yx Note that in case x > k = number of states of i there must occur a repetition in the sequence Y, Y1,....,Yx, say Yy Yz for some 0 < y < z < x. Then if Yo, y'.y,...,Yz..Yx is a B-sequence, the shorter sequence Yo,'..',Y y, Yz+l,1.Yx is still a B-sequence. Consequently the assertion (1) is equivalent to, (2) There is an x < k = number of states of i, and there is a sequence of states Yo, '' Yx such that K[Lo], B[Yo,Yl],..~., B[YX_-1Yx], x A. Because there are only a finite number of sequences oY**~ _x*,, x < k, it is clear that one can effectively check whether or not (2) holds. Because C is equivalent to (1), and (1) is equivalent to (2), this establishes Corollary 1. Corollary 2: Every formula C(x) of W.2.A. defines an ultimately periodic set xC(x) of natural numbers, i.e., there are numbers ~ (phase) and p (period) such that (Vt)[C((+t+p) - C(+t). 2. As R. L. Vaught remarks, this result can be obtained from a theorem of A. Ehrenfeucht; see Robinson [14]. 20

Every ultimately periodic set of natural numbers is definable in W.2.A. by a formula C(x), Proof: By theorem 3 we may assume that C(x) is of the form C(x): (3 J).K[(o)] A (Vt)B[j(t), j(t')] A A[j(x)]. Now, let Y1,....a be those states Y of j for which A[Y], and for v = l,...,a let, C~(x) stand for (3j)[K(o) A (Vt)B(t) A j(x) Yv]. Then clearly, C(x) C(x) V... \/Ca(x), Cv(x) ( ( j)[K(o) / (Vt)o B(t) A j(x) = Y] A (3j)[j(o) - Y A (V t)B(t)] hold in W.2.A. Therefore, if li,..*..Ib (b < a) are those states among Yl,...a' for which (3j)[j(o) Y A (Vt)B(t)], then C(x) = (3j).K(o) A (Vt)o B(t) A [j(x) Y1 V....Vj(x) Yb] holds in W.2.A. Next let k = number of states of j, and let Yl,..,Yb',..,Yk be the states of j, and let rl,...,rk be defined by the recursion rv(o) K[Y],v=l,..., k (1) rv(t') ri(t)B[Y1,Yv]v...vrk(t)B[Yk,Yv],vl,....,k One then easily shows that (3j) [K(o) A (Vt)o B(t) A [j(x) Y1V.. V j(x) Yb]] holds if and only if [rl(x) \/... V rb(x)]. Consequently, xC(x) = x[rl(x) V.o \/ rb(x)]. Now r has 2k states, therefore a repetition must occur in r(o),...,r(2k), say r(Z) - r(%+p) whereby i+p<2k and 0 < p. By (1) it then follows that r(%+t) - r(%+p+t), for all t, so that x[rl(x)V...Vrb(x)] = xC(x) is ultimately periodic with phase ~ and period p. The second part of Corollary 2 is best shown by first obtaining definitions in W.2.A. of the relations x=y, x<y, x2y (mod p), for fixed p. Note also that the selection of Yll^*.~lb from Y1,...,Ya in the proof of Corollary 2 can be effectivelymade (by Corollary 1). As a result one can ef21

fectively find the phase and period of the set xC(x). By using similar methods to those employed in the proof of Corollary 2 one shows that every relation R(x,y) definable in W.2.A. must be of the form R(x,y) V [x<y A Av(x) A Bv(y-x)] vV[y<x A Cv(y) A Dv(x-y)] whereby Av, BV, Cv, are v=l,. ~ a v=l, ~~.,c ultimately periodic. In particular y = f(x) is definable in W.2.Ao if and only if it is ultimately periodic, i.e., satisfies f(1+x+p) = f(P+x) + q, for some f,p,q (compare this with Robinson's [14] result on [O,x+l,2x,j i]). However, the following result seems more informative. Corollary 3: If R(x,y) well-orders a subset of natural numbers and is definable by a formula C(x,y) of W.2.A., then the type a of R is less than w2. Conversely, if a is an ordinal less than o2 one can find a formula C(x,y) of W.20A. such that xyC(x,y) is an aC-well-ordering of all natural numbers. Proof: Suppose R(x,y) is a well-ordering of natural numbers of type a, and for < a let An be the initial segment relative to R of type r. Then from a definition C(x,y) of R in W.2.A. one can easily obtain definitions of the sets Ar, for r < o; so that by Corollary 2 the sets Ar,r < w2 are ultimately periodic. Now it is easy to see that there is no strictly increasing W2-sequence of ultimately periodic sets of natural numbers. Consequently if R(x,y) is definable in W.2.A. then its type a must be less than w2. To indicate a proof of the second part of Corollary 3, let us consider the case a = c3 + 2.. Because one can define x-y(mod 3) and x<y, and x=y in W.2.A., it is clear that one can also define a relation R(x,y) which well-orders the natural numbers in sequence, 6,9,12,^......,1,4~,7,To..,2,5, 8,......,0,* 3. 22

It seems clear that one could use Theorem 3 also to investigate the nature A of sets iC(i) definable in W.2.A. by formulas with free predicate variables. However, a rather concrete characterization of these sets of finite sets is given by Theorems 1 and 2, namely Corollary 4: The sets of n-tuples of finite sets definable in W.2.A. are exactly the behaviors of special outputs of finite automata with n-ary input. We will terminate this section with the presentation of a first-order theory which is equivalent to W.2.A. in a very strong sense. For this purpose note that f(i) = (2X) i(x) defines a one-to-one mapping f from all special predicates (finite sets) of natural numbers onto all natural numbers. f(i) = y simply means that for j = length of i, i(o)i(l).... i(g) is the binary expansion of y. This mapping f induces a natural one-to-one correspondence between relations on special predicates and relations on natural numbers, let us say that R(il,....,in) and S(xi,....,xn) are adjoined to each other in case R(il,....,in) S(f(il),.... f(in)), for all special il,...,in. Let furthermore "Pw2(x)" stand for "x is a power of 2." Theorem 4: The first-order theory [=, +, Pw2] is equivalent to the weak secondorder theory [0, ' i] in the sense that a relation S(xl,....,xn) on natural numbers is definable in [=, +, Pw2] if and only if its adjoined relation R(i,..~.,in) is definable in [0, ', 30i]b Moreover, from a definition C(xi,...,xn) of S one can effectively obtain a definition D(il,...,in) of R, 23

and conversely. Proof: Let S(i, j, s) be the adjoined to x+y=z, i.eo, "S(i, j, s)" stand for "f(i) + f(j) = f(s)." Then by formalizing the procedure of adding natural numbers in binary expansion one obtains the following definition of S in the weak second-order theory [0, ', i] S(i, j, s): (3r).r(o) A (Vt)[r(t') - [r(t)i(t)V r(t)j(t) V i(t)j(t)]] A (V-t)[s(t) - [r(t) V i(t) V j(t)]] whereby "X VY" stands for "XY V YX." Furthermore, if U(i) is the adjoined to Pw2(x); then U(i) (3 x) (Vt) [i(t) - (t=x)] is a definition of U in [o,',-oi]. To prove Theorem 4 in one direction it therefore is sufficient to indicate a translation of formulas C of [=, +, Pw2] into formulas C* of [o, ', U, S, 30i] such that C*(il,.~.,in) and C(xl,...,Xn) define adjoined relations. Because every formula C of [=, +, Pw2] is easily changed to an equivalent one in which no iteration of + occurs, the following specifications yield the required translation.. 1. [xv+x,=xp]* is S(iv,i,ip), 2. [Pw2(xv)]* is U(iv),.3 [C \D]* is C*AD*, 4. [-C]* is C*, 5. [( xv)C]* is (3 iv)C*. To prove Theorem 4 in the other direction we note that E(x,y): Pw2(x)A ( uv)[(y = u+x+v) A (u<v) A [v=o V2x<v]] is a definition in [=, +, Pw2] of "x is a power of 2, and x occurs in the representation of y as a sum of powers of 2." It therefore is sufficient to indicate a translation of formulas C of [o o,, i1] into formulas C~ of [=, +, Pw2, E] such that C_)xl,...,xn) and C(il,....,in) define adjoined relations. If one notes that i(x) means the same as E(x,f(i)), and that every formula C(ii,....,in) can be changed to an equivalent one in which o does not occur and ' only occurs in parts 24

of form ( t)[j(t) = i(t')], then it is clear that the following specifications yield such a translation. We single out the individual variable t and divide the remaining ones in xl,x2,..... ';yly2*. O. In [o,,0oi] we make use of Y1,Y2,..., and t only (while it is intended that in [=, +, Pw2, E] the range of the y's is restricted to Pw2). 1. [iv(y)]~0 is E(yP,xv), 2. [(It)[it(t) iv(t,)]O is [xv = x + x V xv = x, + x + 1], 3. [CAD]O is C~/AD0 4. [-C]I~ is -C, 5 [( iv) C]~ is (3xv) CO, 6. [(3Yv) C]~ is (3yv)[Pw2(yv) A C]. By Theorem 4, Corollary 1, Corollary 4 one clearly obtains, Corollary 5: The first-order theory [=, +, Pw2]is decidable. A relation R(xi,...,xn) is definable in this theory if and only if its adjoined S(ii,....,in) is the behavior of a finite automaton with special output. One might attempt to prove Corollary 5 directly by extending Presburger's [10] method for [=, + ]. Corollary 1 would then follow by Theorem 4. Let Q2(x) stand for "x is a square." Then by Putnam [11], the first-order theory [=, +, Q2] is undecidable. It is interesting to compare this with Corollary 5, and one easily extends the results as follows, Theorem 5: The first-order theory [=, +, P] is (a) undecidable in case P(x) is ultimately a hyper-arithmetic-progression, i.e., in case P ultimately consists of the values of a polynomial of degree > 2. (b) decidable in case P(x) is ultimately a geometric progression. To better understand the jump in strength from [=, + ] to [=, +, o] it would be interesting to know whether there is a recursive predicate P(x) such that [=, +, P ] is undecidable without admitting definitions for all recursive predicates. 25

6. OTHER CONCEPTS OF FINITE AUTOMATA Clearly our concept of finite automata is very closely related to that of Church [3]. What we have callled the transition-recursion and output-recursion of an automaton (with output) are restricted recursions in his sense. While Church allows instantaneous action (the input at time t directly affects the transit and output at the same time t), it is just a matter of convenience that we have presented our theory in terms of automata with delayed action only; also our restriction to special outputs is inessential (see Section 7). The behavior-concept used implicitly by Church is that of the operator u = 4(i) defined by the output-recursion. We hope to show elsewhere how his synthesis procedure (Case II) can be extended to condition-formulas containing predicatequantifiers. Recursions like our output-recursions were first used by Burks and Wright [2]. Their concept of well-formed logical net is equivalent to our finite automata, except that instantaneous action occurs in logical nets. In the following discussion it is intended that a n/m-automaton (whose input has n binary components) represents in coded form a 2n/2m-automaton (whose input has one 2n-ary component. Let 7Z = [(, <V),, = Zg x.... Z (n factors). Under the conventional interpretation of propositional formulas Em denote an element atc Z., while Hm[Ym, Xn] may be interpreted to denote a function T: m x —. Thus, with an n/-automaton EIHm[ym, Xn] is associated a system <, Zm, a, T > calledits transition system. The elements of Zn and Z, are respectiely called irut states ani transitstates, a is the initial-state and T the transit-function of the automaton. An output U[Ym] may be interpreted to denote a subset of transit-states. These re26

marks are intended to indicate how our notion of finite automata (with output) is related to those used by Moore [9], Myhill [8], Rabin and Scott [13], and others. While our notion is syntactic these authors take automata to be what we called transition systems (with output set). The latter definition is not correct if the mathematical concept "finite automaton" is to correspond to physical structures. Two physical systems (two syntactic systems) can be quite different structurally (syntactically) and still display the same transitionsystem. Also from a purely mathematical point of view it is not advisable to identify automata with their transition-structure, as it then becomes impossible to rigorously state existence of algorithms as, for example, in our Theorems 1 and 2. The point is that an algorithm is better thought of as applying to and yielding syntactic entities. We will now indicate how our theory of behavior can be extended to automata with many inputs, each of which may have any number of binary components. For this purpose it is convenient to extend propositional calculus so as to contain u lists, each list consisting of w propositional variables. A notation like "H[Xn; _k; zh]" will be used to stand for a formula of (extended) propositional calculus in which the variables X, Y, Z and only these may occur, and furthermore the variables X belong to a first list, which precedes a second list to which the variables Y belong, which precedes a third list to which the variables Z belong. Definition 1', A (finite) n_;.....;n/ma utoma ton with inputs Xn,...,X and transit Lm is a 2m-tuple E _ Hm[Ym; Xl;.....; Xkk] of propositional formulas (no variables occur in Em). 27

A (binary) output of such an automaton is a propositional formula U[Ym], where ym is the transit of the automaton. It is clear how one extends the notion of transition (output)-recursion, introduced in Section 3, to n,;.....; nk/m-automata (with output). Also for the extension of the concept of special output we refer to Definition 2 in Section 3. Definition 3'. The behavior (Em, Hm, U) of a ni;....; nk/m-automaton with special output is the k-ary relation which holds for the special nl-predicate ii,....,n k-predicate ik, just in case (3x) (Vt)x U[r(t)], whereby rm = (E, H, il;....;ik) is obtained by the transition-recursion of E H. To obtain an extension of the analysis and synthesis Theorems 1 and 2, we extend W.2.A. to contain w lists, each list containing w predicate variables. A notation like "C(i;j)" will be used to denote a formula of (extended) W.2.A. in which the variables i, j and only these may have free occurrences, and such that the variables i all belong to the same list which precedes a list containnl n2 n3s ing all the variables j. A formula C(il; i2; i3 ) of W.2.A. defines a ternary relation 1, i2, s C(il; i2; i3) on special nl-predicates, n2-predicates, n3-predicates. n. nk Theorem 1'. (synthesis) To every formula C(i;....;k ) of (extended) W.2.A. one can construct a nl;....;nk/m-automaton Em Hm with special output U such that the behavior P(E, H, U) is the k-ary relation l1;....;ik C(il;....;ik). Theorem 2' (analysis) To every nl;....;nk/m-automaton Em Hm with special output U one can construct a formula C(il;o....;ik) of W.2.A. such that the k-ary relation i.... C(i;...;k) is the behavior 3(E, H, U). 28

To prove Theorem 1' one at first simply disregards the grouping of the q = nln2.... nk variables in the formula C(inl;....;i k) and constructs the q/m-automaton with special output according to Theorem 1. By properly grouping the q components of the input of this automaton one obtains a nl;..; nk/m-automaton with special output as required in Theorem 1'. Similarly one proves Theorem 2'. It thus appears that the theory of behavior for automata with many inputs does not present any additional difficulties, in caseone works with special predicates rather than finite strings of input states. The reason for this is that a k-tuple (i1;...k4k) of special n-predicates may be reinterpreted as one special nlnn2....nk-predicate. In contrast a k-tuple (xl;....;;k) of finite strings of input states can not readily be reinterpreted as one finite string of states. This seems to be the reason that no theory of behavior of automata with many inputs occurs in the literature. Our concept of finite nl;....;nk/m-automaton still is somewhat specialized in that the components of each input and the transit are binary (i.e., can take values in Zg = ( -A, V ) only). Because we allow many components to occur in an input (transit) there is of course the possibility of indirectly dealing with automata whose sets of input states (transit states) have any finite cardinality, by way of binary coding. However, to obtain an entirely satisfactory theory of nl;....;nk/m-automata (for any numbers nl,...,nk, m one would have to replace Z2 by Z2,Z3,~~~~ (Zk being a set of k elements), and one would have to set up a calculus PCo to replace propositional-calculus (PC2), such that PC, contains variables Xk ranging over Zk and provides names Hk[Xkl,...,Xka] 29

for all functions T: 1l x.... ka- Zka. To generalize the results obtained in Section 4 one would extend W.2.A. to contain variables ik ranging over monadic functions from natural numbers to k which ultimately take the fixed value A k e Zk. It seems clear that this program could be carried out, and moreover the form of the presentation in Section 4 would remain essentially unchanged. We did not present our results in this general version because no calculus PCo is available in the literature. 7. FINITE STRINGS VERSUS SPECIAL PREDICATES; REGULAR RELATIONS According to our definition the behavior f of an n/m-automaton with special output is a set of special n-predicates (infinite strings of input-states which are ultimately -An). Simplifying Kleene's [6] theory of regularity, Myhill [8], Rabin and Scott [13], and Copi, Elgot and Wright [4] work instead with the set Psg consisting of all finite strings of input states which turn on the output. In this approach the restriction to special outputs is not needed, so that it may seem at first that our concept of behavior is too specialized. However we will see in this section that on the contrary our theory of behavior is more general in that it yields a rather natural extension of the concept of regular set of finite strings to regular relation on finite strings. We begin by observing that there is a one-to-one mapping f of all finite strings of elements of n onto all special r-predicates in which have the property i()= Vn, if i is the length of i. Namely, = f(Y ''_h) - (t)th[i(t) Yt]A [i(h') r] (t)t>h,[(t)_]. 3O

In particular the empty string corresponds to the predicate i(o)=r i(t')-A. To simplify the presentation we will identify finite strings with the corresponding n-predicate, i e., (**)A finite n-string of length X is a special n-predicate in of length P+1 which takes the value i(1')=-V. The definition of finite string behavior which occurs in the literature can, in our notation, be formulated thus, Definition 6. The sg-behavior of a n/m-automaton E H with arbitrary output U is the set Psg(I, H, U) consisting of all n-strings i such that U[r(j+l)], if g is the length of the string i and r = _(I, H, i) is the m-predicate determined by the transition-recursion of E H. Theorem 6. A set 3 of n-strings is the sg-behavior Psg(E, H, U) of some n/mautomaton with arbitrary output if and only if it is the behavior 3(I, G, W) of some n/q-automaton with special output. Proof Suppose first that o = Psg(E, H, U), whereby U is an arbitrary output of the n/m-automaton E H. Let the n/m 2-automaton I G and its output W be defined by, Iv Ev GV[Ym Z; Xn]: HV[Y, X], =l,....,m Im+l Gm+ l[) Z; X ] [X I =V] U[Y]V[X A]Z W[Ym Z] Z Then clearly Gm+l [Y Z';A] - Z, and therefore W[G[Y Z;J]] - W[Y Z], which by definition Z means that W is special output of I G. Furthermore note that the transition-recursions of the two automata are, 31

r(o) -E r(o) E, s(o) -A(1) (2) r(t') H[r(t),i(t)] r(t')= H[r(t),i(t)] r(t')= [i(t) = -V] U[r(t)]V[i(t) - AX]s(t) Now let i be any special predicate of length I. If ie(I, G, W) then by (*) of Section 3 and (2), W[r(X+l) s(X+l)], i.e., s(O+l). Therefore by (2), [i(t) ~V] U[r()]V[i(i) = ^]s(f). Because I is the length of i, i(t) = A is not the case, so that [i(t) -V]U[r(X)]. Consequently by definition 6, ieCsg(E, H, U). These steps are reversible, so that also iepsg(E, H, U) implies ie(I, G, W). Thus we have constructed an automaton II G with special output W such that also 3(I, G, W) = 3. This proves Theorem 6 in one direction. Suppose next that 3 = 3(I, H, W), whereby I H is an n/m-automaton with special output. Define U[Ym]: W[H[ym,n]]. Noting that 3 consists of finite n-strings only, and using Definition 6 and (*) of Section 3, one easily shows that 3sg(I3 H, U) = 3(I, H, W) = 3. This establishes Theoran 6 in the other direction. Theorem 6 shows that the restriction to special outputs in our analysis and synthesis Theorems 1 and 2 (Section 4) is not a limitation in generality, but rather a natural feature which appears when one works with special predicates instead of finite strings. In fact it now is easy to obtain synthesis and analysis theorems in terms of sg-behavior and without restriction on the outputs. For this purpose we remark that the set of all finite n-strings can be defined by a formula Sgn(in) of W.2.A., Sgn(in): (3j).j(o)A(Vt)[j(t') D j(t)][j(t)J(t')Dl(t) -V] [J(t)D l(t) -_ and we define a formula C(in) to be an sg-formula in case (Vi) C(i)D Sgn(i) 32

holds in W.20A, (by Corollary 1 one can effectively decide whether a formula of W.2.A. is a sg-formula). Theorem 7. Analysis: To every n/m-automaton E with arbitrary output U one can construct a sg-formula C(in) of W.2.A. such that C(i) defines the sg-behavior Psg(E' H, U). Synthesis: To every sg-formula C(in) of W.2.A. one can construct a n/m-automaton E H with output U such that Psg(E, H, U) = eC(i). Proof: By Theorems 1, 2, and 6. Note that we actually established an effective version of Theorem 6. In short form Theorem 7 states that the sg-behaviors of n/m-automata with arbitrary (binary) output are exactly the sets of finite n-strings definable (by sg-formulas) in W.2.A. It has been shown that the sg-behaviors are the regular sets of finite strings (references at the beginning of this section). Thus, Theorem 8. For any set D of finite n-strings the following are equivalent conditions, (1) D is the sg-behavior of an n/m-automaton with arbitrary output. (2) v is the behavior of an n/m-automaton with special output. (3) 3 is definable in W.2.AJ (by a sg-formula). (4) 3 is regular In the literature sg-behavior has been studied only for automata with one input. Consequently the concept of regularity has been limited to sets. On the other hand we have seen in Section 6 that our theory of behavior can easily 3

be extended to automata with many inputs. On the basis of Theorems 1', 2' (Section 6) and Theorem 8 the following definition suggests itself as a natural extension of the concept of regularity. A formula C(i;.....;kk) of (extended) W.2.A is called an sg-formula if (V8 i1. k) -(il;;...;..aJ)D Sgnl(ii).... Sgnk(ik) holds in W.2.A. Definition 7. A relation R(il;o....;nk) on special nv-predicates (finite nvstrings) is regular if it is definable by a formula (sg-formula) C(i1l;...;) of extended Wo2oA. Theorems 1' and 2' can now be restated in the following short form, Theorem 8'. A relation R(i;.....; ) on special n-predicates (finite n strings) is the behavior P(E, H, U) of a nl;....;/m-automaton with special output, if and only if R is regular. In case one prefers to work with finite strings one could extend Definition 6 to a definition of sg-behavior of many-input-automata with arbitrary output, so as to obtain a corresponding extension of Theorem 6, and Theorem 7. A binary relation on strings which naturally arises in connection with a n/m-automaton Em Hm is its equi-response relation incn (mod E H). Two finite strings i, j of input-states are in this relation if they produce the same transit-state, i.e., if r(i') = s(h') in case r = H(E 1 H, i), s = I(E, H, j), X = length of string i, and h = lengths of string j. It is easy to construct a n;n/q-automaton with special output whose behavior is the relation in<jn (mod E H). Therefore, by Theorem 8', the equi-response relation of any n/mautomaton is a regular relation on finite n-strings. In k-ary number theory 34

(i.e., the theory of finite strings on the alphabet 1,....lk) the equi-response relations module k/q-automata take the place of conventional congruence relations in ordinary (1-ary) number theory. Correspondingly the concept of regularity is the natural analogue in k-ary number theory to ultimate periodicity in ordinary number theory, Another example of a regular relation on special predicates is the adjoined S(i,j,s) under binary expansion (see Section 5) to the relation x+y=z. Moreover Theorem 4 may be restated as follows. A relation R(xl,...xk) is definable in the first-order theory [=, +, Pw2] if and only if it is the adjoined under binary expansion to a regular relation S(ilo...,ik) on special predicates. In case one prefers to deal with finite strings the following modified concept of binary expansion is appropriate. If ao,..,ah are either 1 or 2 then aoal....oah represents ao2~ + a121 +...... + ah2h. In particular the empty string represents the number 0. It is easy to see that this yields a one-toone mapping x = g(i) from all finite 2-strings to all natural numbers. Furthermore one can modify the proof of Theorem 4 to obtain; a relation R(x190o...xn) is definable in [=, +, Pw2] if and only if its adjoined S(ii,..oo.in) under modified binary expansion is a regular relation on finite 2-strings. Consequently the following two conditions on a relation R(xlyooooxn) on natural numbers are equivalent. (1) The adjoined S(il,...,ik) of R(xl,....xk) under binary expansion is a regular relation on special predicates (2) The adjoined Ssg(ii,oo.,ik) of R(x,.o..x,xk) under modified binary expansion is a regular relation on finite 2-strings 35

Let us call such a relation R a 2-regular relation on natural numbers so that, Theorem 9. The relations definable in the first-order theory [=, +, Pw2] are exactly the 2-regular relations on natural numbers. For appropriate definition of k-regular relation (via adjoined under (modified) k-ary expansion) Theorem 9 holds if "2-regular" and'Pw2" are replaced by "k-regular" and "Pwk" (Pwk(x) means x is a power of k). It thus appears that the first-order theory [=, +, Pwk] is suitable for a study of regularity on the alphabet 11....,1k consisting of k letters. In this connection the following remarks are of interest. 1. Let Nk denote the set of all finite strings on the alphabet 11,.',lk, and let the function gk:Nk->N1(Ni = set of natural numbers) be defined by gk(o) = o gk(lvo lv1... 1Yh) = vokO + ikl +.. + vhkh. I.e., gk is that one-to-one ennumeration of Nk in which every string of length h precedes every string of length X > h, while strings of equal length are enumerated in lexicographic order reading from right to left. The inverse gkl yields the modified k-ary expansion of natural numbers. Let +k denote the adjoined to +, i.eo, x +k = = g (gk(x) + gk(y))' for x, YENk, and let Pwk denote the adjoined to Pwk, i.e., Pwk(x) - Pk(gk(x)), for eN We remark that it is easy to set up an algorithm for calculating x +k y (similar to the conventional algorithm for addition in ordinary expansion), and that 36

pwk(x) simply means that x is 11 or x is lk followed by zero or more occurrences of lklo Clearly < N1, +, Pwk > is isomorphic to < Nk, +k, pwk >, so that [1= +, Pwk] may be interpreted as first-order theory of either of these systems. Theorem 9 as well as the following remarks ought to be interpreted accordingly, and we will often speak of a relation when we actually mean it's adjoined under g. 2. Let x <k, y and x >k y denote respectively the initial segment relation and terminal segment relation on Nk (or their adjoined). It is easy to construct a k;klm-automaton with special output whose behavior is the relation x <k y, so that by Theorem 9 (2 replaced by k), this relation is definable in [=, +, Pwk]. Thus, by Theorem 4, The first-order theory of < Nk, <k > is decidable. In contrast we will show elsewhere that the first-order theory of < Nk, <k`, >k > is not decidable. Therefore, x >k y is not definable in [=, +, Pwk]o 3. Let x ky denote the operation of concatenation on Nk (or its adjoined on N). It is easy to see that x y = x+ klgk( y whereby lgk(x) is the length of the string x, ioe., lgk(x) = a.E. ka < x+l < ka+l However, there is no definition of x ky in [=, +, Pwk], because this theory is decidable while it was shown by Quine [12] that [=,2k] is undecidableo It can be shown that [=, ] and [=, +, K] are equivalent in the sense that the primitives of one of these theories are definable in the other 37

4. We have shown (see also Rabin and Scott [13]) that the relations x cy which are equiresponse relations modulo automata with one k-ary input are exactly those right-congruence relations of the operation xC y which divide Nk into finitely many classes. This emphasizes the analogy (remark following Theorem 8') of these relations to ordinary congruence relations of x + y e yly. We remark that while x y is not definable in [=, +, Pwk], the equiresponse relations are definable. 5. The study of congruences is fundamental in elementary number theory. It would be of great importance for a better understanding of regularity (behavior of finite automata) to develop analogously a theory of those (right, left) congruence relations of x y whose partition is finite. 6. Every ultimately periodic set of natural numbers is definable in [= +]. By Theorem 9 (extension to k) it follows, Every ultimately periodic (i.e., 1-regular) set of natural numbers is k-regular, for every k. 7. Let An k(x) stand for lgk(x) - 0 (mod n). It then is easy to see that Ank(X) is k-regular, and therefore definable in [=, +, Pwk]. Because Pwkn(x).. [Pwk(x) A An,k(x)] V x = 1] it follows that Pwkn is definable in [=, +, Pwk]. Conversely, for n > 2, Pwk is definable in [=, +, Pwkn] because Pwk(x).. PWkn(x) V Pwkn(kx) V...V Pwkn(kn-lx). Thus, for any k and n / 0 the theories [=, +, Pwk] and [=, +, Pwkn] are equivalent with respect to definability. By theorem 9 (2 replaced by k) it follows, 38

For any k and n / 0, the k -regular relations on natural numbers are exactly the k-regular relations. 8. Suppose that n > k and Pwn is k-regular. Let A(x) stand for (3t)[kx < nt + 1 < kX+l]. Then A is the set of lengths of elements of Nk which belong to the k-adjoined to Pwn. Therefore, because Pwn is k-regular it follows that A must be ultimately periodic. Let h = phase, p = period of A, and let q be the number of elements of A occurring in an interval (x, x+p-l), where x > h. Take a > h such that A(a). Then also A(a+p), A(a+2p),..., A(a+vp),..., i.e., there are b, bl, b2,... such that ka < nb+l < ka+l (1) ka+vp < nb+l < ka+vp+l, v = 1, 2, 3,... Note that there are exactly q < p members a, a2,..., aq of A occurring in the interval (a, a+p-l), and that, because n > k, no ntl nt2 can have the same length x (ntl + 1 and nt2 + 1 cannot belong to the same interval (kX, kX+l-l)). b b+l It follows that a, a2,..., aq, a+p are in order the lengths of n,, n... nb+- nb+ = n b Therefore bl = b+q, and similarly one shows by = b+vq, v = 1, 2, 3,.... It follows by (1) that (ka+vpl)lka+l < nV < ka +ll(kal), v = 1, 2, 3,.. Therefore, (kVP-k-a). v < nq < ka+ll(ka-1). kP, v = 1, 2, 3,. Letting v approach infinity this clearly yields nq = kP. Thus we have shown that for n < k, if Pwn is k-regular then n4 = kP for some pfO and q0O. This assertion extends to all n > 2; because if n > 2 there is an a such that na > k, and by 7 if Pwn is k-regular then also Pwna is k-: 39

regular, so that there are p/O and qj0 such that naq = kP. Consequently, if one defines (a) x ~ y: (3uv)[u0 A v/O A xu = yV] one obtains by 7, (b) If n > 2 then Pwn is k-regular (definable in [=, +, Pwk]) if and only if n k. (c) The k-regular relations are exactly the n-regular relations if and only if n k. (d) If n > 2 and Pwn is k-regular (definable in [=, +, Pwk]) then also Pwk is n-regular (definable in [=, +, Pwn]), and k-regularity and n-regularity have the same meaning. These facts can, of course, be stated in terms of sequences. For example, the one-to-one mapping gn gk of Nk takes regular relations on Nk onto regular relations on Nn just in case n = k. To better understand the equivalence relation a, let us say that a number x is simple if [x = OV x = lV - (3uv)(vl A x = uv)], and let spl(y) stand for that simple number x of which y is a power. Then by elementary number theoretic considerations (prime-decomposition) one shows, (e) x u.=. spl(x) = spl(y) Furthermore, the simple numbers constitute a system of representatives for a, and the equivalence class of a simple number x is {xnln/O). Because of (b), (c), (d) it follows that it is sufficient to deal with k-regularity for simple k. The theory [=, +, Pwn] is equivalent to [=, +, Pwk], for k = spl(n). (Note that a number k is simple just in case g.c.d.(al,..., an) = i if k = Pi...pn is the prime-decomposition of k.) 40

By (b) it follows that Pw2 is not 3-regular. This seems to mean that there is no finite automation with binary input and ternary output which translates binary expansions of numbers into the corresponding ternary expansions. 8. REMARKS ON FEEDBACK The essentially new element added to pure switching circuits to obtain sequential circuits is feedback. The presence of feedback in our finite automata is reflected in the recursiveness of the definition of the input to transit operation r = ~(i) of a finite automaton. In contrast, for a pure switching circuit this operation is introduced by explicit definition. The relationship of feedback to recursions was first clearly realized by Burks and Wright (2] and Kleene [6], and is emphasized by Church's contribution to automata theory [3]. A formalism, sufficiently rich to provide notations for all behaviors of finite automata, must contain an operator corresponding to feedback. In Kleene's [6] formalism of regular expressions, this operation is *. Copi, Elgot, and Wright [4] and Myhill [8], in their modified version of Kleene's theory use a related monadic operator *. In W.2.A. = [o,, 30i] it is the finite-set-quantifier 3oi which corresponds to feedback. This is best shown by indicating how the primitive operators U,, and * on regular sets can be obtained in W.2.A. For this purpose to every Sgn-formula C(i) of W.2.A we define the formulas cY(i) and (i) as follows. First obtain a normal form of C(i), say C(i): (3 ).K[j(o)] (t) B[i(t), j(t), J(t')] 41

Then define cY(i): j). K[(x)] A (t) B(t) A B[v ( ()] (t)B, CY(i) (3j) K[j(x)] A (\/t)xB(t)A B[V I jy)j(y')] A (Vt) B j (t) (t) CU(i): (J_). K[j(x)] A (\t)x B[i(t), j(t), j(t')] Next for any Sgn-formulas C(i), D(i) of W.2.A. we define CUD, C D, C by [C UD](i): C(i) V D(i) [C D](i): (3y). (i)A (i) [C*](i): s). (xy)[s(x) s(y) (Vt)J S(t)Cy(i)] A(Vx)[S(x)(x s(t) _L(i)] It is easy to see that these operators on Sgn-formulas of W.2.A. define the operations U, on sets of finite n-strings. Note that ~ corresponds to individual quantification, while the feedback-operation * is reflected as a finite-set quantification. 9. AN UNSOLVED PROBLEM In essence our main result says that in [o, ', 30i] one can define only very simple recursive operators u = 4(i), namely, input to output operators of finite automata. In contrast [o, ', 2x, 0oi] contains definitions for all recursive operators u = *(i) (see Robinson [14]). Problem 1: Is the weak second-order theory [o, 2x+l, 2x+2, ~1oi] decidable? Which are the recursive operators definable in this theory? 42

These questions are of interest for automata theory, because via the enumeration of finite strings on two letters 11, 12 (see Section 7,1). The theory [o, 2x+l, 2x+2, 0oi] is equal to the theory [o, 11x, 1x, 0i] on the set N2 of finite strings. Let -Eooi denote quantification over all finite subsets of Nk which in addition are chains with respect to the terminal segment relation on Nk. Then by a straightforward extension of the methods used in this paper one obtains: Theorem 10: The "very weak" second-order theory [o, 11x,...,, 300i] is decidable. All regular sets, and only regular sets, on the alphabet 11,..., 1k can be defined by formulas C(x) of this theory. 43

BIBLIOGRAPHY 1. Behmann, Heinrich, "Beitrage zur Algebra der Logik, insbesondere zum Entscheidungsproblem," Mathematische Annalen, Vol. 86, pp. 163-229 (1922). 2. Burks, A. W., and Wright, J. B., "Theory of Logical Nets," Proc IRE, 41, 1357-1365 (1953). 3. Church, Alonzo, "Application of Recursive Arithmetic to the Problem of Circuit Synthesis," Proceedings of the Cornell Logic Conference, Cornell University, 1957. Also see "Application of Recursive Arithmetic in the Theory of Computing and Automata," notes for a summer course, The University of Michigan, 1959. 4. Copi, I. M., Elgot, C.C., and Wright, J. B., "Realization of Events by Logical Nets," Journal of the Association for Computing Machinery, 5, pp. 181-196 (1958). 5. Godel, Kurt, "On undecidable propositions of formal mathematical systems," Notes by S. C. Kleene and Barkley Rosser on lectures at the Institute for Advanced Study, 1934. Mimeographed, Princeton, N. J., 30 pp. 6. Kleene, S. C., "Representation of Events in Nerve Nets and Finite Automata," Automata Studies, Princeton University Press, 1956, pp. 3-41. 7. Medvedev, I. T., "On a Class of Events Representable in a Finite Automaton," MIT Lincoln Laboratory Group Report, 34-73, translated from the Russian by J. Schorr-Kon, June 30, 1958. 8. Myhill, John, "Finite Automata and Representation of Events," WADC Report TR 57-624, Fundamental Concepts in the Theory of Systems, October, 1957, pp. 112-137. 9. Moore, E. F., "Gedanken-Experiments on Sequential Machines," Automata Studies, Princeton, 1956, pp. 129-153. 10. Presberger, M., Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt." Comptes-rendus du I Congres des Mathematiciens des Pays Slavs, Warsaw, 1930, pp. 92-101, 395. 11. Putnam, H., "Decidability and Essential Undecidability," Journal of Smbolic Logic, Vol. 22 (1957) pp. 39-54. 12. Quine, W. V., Mathematical Logic. Harvard Univ. Press, Cambridge, 1947. 44

13. Rabin, M., and Scott, D., "Finite Automata and Their Decision Problems," IBM Journal, April, 1959, pp. 114-125. 14, Robinson, R. M., "Restricted Set-Theoretical Definitions in Arithmetic," Proc. American Mathematical Society, Vol. 9, (1958), pp. 238-242. 15. Skolem, Thoralf, "Untersuchungen uber die Axiome des Klassenkalkuls und uber Produktations- und Summationsprobleme, welche gewisse Klassen von Aussagen betreffen," Skrifter utgit av Videnskapsselskapet i Kristiania, I. Matematisk-naturvidenskabelig klasse 1919, No. 3, 37 PP. kS

UNIVERSITY OF MICHIGAN 3 9015 02652 8102