B. A. TRAKHTENBROT

SOME CONSTRUCTIONS IN THE LOGIC OF MONADIC PREDICATES

(Presented by Academician P. S. Novikov on 29 XII 1960)

1. In [1] it was shown that the calculus of monadic predicates is an adequate language for describing operators realized by finite automata. Similar results are also contained in [2], whose author was not acquainted with our article [1]. The connection found between finite automata and the indicated logical calculus proves useful in considering both purely logical problems and problems from the theory of finite automata. In the present note, a solution of one of Tarski’s problems is obtained in this way (see Sec. 3), and the possibility is traced of transferring certain facts from the theory of algorithms to finite automata.

2. Let (I) be the theory constructed, by means of the extended calculus of monadic predicates, from atomic formulas of the type (X(t)), (Y(\tau')), (Z(\sigma''),\ldots), where (t,\tau,\sigma,\ldots) are interpreted as natural numbers; (') as the immediate-successor function; and (X,Y,Z,\ldots) as predicate variables defined on the natural number series. In (I), the relations of equality and inequality ((<)) are definable for object variables, and consequently so are bounded object quantifiers. The same applies to the theory (I'), which differs from (I) only in that the predicate variables are interpreted as special predicates, i.e., such predicates (X) that ((Et)(\tau)\,\bar X(\tau)). A formula (\mathfrak{B}[x_1,\ldots,x_m]) of (I) (or (I')), containing no other free variables except the indicated predicate variables, defines the set
(\hat X_1\ldots \hat X_m \mathfrak{B}(x_1,\ldots,x_m)) of those tuples of predicates that satisfy it. In the same sense the formulas (\mathfrak{B}(t)), (\mathfrak{B}(t,\tau)), (\mathfrak{B}(t,\tau,\sigma),\ldots) define the corresponding sets of numbers (t), pairs of numbers (\langle t,\tau\rangle), triples of numbers (\langle t,\tau,\sigma\rangle), and, in particular, the operation (\sigma=f(t,\tau)), if ((t)(\tau)(E!\sigma)\mathfrak{B}(t,\tau,\sigma)).

3. Under the indicated interpretation of (I), every closed formula is either true or false, and therefore it is natural to ask:

Problem 1 (Tarski). Is the theory (I) decidable?

It is known that if (I) is extended by adding the operation of addition, then all recursive functions become definable, and the extended theory itself is undecidable. In connection with this there arises:

Problem 2 (Tarski). Is the operation of addition definable in (I)?

It is clear that a positive solution of either one of these problems entails a negative solution of the other. Büchi [2], and also Ehrenfeucht, established the decidability of the system (I'), which is weaker than (I), and Robinson [3] proved that addition is definable if the operation of doubling a number is added to (I'). Below (Sec. 4) a negative solution of Problem 2 for (I) is given. Although Problem 1 remains open thereby, it seems plausible that it has a positive solution.

4. Let (\mathfrak{B}(x,\ldots,x_m)) be an arbitrary formula of (I). There is an algorithm transforming the formula
(\mathfrak{B}(x_1,\ldots,x_m)\,\&\,(\tau)[\bar x_1(\tau)\,\&\,\ldots\,\&\,\bar x_m(\tau)])
into an equivalent formula of the form

[
\Phi\bigl(\Gamma_1(x_1,\ldots,x_m;t),\ldots,\Gamma_\nu(x_1,\ldots,x_m;t),\Omega_1,\ldots,\Omega_\mu\bigr),
]

where (\Phi) is a function of the algebra of logic; (\Gamma_1,\ldots,\Gamma_\nu) are (t)-formulas with controlled quantifiers (see [1]); (\Omega_1,\ldots,\Omega_\mu) are closed formulas of (I).

Since, after computing the truth values of the formulas (\Omega_1,\ldots,\Omega_\mu), the formula (\Phi) itself becomes a (t)-formula with controlled quantifiers, it follows that:

Theorem 1. For every formula (\mathfrak B(x_1,\ldots,x_m)) of (\mathcal I) there exists a finite automaton having the following property: to the input word
[
\langle x_1(1),\ldots,x_m(1)\rangle
\langle x_1(2),\ldots,x_m(2)\rangle
\cdots
\langle x_1(t),\ldots,x_m(t)\rangle
]
there corresponds the output (W(t)=1) if and only if the set of predicates (x_1,\ldots,x_m), extended by being set equal to (0) for all (\tau>t), belongs to
[
\tilde x_1\ldots \tilde x_m\,\mathfrak B(x_1,\ldots,x_m).
]

In this sense, membership of special predicates in the set
[
\tilde x_1\ldots \tilde x_m\,\mathfrak B(x_1,\ldots,x_m)
]
is recognizable “by an automaton.”

Corollary. Every set (N) of natural numbers definable in (\mathcal I) is periodic*.

Thus, in (\mathcal I) only a very narrow class of recursive sets is definable. From this it follows immediately (see Sec. 3):

Theorem 2. Addition is not definable in (\mathcal I).

Remark. The proof of Theorem 1 is such that, in order to obtain the canonical equations of the corresponding automaton, one must first establish the truth or falsity of the closed formulas (\Omega_1,\ldots,\Omega_\mu). Therefore a positive solution of Problem 1 would make it possible to extract from this proof an algorithm that supplies the canonical equations for any given formula (\mathfrak B(x_1,\ldots,x_m)).

1. The fact that, in the language describing finite-automaton operators, predicate quantifiers are admissible sometimes entails a violation of analogies with well-known theorems of the theory of recursive functions, where quantifiers play a different role. In other cases, although the analogy holds, establishing it is almost obvious. Examples illustrating these points are given below.

In the theory of finite automata, an analogue of a recursive set may be considered to be any set of words (\mathfrak M) for which there exists a finite automaton that produces (1) when a word from (\mathfrak M) is presented and (0) when any other input word is presented; we shall call such a set (a)-decidable. If, however, there exists a finite automaton that maps the set of all input words onto (\mathfrak M), then (\mathfrak M) (we shall call it an (a)-enumerable set) is analogous to a recursively enumerable set.

Obviously, an (a)-enumerable set (\mathfrak M) has the following properties:

I. If a word (M\in\mathfrak M), then every initial segment of it belongs to (\mathfrak M).

II. If (M\in\mathfrak M), then there exists in (\mathfrak M) a word whose initial segment is (M).

Let the input alphabet of a finite automaton be the direct product of two alphabets; then each input word may be regarded as a pair of words (\langle M,N\rangle) in the corresponding alphabets. If the set (\mathfrak M), (a)-decidable by this automaton, is such that
[
(M)(E!N){\langle M,N\rangle\in\mathfrak M},
]
then the finite automaton thereby defines implicitly an operator that transforms words (M) into words (N).

For the notions introduced, the following assertions are valid:

A. Every (a)-enumerable set is (a)-decidable.

B. In order that an (a)-decidable set be (a)-enumerable, it is necessary and sufficient that it have properties I–II.

C. Every operator without anticipation ((^4)), implicitly specified in a finite automaton, is realized (explicitly) in some finite automaton.

Received
23 XI 1960

References

1. B. A. Trakhtenbrot, DAN, 118, No. 4 (1958).
2. J. R. Büchi, Zs. f. math. Logik u. Grundlagen d. Math., 6, No. 1, 66 (1960).
3. R. M. Robinson, Proc. Am. Math. Soc., 9, 238 (1958).
4. B. A. Trakhtenbrot, DAN, 112, No. 6 (1957).

* That is, there exist (p,q) such that
[
(x)\bigl(x+p\in N \equiv x+p+q\in N\bigr).
]