Hilbert’s tenth problem for term algebras with a substitution operator

Abstract

The analogue of Hilbert’s 10th Problem for a first-order structure $A$ with signature $L$ asks whether there exists an algorithm that given an $L$ -sentence of the form $\exists \vec{x} [s = t]$ decides whether $\exists \vec{x} [s = t]$ is true in $A$ . In this paper, we consider term algebras over a finite signature with at least one constant symbol and one function symbol of arity at least two. We investigate the structure we obtain by extending the term algebra with a substitution operator. We prove undecidability of the analogue of Hilbert’s 10th problem without relying on the solution to the original Hilbert’s 10th Problem.

Keywords

Hilbert’s 10th problem term algebras substitution operator

1. Introduction

Hilbert’s 10th Problem asks whether there exists an algorithm that given a polynomial $f \in Z [x_{1}, x_{2}, \dots, x_{n}]$ decides whether f has a zero in $Z^{n}$ . By Lagrange’s four-square theorem, this problem is Turing equivalent to solvability of equations over the natural numbers: given $f, g \in N [x_{1}, x_{2}, \dots, x_{n}]$ , decide whether there exist natural numbers $a_{1}, \dots, a_{n}$ such that $f (a_{1}, \dots, a_{n}) = g (a_{1}, \dots, a_{n})$ . In 1970, Yuri Matiyasevich proved that Hilbert’s 10th Problem is undecidable by showing that the exponential function is existentially definable in terms of addition and multiplication (see for example Davis [3]). After this, a standard technique for showing that a structure has undecidable existential theory has been to show that it existentially interprets the first-order structure of arithmetic $(N, 0, 1, +, \times)$ (see Sections 5.3 and 5.4a of Hodges [6] for more details). Such a proof does not in general give a good picture of the existentially definable subsets of the universe. Matiyasevich’s result builds on the work of Davis, Putnam & Robinson [4] and shows that a set of natural numbers is computably enumerable if and only if it is diophantine, that is, it is definable in $(N, 0, 1, +, \times)$ by a formula of the form $\exists \vec{x} [f (t, \vec{x}) = g (t, \vec{x})]$ .

The analogue of Hilbert’s 10th Problem for a first-order structure $A$ with signature $L$ asks whether there exists an algorithm with input and output as follows:

input:	an $L$ -sentence of the form $\exists \vec{x} [s = t]$
output:	YES if $\exists \vec{x} [s = t]$ is true in $A$ , and NO otherwise.

In this paper, we investigate existential definability and the analogue of Hilbert’s 10th Problem for term algebras extended with an operator that can be viewed as a generalization of the operation of string concatenation. Given a finite alphabet

A = {a_{1}, a_{2}, \dots, a_{n}}

, we identify the set

A^{*}

of all finite strings over A with the set

H (L_{A})

of all variable-free terms in the language

L_{A} = {ε, a_{1}, a_{2}, \dots, a_{n}}

where ε is a constant symbol and each

a_{i}

is a unary function symbol. We identify the empty string with the term ε and a finite string

a_{k_{1}} a_{k_{2}} \dots a_{k_{m}}

with the term

a_{k_{1}} a_{k_{2}} \dots a_{k_{m}} ε

written in prefix notation. Concatenation is a substitution operation: to concatenate s and t is to replace the occurrence of ε in s with t. This leads naturally to a general substitution operator where we replace an arbitrary term instead of just ε. This ternary function

\cdot [\cdot \mapsto \cdot] : H {(L_{A})}^{3} \to H (L_{A})

is defined by recursion:

t [r \mapsto s] = w

where: (1)

w = s

r = t

, (2)

w = t

t \neq r

and

t = ε

, (3)

w = a (t^{'} [r \mapsto s])

t \neq r

and t is the term

a (t^{'})

. This function is easily seen to be expressible in terms of concatenation:

t [r \mapsto s] = w

if and only if: (i)

r = t

and

w = s

or (ii) there exists v such that t is the concatenate of v and r, and w is the concatenate of v and s. Definability of the substitution operator in terms of concatenation persists even when we extend the language with an arbitrary finite number of constant symbols. Makanin [10] has shown that the existential theory of finitely generated free monoids is decidable.

Just as concatenation becomes more expressive when we have more than one letter, the substitution operator is more expressive over a signature with function symbols of higher arity together with constant symbol. With $H (L)$ denoting the set of all variable-free $L$ -terms, we define the substitution operator by recursion $\begin{matrix} z [x \mapsto y] = \{\begin{array}{ll} y & if z = x \\ z & if z \neq x and z is a constant symbol \\ f (u_{1} [x \mapsto y], \dots, u_{n} [x \mapsto y]) & if z \neq x and z = f (u_{1}, \dots, u_{n}) . \end{array} \end{matrix}$ Let $T (L)$ denote the structure we obtain by extending the term algebra defined by $L$ with the substitution operator: the universe is $H (L)$ and each variable-free $L$ -term is interpreted as itself. We prove undecidability of the analogue of Hilbert’s 10th Problem by encoding computations by Turing machines with existential formulas. This result was first published in the conference paper Murwanashyaka [11]. In this paper, we give a more general construction that tries to shed some light on the existentially definable subsets of the universe. We restrict ourselves to the signature consisting of just one constant symbol ⊥ and one binary function symbol $⟨ \cdot, \cdot ⟩$ , the methods extend easily to the general case. We write H instead of $H (L)$ and interchangeably refer to elements of H as finite (full) binary trees. We denote the signature ${⊥, ⟨ \cdot, \cdot ⟩, \cdot [\cdot \mapsto \cdot]}$ by $L_{BT}$ .

Although our proof of undecidability of the existential theory of $H (L_{BT})$ does not use the solution to Hilbert’s 10th Problem, it is not clear to us whether this result can be used to give a new proof of unsolvability of Hilbert’s 10th Problem.

Open Problem 1.
Construct a Turing reduction of the existential theory of $T (L_{BT})$ to the existential theory of $(N, 0, 1, +, \times)$ which does not rely on the solution to Hilbert’s 10th Problem.

2. Bounded quantifiers

Before proving undecidability of solvability of equations over $T (L_{BT})$ , we investigate the amount of bounded quantification needed to get undecidability. Recall that $T (L_{BT})$ denotes the structure $(H, ⊥, ⟨ \cdot, \cdot ⟩, \cdot [\cdot \mapsto \cdot])$ where H is the set of all variable-free terms in the language ${⊥, ⟨ \cdot, \cdot ⟩}$ (equivalently, finite full binary trees). Although $L_{BT}$ does not contain a relation symbol, the subtree relation, denoted ⊑, is easily seen to have a quantifier-free definition in terms of the substitution operator. We introduce the bounded quantifiers $\exists x ⊑ t [ϕ]$ , $\forall x ⊑ t [ϕ]$ as shorthand notation for $\exists x [x ⊑ t \land ϕ]$ and $\forall x [x ⊑ t \to ϕ]$ , respectively, where $x ⊑ t$ and $x ⋢ t$ are shorthand for $t [x \mapsto ⟨ x, x ⟩] \neq t$ and $t [x \mapsto ⟨ x, x ⟩] = t$ , respectively. We define Σ-formulas inductively: ϕ and $\neg ϕ$ are Σ-formulas if ϕ is an atomic formula, $(ϕ \lor ψ)$ , $(ϕ \land ψ)$ , $\exists x ⊑ t [ϕ]$ , $\forall x ⊑ t [ϕ]$ , $\exists x [ϕ]$ are Σ-formulas if ϕ and ψ are Σ-formulas and x is a variable that does not occur in the term t. An existential formula is a Σ-formula that does not contain bounded quantifiers. A sentence is a formula without free variables.

We investigate also what happens when we take ⊑ as primitive. Let $L_{T^{-}} = {⊑}$ and $L_{T} = {⊥, ⟨ \cdot, \cdot ⟩, ⊑}$ . We interpret ⊑ as the subtree relation: s is a subtree of t iff $s = t$ or $t = ⟨ t_{1}, t_{2} ⟩$ and s is a subtree of $t_{1}$ or $t_{2}$ . We consider the two structures $T (L_{T^{-}}) = (H, ⊑)$ and $T (L_{T}) = (H, ⊥, ⟨ \cdot, \cdot ⟩, ⊑)$ .

In Venkataraman [14], it is shown that the set of existential $L_{T}$ -sentences true in $T (L_{T})$ is computable and that the set of true Σ-sentences is not computable. As a step towards determining the boundary between what we can and cannot effectively decide, we classify Σ-formulas according to the number and the type of quantifiers they contain: A $Σ_{n, m, k}$ -formula is a Σ-formula that contains n unbounded existential quantifiers, m bounded existential quantifiers and k bounded universal quantifiers. The fragment $Σ_{n, m, k}^{A}$ is the set of all $Σ_{n, m, k}$ -sentences that are true in $A$ . The existential theory (existential fragment) of $A$ is the set of all existential sentences that are true in $A$ . We let ${Th}^{\exists} (A)$ denote the existential theory of $A$ . The Σ-theory of $A$ , denoted ${Th}^{Σ} (A)$ , is the set of all Σ-sentences in the language of $A$ that are true in $A$ . That is, ${Th}^{Σ} (A) = ⋃_{n, m, k ⩾ 0} Σ_{n, m, k}^{A}$ . We let ${Th}^{H 10} (A)$ denote the set of all sentences of the form $\exists \vec{x} [s = t]$ that are true in $A$ .

In this section, we show that the fragment $Σ_{1, 0, 2}^{T (L_{T})}$ is undecidable. That is, we show that there cannot exist an algorithm that takes as input an $L_{T}$ -sentence ϕ of the form $\exists x \forall y ⊑ x \forall z ⊑ x [ϕ_{0}]$ , where $ϕ_{0}$ is quantifier-free, and decides whether ϕ is true in $T (L_{T})$ . Next, we prove undecidability of the Σ-fragment of $T (L_{T^{-}})$ . Finally, we show that the fragment $Σ_{1, 0, 1}^{T (L_{BT})}$ is undecidable.

Open Problem 2.
Is the fragment $Σ_{1, 0, 1}^{T (L_{T})}$ undecidable?

2.1. Finite sets of finite binary trees

The proofs we give depend on our ability to code finite sets of finite full binary trees of a certain form as finite full binary trees.

Definition 3.
Let $α \in H$ . Then, $x \in_{α} y$ is shorthand for $⟨ x, α ⟩ ⊑ y \land α ⋢ x$ .

We read $x \in_{α} y$ as: x belongs to a finite set encoded by y using α as a marker. See Fig. 1 for examples. In the proofs, we translate the membership relation as follows $\begin{matrix} x \in y \equiv x \in_{α} y where α \equiv ⟨ ⊥, ⟨ ⊥, ⊥ ⟩ ⟩ . \end{matrix}$ Observe that if $x \in y$ , then $x ⊑ y$ . It is important to notice that our definition of the membership relation is quantifier-free. In particular, subformulas of the form $x \in y$ will not hide any quantifier complexity. This is also true of the structure $T (L_{BT})$ since we chose to define the subtree relation as follows: $x ⊑ y \equiv y [x \mapsto ⟨ x, x ⟩] \neq y$ .

Figure 1.
Two encodings of the finite set ${w_{0}, w_{1}, w_{2}}$ using α as a marker. We assume α is not a subtree of $w_{k}$ for all $k \in {0, 1, 2}$ .
2.2. Notation

We will encounter many cases where we need to associate a finite sequence of binary trees on the meta level with a term in the formal language. To improve readability, we introduce the following notation (see Fig. 2 for examples)

$⟨ x ⟩ \equiv x$ and $⟨ x_{1}, \dots, x_{n}, x_{n + 1} ⟩ \equiv ⟨ ⟨ x_{1}, \dots, x_{n} ⟩, x_{n + 1} ⟩$ for $n > 0$

$t^{1} \equiv t$ and $t^{n + 1} \equiv ⟨ t^{n}, t ⟩$ for $n > 0$

${⟨ x_{1}, \dots, x_{n} ⟩}^{1} \equiv ⟨ x_{1}, \dots, x_{n} ⟩$ and ${⟨ x_{1}, \dots, x_{n} ⟩}^{k + 1} \equiv ⟨ {⟨ x_{1}, \dots, x_{n} ⟩}^{k}, x_{1}, \dots, x_{n} ⟩$ for $k > 0$

${⟨ x_{1}, \dots, x_{n} ⟩}^{⌢} ⟨ y_{1}, \dots, y_{m} ⟩ \equiv ⟨ x_{1}, \dots, x_{n}, y_{1}, \dots, y_{m} ⟩$ .

For example, occurrences of $x^{⌢} y$ , ${x^{2}}^{⌢} y$ and $x^{⌢} y^{2}$ in formal formulas should be interpreted as shorthand notation for $⟨ x, y ⟩$ , $⟨ x, x, y ⟩$ and $⟨ x, y, y ⟩$ , respectively.

Figure 2.

Visualization of $⟨ x_{1}, x_{2}, x_{3} ⟩$ , ${⟨ x_{1}, x_{2} ⟩}^{2}$ , $t^{3}$ and ${⟨ s, t ⟩}^{⌢} ⟨ r, w ⟩$ , respectively, as finite full binary trees.

2.3. Post’s correspondence problem

We show that $Σ_{1, 0, 2}^{T (L_{T})}$ is undecidable by giving a many-to-one reduction of Post‘s correspondence problem (see Post [12]). The input to Post’s correspondence problem is a finite set of dominos, and the solution is a list of these dominos (repetition allowed) so that the string we get by reading off the symbols on the top is the same as the string we get by reading off the symbols on the bottom.

Let ${0, 1}^{+}$ denote the set of all nonempty binary strings.

Definition 4.
The Post Correspondence Problem (PCP) is given by
Instance: a list of pairs (dominos) $[\frac{a_{1}}{b_{1}}]$ , $[\frac{a_{2}}{b_{2}}], \dots, [\frac{a_{n}}{b_{n}}]$ where $a_{i}, b_{i} \in {0, 1}^{+}$

Solution: a finite nonempty sequence $i_{1}, \dots, i_{m}$ of indexes such that $a_{i_{1}} a_{i_{2}} \dots a_{i_{m}} = b_{i_{1}} b_{i_{2}} \dots b_{i_{m}}$ .

Venkataraman [14] proved that the fragment ${Th}^{Σ} (T (L_{T}))$ is undecidable by giving a many-to-one reduction of PCP. An inspection of the proof shows that what is proved is actually that the fragment $Σ_{1, 2, 7}^{T (L_{T})}$ is undecidable. Venkataraman introduces a constant symbol c, a unary operator $d_{i} (\cdot)$ for each letter $d_{i}$ of the alphabet and a ternary function f. The string $d_{i_{1}} \dots d_{i_{m}}$ is represented as the term $d_{i_{1}} (\dots (d_{i_{m}} (c)) \dots)$ . Venkataraman then tries to capture that an instance of PCP has a solution if and only if there exists a witnessing term t of the form $\begin{matrix} t = f (r_{1}, s_{1}, f (r_{2}, s_{2}, f (\dots f (r_{m + 1}, s_{m + 1}, c) \dots))) \end{matrix}$ where $r_{j} = a_{i_{j}} \dots a_{i_{m}}$ , $s_{j} = b_{i_{j}} \dots b_{i_{m}}$ and $r_{m + 1} = s_{m + 1}$ is the empty string. It becomes immediately clear that at least three bounded universal quantifiers are needed since we need to talk about arbitrary subterms of t of the from $f (x, y, z)$ . Two bounded existential quantifier are necessary to say that t has the form $t = f (u, u, v)$ . We get a stronger result by encoding PCP differently.
Theorem 5.
The fragment $Σ_{1, 0, 2}^{T (L_{T})}$ is undecidable.
Proof.
We start by translating concatenation of finite strings. Let $0 \equiv ⊥^{3}$ and $1 \equiv ⊥^{4}$ . Consider a nonempty binary string $w = w_{1} \dots w_{k}$ where $w_{i} \in {0, 1}$ for each $1 ⩽ i ⩽ k$ . We represent w in the formal language as $⟨ w_{1}, \dots, w_{k} ⟩$ . We represent $x w$ as $x^{⌢} w$ . Recall that $x^{⌢} ⟨ w_{1}, \dots, w_{k} ⟩ \equiv ⟨ x, w_{1}, \dots, w_{k} ⟩$ . For example, if $w = w_{1} w_{2} w_{3}$ , then 0, 1, w and $x w$ are drawn, respectively, in Fig. 3.

Figure 3.
Translation of the binary strings 0, 1, $w = w_{1} w_{2} w_{3}$ and $x w$ in the proof of Theorem 5, $w_{j} \in {0, 1}$ for each $j \in {1, 2, 3}$ .

Before proceeding, we need to choose a suitable parameter α for our definition of set membership (see Definition 3). Since we want to talk about finite sets of binary strings, a representation of a binary string cannot have α as a subtree. We let $\begin{matrix} x \in y \equiv x \in_{α} y where α \equiv ⟨ ⊥, ⊥^{2} ⟩ . \end{matrix}$ We remind the reader that if $x \in y$ , then $x ⊑ y$ . This is important to see that the bounded universal quantifiers in the formula ϕ below cover the search space we are interested in.

Given an instance $[\frac{a_{1}}{b_{1}}]$ , $[\frac{a_{2}}{b_{2}}], \dots, [\frac{a_{n}}{b_{n}}]$ of PCP, we need to compute a $Σ_{1, 0, 2}$ -sentence ϕ that is true in $T (L_{T})$ if and only if there exists a finite nonempty sequence $i_{1}, \dots, i_{m}$ of indeces such that $a_{i_{1}} a_{i_{2}} \dots a_{i_{m}} = b_{i_{1}} b_{i_{2}} \dots b_{i_{m}}$ . The existence of $i_{1}, \dots, i_{m}$ is equivalent to the existence of a finite set T that satisfies the following
there exists $i \in {1, \dots, n}$ such that $⟨ a_{i}, b_{i} ⟩ \in T$

if $⟨ L, R ⟩ \in T$ and $L \neq R$ , then $⟨ L^{⌢} a_{i}, R^{⌢} b_{i} ⟩ \in T$ for some $i \in {1, \dots, n}$ .

Given a solution $i_{1}, \dots, i_{m}$ , the witnessing set T can be any finite binary tree that encodes the set $\begin{matrix} {⟨ a_{i_{1}}^{⌢} \dots^{⌢} a_{i_{j}}, b_{i_{1}}^{⌢} \dots^{⌢} b_{i_{j}} ⟩ : 1 ⩽ j ⩽ m} . \end{matrix}$

We let ϕ be the following sentence $\begin{matrix} \exists T \forall L, R ⊑ T [⋁_{i = 1}^{n} ⟨ a_{i}, b_{i} ⟩ \in T \land ((⟨ L, R ⟩ \in T \land L \neq R) \to ⋁_{i = 1}^{n} ⟨ L^{⌢} a_{i}, R^{⌢} b_{i} ⟩ \in T)] . \end{matrix}$ □
2.4. Post’s correspondence problem II

Recall that $L_{T^{-}} = {⊑}$ and $T (L_{T^{-}})$ denotes the restriction of $T (L_{T})$ to $L_{T^{-}}$ . In this section, we show that the Σ-theory of $T (L_{T^{-}})$ is undecidable. That is, we show that there cannot exist an algorithm that takes as input an $L_{T^{-}}$ Σ-sentence ϕ and decides whether ϕ is true in $T (L_{T^{-}})$ . The proof we give is a modification of the proof of Theorem 5. The basic idea is the same but we need to work with multivalued functions since our language does not have function symbols. A multivalued function from $H^{n}$ to H is just a relation $R \subseteq H^{n + 1}$ such that for all $x_{1}, \dots, x_{n} \in H$ there exists $y \in H$ such that $R (x_{1}, \dots, x_{n}, y)$ holds, equivalently, it is a function from $H^{n}$ to $P (H)$ . Recall that H denotes the set of all finite full binary trees.

In the proof of Theorem 5, we showed that the instance $[\frac{a_{1}}{b_{1}}]$ , $[\frac{a_{2}}{b_{2}}], \dots, [\frac{a_{n}}{b_{n}}]$ of PCP has a solution if and only if the sentence $\begin{matrix} ϕ \equiv \exists T \forall L, R ⊑ T [⋁_{i = 1}^{n} ⟨ a_{i}, b_{i} ⟩ \in T \land ((⟨ L, R ⟩ \in T \land L \neq R) \to ⋁_{i = 1}^{n} ⟨ L^{⌢} a_{i}, R^{⌢} b_{i} ⟩ \in T)] \end{matrix}$ is true in $T (L_{T})$ . The idea is to find a $L_{T^{-}}$ -sentence ψ that is true in $T (L_{T^{-}})$ if and only if ϕ is true in $T (L_{T})$ . We use the following ingredients to construct ψ

we give a definition of $s \in_{α} T$ over $T (L_{T^{-}})$

we replace $⟨ x, y ⟩$ with a multivalued pairing function ${Pair}_{β, γ} (x, y, z)$ that takes β and γ as parameters

we replace $L^{⌢} a_{i}$ with a multivalued function ${Conc}_{a_{i}} (L, y)$

we replace $R^{⌢} b_{i}$ with a multivalued function ${Conc}_{b_{i}} (R, y)$ .

The multivalued functions

{Conc}_{a_{i}} (x, y)

{Conc}_{b_{i}} (x, y)

will be defined from the more elementary multivalued functions

{Conc}_{0} (x, y)

{Conc}_{1} (x, y)

by composing these functions in the obvious way.

The sentence ϕ is true in $T (L_{T})$ if and only if there exists a finite nonempty sequence $i_{1}, \dots, i_{m}$ of indexes such that $a_{i_{1}} a_{i_{2}} \dots a_{i_{m}} = b_{i_{1}} b_{i_{2}} \dots b_{i_{m}}$ . The sequence $i_{1}, \dots, i_{m}$ exists if and only if (this is what ψ captures)

there exist a sequence of finite binary trees $A_{1}, B_{1}, \dots, A_{m}, B_{m}$ such that

${Conc}_{a_{i_{1}}} (δ, A_{1})$ and ${Conc}_{b_{i_{1}}} (δ, B_{1})$ for some parameter δ

${Conc}_{a_{i_{k + 1}}} (A_{k}, A_{k + 1})$ and ${Conc}_{b_{i_{k + 1}}} (B_{k}, B_{k + 1})$

$A_{m} = B_{m}$ .

We let $x ⊏ y \equiv x ⊑ y \land x \neq y$ .

Theorem 6.
The fragment ${Th}^{Σ} (T (L_{T^{-}}))$ is undecidable.
Proof.
Given an instance $[\frac{a_{1}}{b_{1}}]$ , $[\frac{a_{2}}{b_{2}}], \dots, [\frac{a_{n}}{b_{n}}]$ of PCP, we compute an $L_{T^{-}}$ -sentence ψ that is true in $T (L_{T^{-}})$ if and only if there exists a finite nonempty sequence $i_{1}, \dots, i_{m}$ of indices such that $a_{i_{1}} a_{i_{2}} \dots a_{i_{m}} = b_{i_{1}} b_{i_{2}} \dots b_{i_{m}}$ . Our starting point is to translate the two string operations $x \mapsto x 0$ , $x \mapsto x 1$ as multivalued functions. Our translations need to ensure that we can tell the two functions apart.

We capture the string operation $x \mapsto x 0$ as a multivalued function as follows $\begin{array}{rcl} Zero (x, y) \equiv \exists z, w ⊑ y & [x ⊑ z \land x ⊑ w \land z ⋢ w \land w ⋢ z \land \\ \forall r ⊑ y [r = y \lor r = z \lor r = w \lor r ⊑ x]] . \end{array}$

Figure 4 shows the subtrees of y when $Zero (x, y)$ holds. Observe that for each x with at least two distinct subtrees, we can find y such that $Zero (x, y)$ holds. For example, if u and v are distinct subtrees of x, then we can let y be $⟨ ⟨ x, u ⟩, ⟨ x, v ⟩ ⟩$ .

Figure 4.
Translation of the string operation $x \mapsto x 0$ in the proof of Theorem 6. $X \to Y$ means $X ⊏ Y$ . If there is no directed path connecting X and Y, then X and Y are incomparable with respect to ⊑. If $Y ⊑ y \land x ⊑ Y$ , then Y appears in the diagram.

We capture the string operation $x \mapsto x 1$ as a multivalued function as follows $\begin{array}{rcl} One (x, y) \equiv \exists s, t ⊑ y & [Zero (x, s) \land Zero (x, t) \land s ⋢ t \land t ⋢ s \land \\ \forall r ⊑ y [r = y \lor r ⊑ s \lor r ⊑ t]] . \end{array}$

Figure 5 shows the subtrees of y when $One (x, y)$ holds. Observe that for each x with at least three distinct subtrees, we can find y such that $One (x, y)$ holds. For example, if u, v, w are three distinct subtrees of x, then we can let y be $⟨ ⟨ ⟨ x, u ⟩, ⟨ x, v ⟩ ⟩, ⟨ ⟨ x, u ⟩, ⟨ x, w ⟩ ⟩ ⟩$ .

Figure 5.
Translation of the string operation $x \mapsto x 1$ in the proof of Theorem 6. $X \to Y$ means $X ⊏ Y$ . If there is no directed path connecting X and Y, then X and Y are incomparable with respect to ⊑. If $Y ⊑ y \land x ⊑ Y$ , then Y appears in the diagram.

For each binary string w, we capture the string operation $x \mapsto x w$ as multivalued function by recursion as follows: Let ${Conc}_{0} (x, y) \equiv Zero (x, y)$ and ${Conc}_{1} (x, y) \equiv One (x, y)$ . Let $w = w_{0} w_{1}$ where $w_{1} \in {0, 1}$ and $w_{0} \in {0, 1}^{+}$ . Let $\begin{matrix} {Conc}_{w} (x, y) \equiv \{\begin{array}{ll} \exists z ⊑ y [{Conc}_{w_{0}} (x, z) \land Zero (z, y)] & if w_{1} = 0 \\ \exists z ⊑ y [{Conc}_{w_{0}} (x, z) \land One (z, y)] & if w_{1} = 1 . \end{array} \end{matrix}$

What remains is to define a multivalued pairing function and a notion of set membership. We define the membership relation as follows $\begin{matrix} x \in_{α} y \equiv x ⋢ α \land α ⋢ x \land \exists z ⊑ y \forall u ⊑ z [u = z \lor u ⊑ x \lor u ⊑ α] . \end{matrix}$ Observe that if $x \in_{α} y$ , then the variable z in the formula is such that $z = ⟨ x, α ⟩$ or $z = ⟨ α, x ⟩$ since x and α are incomparable with respect to the subtree relation.

We define a multivalued pairing function on finite binary trees as follows (Fig. 6 shows the subtrees of z when ${Pair}_{β, γ} (x, y, z)$ holds) $\begin{array}{c} {Pair}_{β, γ} (x, y, z) \equiv β ⋢ γ \land γ ⋢ β \land \exists s, t, s_{0}, t_{0} ⊑ z [Zero (x, s) \land Zero (y, t) \land β ⋢ s \land s ⋢ β \land \\ \forall r ⊑ s_{0} [r = s_{0} \lor r ⊑ β \lor r ⊑ s] \land γ ⋢ t \land t ⋢ γ \land \forall r ⊑ t_{0} [r = t_{0} \lor r ⊑ γ \lor r ⊑ t] \land \\ \forall r ⊑ z [r = z \lor r ⊑ s_{0} \lor r ⊑ t_{0}]] . \end{array}$

Figure 6.
The multivalued pairing function ${Pair}_{β, γ} (x, y, z)$ in the proof of Theorem 6. The trees β, γ are parameters that allow us to recognize that an element represents a pair. $X \to Y$ means $X ⊏ Y$ . If $Y ⊑ z$ and $x ⊑ Y \lor y ⊑ Y \lor β ⊑ Y \lor γ ⊑ Y$ , then Y appears in the diagram.

We let ψ be the following sentence $\begin{array}{c} ψ \equiv \exists α β γ δ \exists T \forall L, R, S ⊑ T \\ [⋁_{i = 1}^{n} \exists x, y, z ⊑ T [{Conc}_{a_{i}} (δ, x) \land {Conc}_{b_{i}} (δ, y) \land {Pair}_{β, γ} (x, y, z) \land z \in_{α} T] \\ \land (({Pair}_{β, γ} (L, R, S) \land S \in_{α} T \land L \neq R) \\ \to ⋁_{i = 1}^{n} \exists u, v, w ⊑ T [{Conc}_{a_{i}} (L, u) \land {Conc}_{b_{i}} (R, v) \land {Pair}_{β, γ} (u, v, w) \land w \in_{α} T])] . \end{array}$ □
2.5. The modulo problem

In this section, we show that the fragment $Σ_{1, 0, 1}^{T (L_{BT})}$ is undecidable. We cannot prove this result by giving a many-to-one reduction of PCP since expressing that an instance of PCP has a solution necessitates the use of two bounded universal quantifiers. Instead, we give a many-to-one reduction of the Modulo Problem, which is an arithmetical problem. The Modulo Problem is introduced in Kristiansen & Murwanashyaka [8] where it is used to characterize undecidable fragments of finitely generated free semigrooups extended with natural binary relations on strings such as the prefix relation and the substring relation. Undecidability of the Modulo Problem follows from undecidability of a generalized version of the Collatz conjecture studied first by Conway [2] and then by Kurtz & Simon [9]. The main difference between the Modulo Problem and PCP is that the Modulo problem is about sequences of 1-tuples while PCP is about sequences of 2-tuples.

Definition 7.
Let $f^{N}$ denote the Nth iteration of f: $\begin{matrix} f^{0} (x) = x and f^{N + 1} (x) = f (f^{N} (x)) . \end{matrix}$ The Modulo Problem is given by
Instance: a list of pairs $(A_{0}, B_{0})$ , $(A_{1}, B_{1}), \dots, (A_{M - 1}, B_{M - 1})$ where $M > 1$ and $A_{i}, B_{i} \in N$ for $i = 0, 1, \dots, M - 1$ .

Solution: a natural number N such that $f^{N} (3) = 2$ where $\begin{matrix} f (x) = A_{j} z + B_{j} \end{matrix}$ if there exists $j \in {0, 1, \dots, M - 1}$ such that $x = M z + j$ .

We need to show that given an instance of the Modulo Problem, we can compute a $Σ_{1, 0, 1}$ -sentence that is true in $T (L_{BT})$ if and only if the instance has a solution. As we can see from the definition, to encode the Modulo Problem, we need to encode linear polynomials in one variable.
Theorem 8.
The fragment $Σ_{1, 0, 1}^{T (L_{BT})}$ is undecidable.
Proof.
We continue to work with the following definition of set membership $\begin{matrix} x \in y \equiv x \in_{α} y where α \equiv ⟨ ⊥, ⊥^{2} ⟩ . \end{matrix}$

Recall that $t [r \mapsto s]$ denotes the term we obtain by replacing each occurrence of r in t with s. We encode natural numbers as follows: $n \equiv ⊥^{n + 2}$ . For example, the natural numbers 0, 1, 2, 3 are drawn in Fig. 7.

Figure 7.
Translation of the natural numbers 0, 1, 2, 3 in the proof of Theorem 8.

The next step is to associate linear polynomials in one variable with $L_{BT}$ -terms. Let $L (z) \equiv z [0 \mapsto z]$ . If z represents the natural number q, then $L (z)$ represents the natural number $2 q$ since 0 has exactly one occurrence in z (see Fig. 7). Recall that $L^{0} (z) = z$ and $L^{k + 1} (z) = L (L^{k} (z))$ . Hence, if $n > 0$ , then $L^{n - 1} (z)$ represents the natural number $n q$ . If $n > 0$ , then the term $m [0 \mapsto L^{n - 1} (z)]$ represents the natural number $n q + m$ . We complete our translation of linear polynomials in one variable as follows: For any formula $ϕ (x)$ where x is a free variable in ϕ $\begin{matrix} ϕ (n z + m) \equiv \{\begin{array}{ll} ϕ (m) & if n = 0 \\ ϕ (m [0 \mapsto L^{n - 1} (z)]) & if n > 0 . \end{array} \end{matrix}$

Given an instance $(A_{0}, B_{0})$ , $(A_{1}, B_{1}), \dots, (A_{M - 1}, B_{M - 1})$ , we need to compute a $Σ_{1, 0, 1}$ -sentence ψ that is true in $T (L_{BT})$ if and only if the instance has a solution. The sentence ψ needs to say that there exists a finite set T such that
$3 \in T$ and $2 \in T$

if $2 \neq M z + j \in T$ and $0 ⩽ j < M$ , then $A_{j} z + B_{j} \in T$ .

With this in mind, we let ψ be the following sentence $\begin{matrix} \exists T \forall z ⊑ T [3 \in T \land ⋀_{j = 0}^{M - 1} ((M z + j \in T \land M z + j \neq 2) \to A_{j} z + B_{j} \in T)] . \end{matrix}$ □

The preceding result says that we have undecidability with only one existential quantifier and one bounded universal quantifier. Clearly, it is decidable whether a Σ-sentence with no occurrence of unbounded existential quantifiers is true. Hence, the next question is whether we can have undecidability without bounded universal quantifiers. In the following section, we show that existential theory of $T (L_{BT})$ is undecidable.
3. Existential interpretation of arithmetic

In this section, we show that the existential theory of $T (L_{BT})$ is undecidable by constructing an existential interpretation of $(N, 0, 1, +, \times)$ in $T (L_{BT})$ . In Section 3.4, we show that this implies that the analogue of Hilbert’s 10th Problem for $T (L_{BT})$ is undecidable. In Section 4, we give a direct proof of this result by encoding computation by Turing machines. The construction is inspired by the methods we develop in this section.

Let $L_{0}$ and $L_{1}$ be finite (one-sorted) first-order languages. A $L_{0}$ -structure $A$ is ∃-interpretable (existentially interpretable) in a $L_{1}$ -structure $B$ if

we can find an existential $L_{1}$ -formula $δ (x)$ that defines a non-empty subset $A^{'}$ of the universe B of $B$

for each constant symbol c of $L_{0}$ , we can find an existential $L_{1}$ -formula $ϕ_{c} (x)$ that defines a unique element $c^{'} \in A^{'}$

for each n-ary function symbol f of $L_{0}$ , we can find an existential $L_{1}$ -formula $ϕ_{f} (x_{1}, \dots, x_{n}, y)$ that defines a function from ${(A^{'})}^{n}$ to $A^{'}$

for each n-ary relation symbol R of $L_{0}$ , we can find existential $L_{1}$ -formulas $ϕ_{R} (x_{1}, \dots, x_{n})$ , $ϕ_{R^{c}} (x_{1}, \dots, x_{n})$ that define disjoint sets $R^{'} \subseteq {(A^{'})}^{n}$ , ${(R^{c})}^{'} \subseteq {(A^{'})}^{n}$ such that $R^{'} \cup {(R^{c})}^{'} = {(A^{'})}^{n}$

(1)–(4) define a $L_{0}$ -structure $A^{'}$ that is isomorphic to $A$ .

The formulas that occur in (1)–(4) are parameter-free. That is, we display all free variables. If $A$ is ∃-interpretable in $B$ and $B$ is ∃-interpretable in $A$ , we say that $A$ and $B$ are mutually ∃-interpretable.

The following proposition summarizes important properties of this notion. They are straightforward and the proof is therefore omitted.

Proposition 9.
Let $A$ , $B$ and $C$ be first-order structures in finite languages.
If $A$ is ∃-interpretable in $B$ and $B$ is ∃-interpretable in $C$ , then $A$ is ∃-interpretable in $C$ .

If $A$ is ∃-interpretable in $B$ and ${Th}^{\exists} (B)$ is decidable, then ${Th}^{\exists} (A)$ is decidable.

3.1. Numbers

The first step towards an existential interpretation of $(N, 0, 1, +, \times)$ in $T (L_{BT})$ is to associate the set $N$ of natural numbers with an existentially definable class of finite binary trees. In Section 2.5, we associated the set of natural numbers with a class $N$ of binary trees by mapping the natural number n to the finite binary tree $⊥^{n + 2}$ (see Fig. 7 for examples). We can translate addition on $N$ as follows $x + y = z \equiv z = x [⊥^{2} \mapsto y]$ . The translation of multiplication is a bit more demanding. We develop the tools we need to handle multiplication in Section 3.2. In this section, we show that a number of $N$ -like classes of finite binary trees are existentially definable in $T (L_{BT})$ .

Given a binary tree t, we could have associated the natural number n with the binary tree $t^{n + 2}$ . We can generalize this construction. Given a finite list $t_{1}, \dots, t_{m}$ of binary trees, we can associate the natural number n with the binary tree ${⟨ t_{1}, \dots, t_{m} ⟩}^{n + 2}$ (see Section 2.2 for the notation). The definition of ${⟨ t_{1}, \dots, t_{m} ⟩}^{n}$ does not refer directly to the substitution operator. We work with a natural generalization that uses the substitution operator. The construction is so simple that it has a quantifier-free definition in $T (L_{BT})$ .

To improve readability, it will occasionally be more convenient to represent finite binary trees using notation that is closer to their visual form.

Definition 10.
Let $\begin{matrix} ⟨ x_{1} ⟩ \equiv x_{1} and ⟨ x_{1}, \dots, x_{m}, x_{m + 1} ⟩ \equiv ⟨ ⟨ x_{1}, \dots, x_{m} ⟩, x_{m + 1} ⟩ . \end{matrix}$

Recall that H denotes the set of all finite full binary trees.
Definition 11.
Let $α \in H$ . Let $s_{1}, \dots, s_{n} \in H$ be such that α is not a subtree of $s_{i}$ for all $i ⩽ n$ and $s_{n} \neq s_{j}$ for all $j < n$ . Let $\begin{matrix} \frac{1}{α, \vec{s}} \equiv ⟨ α, s_{1}, \dots, s_{n} ⟩ and \frac{m + 1}{α, \vec{s}} \equiv \frac{1}{α, \vec{s}} [α \mapsto \frac{m}{α, \vec{s}}] . \end{matrix}$ Let $\begin{matrix} N_{\vec{s}}^{α} = {\frac{m}{α, \vec{s}} \in H : m \in N \land m ⩾ 1} . \end{matrix}$

For example, the binary trees $\frac{5}{α, s}$ , $\frac{2}{⟨ α, β ⟩, s, t}$ , $\frac{2}{α, r, s, t}$ are drawn in Fig. 8.

Figure 8.
Visualization of the binary trees $\frac{5}{α, s}$ , $\frac{2}{⟨ α, β ⟩, s, t}$ , $\frac{2}{α, r, s, t}$ .
Lemma 12.
Let $α \in H$ . Let $s_{1}, \dots, s_{n} \in H$ be such that α is not a subtree of $s_{i}$ for all $i ⩽ n$ and $s_{n} \neq s_{j}$ for all $j < n$ . Then, for all $T \in H$ $\begin{matrix} T \in N_{\vec{s}}^{α} \Leftrightarrow T = \frac{1}{α, \vec{s}} \lor (\frac{2}{α, \vec{s}} ⊑ T \land T = \frac{1}{α, \vec{s}} [α \mapsto T [\frac{2}{α, \vec{s}} \mapsto \frac{1}{α, \vec{s}}]]) . \end{matrix}$
Proof.
The left-right implication of the claim is straightforward. Let the size of a binary tree T be the number of nodes in T. We prove by induction on the size of T that $\begin{matrix} () & T = \frac{1}{α, \vec{s}} \lor (\frac{2}{α, \vec{s}} ⊑ T \land T = \frac{1}{α, \vec{s}} [α \mapsto T [\frac{2}{α, \vec{s}} \mapsto \frac{1}{α, \vec{s}}]]) \end{matrix}$ implies $T \in N_{\vec{s}}^{α}$ .

Assume T satisfies (). We need to show that $T \in N_{\vec{s}}^{α}$ . If $T = \frac{1}{α, \vec{s}}$ , then certainly $T \in N_{\vec{s}}^{α}$ . Otherwise, by the second disjunct in (), $\frac{2}{α, \vec{s}} ⊑ T$ . Let $\begin{matrix} S = T [\frac{2}{α, \vec{s}} \mapsto \frac{1}{α, \vec{s}}] . \end{matrix}$ Then, S is strictly smaller than T. By the second disjunct in () $\begin{matrix} T = \frac{1}{α, \vec{s}} [α \mapsto S] . \end{matrix}$ By Definition 11, $\frac{1}{α, \vec{s}} = ⟨ α, s_{1}, \dots, s_{n} ⟩$ . Since α is not a subtree of any $s_{i}$ $\begin{aligned} T & = \frac{1}{α, \vec{s}} [α \mapsto S] \\ = ⟨ α, s_{1}, \dots, s_{n} ⟩ [α \mapsto S] \\ () & = ⟨ S, s_{1}, \dots, s_{n} ⟩ . \end{aligned}$ We know that $\frac{2}{α, \vec{s}} ⊑ T$ . By Definition 11, $\frac{2}{α, \vec{s}} = ⟨ α, s_{1}, \dots, s_{n}, s_{1}, \dots, s_{n} ⟩$ . Since $s_{n} \neq s_{j}$ for all $1 ⩽ j < n$ , it follows from $\frac{2}{α, \vec{s}} ⊑ T$ and () that we have one of the following cases: (i) $S = \frac{1}{α, \vec{s}}$ , (ii) occurrences of $\frac{2}{α, \vec{s}}$ in T can only be found in S. In case of (ii) $\begin{array}{rcl} S & = & T [\frac{2}{α, \vec{s}} \mapsto \frac{1}{α, \vec{s}}] \\ = & ⟨ S, s_{1}, \dots, s_{n} ⟩ [\frac{2}{α, \vec{s}} \mapsto \frac{1}{α, \vec{s}}] \\ = & ⟨ S [\frac{2}{α, \vec{s}} \mapsto \frac{1}{α, \vec{s}}], s_{1}, \dots, s_{n} ⟩ \\ = & ⟨ α, s_{1}, \dots, s_{n} ⟩ [α \mapsto S [\frac{2}{α, \vec{s}} \mapsto \frac{1}{α, \vec{s}}]] \\ = & \frac{1}{α, \vec{s}} [α \mapsto S [\frac{2}{α, \vec{s}} \mapsto \frac{1}{α, \vec{s}}]] . \end{array}$ We thus see that in case of either (i) or (ii), S satisfies (*). Hence, by the induction hypothesis, $S \in N_{\vec{s}}^{α}$ . It then follows from (**) that $T \in N_{\vec{s}}^{α}$ . □
3.2. Multiplication

When we existentially interpret $(N, 0, 1, + \times)$ in the next section, $N_{\vec{s}}^{α}$ is used to find an existentially definable domain while the substitution operator is used to show that addition is existentially definable on this domain. In this section, we develop the tools that will allow us to show that multiplication is existentially definable. The classes $N_{\vec{s}}^{α}$ on their own are not sufficient to show that multiplication is existentially definable since elements of the classes $N_{\vec{s}}^{α}$ have a simple repetitive structure. We need to show that classes of finite binary trees with a bit more complex structure are existentially definable.

We are interested in describing the relation $x \times y = z$ , on the set of natural numbers, by existential $L_{BT}$ -formulas. Our approach is to characterize $x \times y = z$ in terms of the computation tree of $x \times y$ . We know that given three natural numbers $n, k, m > 0$ , the equality $n \times k = m$ holds if and only if there exists a sequence of pairs of natural numbers $\begin{matrix} (*) & (k_{1}, m_{1}), (k_{2}, m_{2}), \dots, (k_{r}, m_{r}) \end{matrix}$ such that

$k_{1} = 1$ and $m_{1} = n$

$k_{i + 1} = k_{i} + 1$ and $m_{i + 1} = m_{i} + n$ for $1 ⩽ i < r$

$k_{r} = k$ and $m_{r} = m$ .

We start by characterizing the existence of (*) in terms of finite binary trees. For technical reasons which have to do with the proof of Lemma 14, we work with two distinct representations of natural numbers. We use one representation to encode numbers in the sequence $k_{1}, \dots, k_{r}$ , and we use another representation to encode numbers in the sequence $m_{1}, \dots, m_{r}$ . Let α, β be finite binary trees that are incomparable with respect to the subtree relation. Let s and t be such that α is a substree of neither s nor t, and β is a subtree of neither s nor t. We have the following two ways of associating natural numbers with finite binary trees (see Definition 11):

We map the natural n to the binary tree $\frac{n}{α, s}$ defined by recursion as follows $\begin{matrix} \frac{0}{α, s} \equiv α and \frac{n + 1}{α, s} \equiv ⟨ α, s ⟩ [α \mapsto \frac{n}{α, s}] . \end{matrix}$

We map the natural n to the binary tree $\frac{n}{β, t}$ defined by recursion as follows $\begin{matrix} \frac{0}{β, t} \equiv β and \frac{n + 1}{β, t} \equiv ⟨ β, t ⟩ [β \mapsto \frac{n}{β, t}] . \end{matrix}$

We use (A) to represent the sequence $k_{1}, \dots, k_{r}$ , and we use (B) to represent the sequence $m_{1}, \dots, m_{r}$ . We can now characterize the existence of (*) in terms of finite binary trees. Given three natural numbers $n, k, m > 0$ , the equality $n \times k = m$ holds if and only if there exists a sequence of pairs of finite binary trees $\begin{matrix} (**) & ⟨ u_{1}, v_{1} ⟩, ⟨ u_{2}, v_{2} ⟩, \dots, ⟨ u_{r}, v_{r} ⟩ \end{matrix}$ such that

$u_{1} = \frac{1}{α, s}$ and $v_{1} = \frac{n}{β, t}$

given $1 ⩽ i < r$ , if $u_{i} = \frac{j_{0}}{α, s}$ and $v_{i} = \frac{j_{1}}{β, t}$ , then $u_{i + 1} = \frac{j_{0} + 1}{α, s}$ and $v_{i + 1} = \frac{j_{1} + n}{β, t}$

$u_{r} = \frac{k}{α, s}$ and $v_{r} = \frac{m}{β, t}$ .

The next step is to associate (**) with a finite binary tree. Let γ be a finite binary tree that is such that α, β, γ are incomparable with respect to the subtree relation. Using the notation of Definition 10, we associate (**) with the finite binary tree $\begin{matrix} (***) & ⟨ γ, ⟨ u_{1}, v_{1} ⟩, ⟨ u_{2}, v_{2} ⟩, \dots, ⟨ u_{r}, v_{r} ⟩ ⟩ . \end{matrix}$ For example, the left tree in Fig. 9 represents $5 \times 3 = 15$ and the right tree in Fig. 9 represents $50 \times 3 = 150$ .

Figure 9.

Encoding $5 \times 3 = 15$ and $50 \times 3 = 150$ with finite binary trees.

Now that we have a way of associating $n \times k = m$ with a particular finite binary tree $T (n, k, m)$ , we need to find an existentially definable class that contains $T (n, k, m)$ and is such that it is easy to characterize $T (n, k, m)$ in terms of representations of n, k, m. Our approach is the following: Given a fixed natural number $n > 0$ , let $M_{s, t, n}^{α, β, γ}$ denote the class of all finite binary trees S of the form (***), i.e., S encodes the computation tree of $n \times k$ for some $k > 0$ . After giving a formal definition of $M_{s, t, n}^{α, β, γ}$ , we prove that $M_{s, t, n}^{α, β, γ}$ is existentially definable. That $M_{s, t, n}^{α, β, γ}$ is existentially definable means that we can associate it with some existential $L_{BT}$ -formula $ψ (x, α, β, γ, s, t, \frac{n}{β, t})$ , where x is the defining variable and α, β, γ, s, t, $\frac{n}{β, t}$ are parameters.

Definition 13.

Let $α, β, γ \in H$ be incomparable with respect to the subtree relation. Let $s, t \in H$ be such that α is a substree of neither s nor t and β is a subtree of neither s nor t. Let $n ⩾ 1$ . Let $M_{s, t, n}^{α, β, γ}$ denote the smallest class of finite full binary trees that satisfies the following

$⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ \in M_{s, t, n}^{α, β, γ}$

if $T \in M_{s, t, n}^{α, β, γ}$ and $T = ⟨ R, ⟨ \frac{k}{α, s}, \frac{m}{β, t} ⟩ ⟩$ , then $⟨ T, ⟨ \frac{k + 1}{α, s}, \frac{m + n}{β, t} ⟩ ⟩ \in M_{s, t, n}^{α, β, γ}$ .

To improve readability, we introduce the following abbreviation $\begin{matrix} t [r_{1} \mapsto s_{1}, r_{2} \mapsto s_{2}, \dots, r_{k} \mapsto s_{k}] \equiv t [r_{1} \mapsto s_{1}] [r_{2} \mapsto s_{2}] \dots [r_{k} \mapsto s_{k}] . \end{matrix}$

Lemma 14.

Let $α, β, γ \in H$ be incomparable with respect to the subtree relation. Let $s, t \in H$ be such that α is a substree of neither s nor t and β is a subtree of neither s nor t. Let $n ⩾ 1$ . Let $T \in H$ . Then, $T \in M_{s, t, n}^{α, β, γ}$ if and only if

$⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ ⊑ T$

there exist $L \in N_{s}^{α} \cup {α}$ and $R \in N_{t}^{β} \cup {β}$ such that $\begin{matrix} T = ⟨ T [⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ \mapsto γ, \frac{1}{α, s} \mapsto α, \frac{n}{β, t} \mapsto β], ⟨ L, R ⟩ ⟩ . \end{matrix}$

Before we prove the lemma, we illustrate with an example how (1)–(2) work. Assume T is the right tree in Fig. 9, which encodes the computation tree of $50 \times 3$ . So $\begin{matrix} T = ⟨ γ, ⟨ \frac{1}{α, s}, \frac{50}{β, t} ⟩, ⟨ \frac{2}{α, s}, \frac{100}{β, t} ⟩, ⟨ \frac{3}{α, s}, \frac{150}{β, t} ⟩ ⟩ . \end{matrix}$ Since $⟨ \frac{1}{α, s}, \frac{50}{β, t} ⟩$ occurs only at the bottom of T, we have $\begin{array}{rcl} T_{0} & : = & T [⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ \mapsto γ] \\ = & ⟨ γ, ⟨ \frac{2}{α, s}, \frac{100}{β, t} ⟩, ⟨ \frac{3}{α, s}, \frac{150}{β, t} ⟩ ⟩ . \end{array}$ The binary tree $\frac{1}{α, s}$ occurs in $T_{0}$ only at the bottom of $\frac{2}{α, s}$ and $\frac{3}{α, s}$ . Hence $\begin{array}{rcl} T_{1} & : = & T_{0} [\frac{1}{α, s} \mapsto α] \\ = & ⟨ γ, ⟨ \frac{1}{α, s}, \frac{100}{β, t} ⟩, ⟨ \frac{2}{α, s}, \frac{150}{β, t} ⟩ ⟩ . \end{array}$ The binary tree $\frac{50}{β, t}$ occurs in $T_{1}$ only at the bottom of $\frac{100}{β, s}$ and $\frac{150}{β, t}$ . Hence $\begin{array}{rcl} T_{2} & : = & T_{1} [\frac{50}{β, t} \mapsto β] \\ = & ⟨ γ, ⟨ \frac{1}{α, s}, \frac{50}{β, t} ⟩, ⟨ \frac{2}{α, s}, \frac{100}{β, t} ⟩ ⟩ . \end{array}$

Proof of Lemma 14.

The only if part is obvious. We prove the if part by induction on the size of T. We need the following properties:

Since α, β, γ are incomparable with respect to the subtree relation, the binary tree $⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩$ is not a subtree of elements of the form $⟨ u, v ⟩$ where $u, v \in N_{s}^{α} \cup N_{t}^{β} \cup {α, β}$ .

Since α, β are incomparable with respect to the subtree relation and α is not a substree of t, the binary tree $\frac{1}{α, s}$ is not a subtree of elements of $N_{t}^{β} \cup {β}$ .

Since α, β are incomparable with respect to the subtree relation and β is not a substree of s, the binary tree $\frac{n}{β, t}$ is not a subtree of elements of $N_{s}^{α} \cup {α}$ and $s \notin N_{t}^{β} \cup {β}$ .

Assume T satisfies (1)–(2). We need to show that $T \in M_{s, t, n}^{α, β, γ}$ . Recall that (see Definition 11) $\begin{array}{c} \frac{0}{α, s} = α \land \forall L \in N_{s}^{α} \exists k \in N [k ⩾ 1 \land L = \frac{k}{α, s}] and \\ \frac{0}{β, t} = β \land \forall R \in N_{t}^{β} \exists m \in N [m ⩾ 1 \land R = \frac{m}{β, t}] . \end{array}$ Hence, since T satisfies (1)–(2), there exist natural numbers $k, m ⩾ 0$ such that $\begin{array}{c} (i) & ⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ ⊑ T \\ (ii) & T = ⟨ T [⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ \mapsto γ, \frac{1}{α, s} \mapsto α, \frac{n}{β, t} \mapsto β], ⟨ \frac{k}{α, s}, \frac{m}{β, t} ⟩ ⟩ . \end{array}$

Let $\begin{matrix} S = T [⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ \mapsto γ, \frac{1}{α, s} \mapsto α, \frac{n}{β, t} \mapsto β] . \end{matrix}$ Assume $S = γ$ . By (i), $⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩$ is a subtree of T. By (A), $⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩$ is not a subtree of $⟨ \frac{k}{α, s}, \frac{m}{β, t} ⟩$ . Hence $\begin{matrix} T = ⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ \in M_{s, t, n}^{α, β, γ} . \end{matrix}$

Assume now $S \neq γ$ . Since T satisfies (i), $⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩$ is a subtree of T. By (A), $⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩$ is not a subtree of $⟨ \frac{k}{α, s}, \frac{m}{β, t} ⟩$ . Hence, by (ii) and the definition of S $\begin{matrix} (iii) & ⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ ⊑ S . \end{matrix}$ By (ii) and (A)–(C) $\begin{aligned} S & = T [⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ \mapsto γ, \frac{1}{α, s} \mapsto α, \frac{n}{β, t} \mapsto β] \\ = ⟨ S, ⟨ \frac{k}{α, s}, \frac{m}{β, t} ⟩ ⟩ [⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ \mapsto γ, \frac{1}{α, s} \mapsto α, \frac{n}{β, t} \mapsto β] \\ (iv) & = ⟨ S [⟨ γ, ⟨ \frac{1}{α, s}, \frac{n}{β, t} ⟩ ⟩ \mapsto γ, \frac{1}{α, s} \mapsto α, \frac{n}{β, t} \mapsto β], ⟨ \frac{k \dot{-} 1}{α, s}, \frac{m \dot{-} n}{β, t} ⟩ ⟩ . \end{aligned}$ where $\begin{matrix} x \dot{-} y = \{\begin{array}{ll} x & if x < y \\ x - y & otherwise. \end{array} \end{matrix}$ By (iii)–(iv), S satisfies (1)–(2). Hence, by the induction hypothesis, $S \in M_{s, t, n}^{α, β, γ}$ . It then follows from (iv) and (ii) that $T \in M_{s, t, n}^{α, β, γ}$ .

Thus, by induction, $T \in M_{s, t, n}^{α, β, γ}$ if T satisfies (1)–(2). □

In the proof of Lemma 14, we did not use the assumption that α is not a substree of s and β is not a substree of t. With these assumptions, Lemma 12 tells us that $N_{s}^{α} \cup {α}$ and $N_{t}^{β} \cup {β}$ are existentially definable in $T (L_{BT})$ . Thus, Lemma 14 shows that $M_{s, t, n}^{α, β, γ}$ is existentially definable in $T (L_{BT})$ .

3.3. Arithmetic with the substitution operator

We are finally ready to give an existential interpretation of $(N, 0, 1, +, \times)$ in $T (L_{BT})$ . Lemma 12 will allow us to specify an existentially definable domain while Lemma 14 will allow us to give an existential definition of multiplication on the chosen domain. Addition will be handled very easily using the substitution operator.

Theorem 15.
$(N, 0, 1, +, \times)$ is ∃-interpretable in $T (L_{BT})$ . Hence, ${Th}^{\exists} (T (L_{BT}))$ is undecidable.
Proof.
Let $\begin{matrix} 0 \equiv ⟨ ⊥, ⊥ ⟩, s \equiv ⊥, t = s and n \equiv \frac{n}{0, s} for each n ⩾ 1 . \end{matrix}$ Lemma 12 tells us that the class $N : = N_{s}^{0} \cup {0}$ is existentially definable in $T (L_{BT})$ . We translate addition on $N$ as follows $\begin{matrix} x + y = z \equiv N (x) \land N (y) \land N (z) \land z = y [0 \mapsto x] . \end{matrix}$ We use Lemma 14 to give a translation of multiplication on $N$ . Let $\begin{matrix} γ \equiv ⟨ ⊥, ⊥^{3} ⟩, α \equiv ⟨ ⊥, ⊥^{4} ⟩, β \equiv ⟨ ⊥, ⊥^{5} ⟩ . \end{matrix}$ Let $\begin{array}{rcl} x \times y & = & z \equiv N (x) \land N (y) \land N (z) \\ \land ((x = 0 \land z = 0) \lor (y = 0 \land z = 0) \lor (x \neq 0 \land y \neq 0 \land Φ (x, y, z))) \end{array}$ where $\begin{matrix} Φ (x, y, z) \equiv \exists n, v, w [n = x [0 \mapsto β] \land M_{s, t, n}^{α, β, γ} (w) \land w = ⟨ v, ⟨ y [0 \mapsto α], z [0 \mapsto β] ⟩ ⟩] . \end{matrix}$ It follows from the definition of $M_{s, t, n}^{α, β, γ}$ that $Φ (x, y, z)$ captures correctly $x \times y = z$ when $x, y > 0$ . □

Since computably enumerable sets of natural numbers are Diophantine, we have the following corollary. Corollary 16.
$(N, 0, 1, +, \times)$ and $T (L_{BT})$ are mutually ∃-interpretable.

3.4. Analogue of Hilbert’s 10th problem

In this section, we show that the analogue of Hilbert’s 10th Problem for $T (L_{BT})$ is undecidable. That is, we show that there cannot exist an algorithm that takes as input an $L_{BT}$ -sentence of the form $\exists \vec{x} [s = t]$ and decides whether $\exists \vec{x} [s = t]$ is true in $T (L_{BT})$ . Let ${Th}^{H 10} (T (L_{BT}))$ denote the set of all sentences of the form $\exists \vec{x} [s = t]$ that are true in $T (L_{BT})$ .

Theorem 17.
The fragment ${Th}^{H 10} (T (L_{BT}))$ is undecidable.
Proof.
Since ${Th}^{\exists} (T (L_{BT}))$ is undecidable, it suffices to show that given an existential $L_{BT}$ -sentence ϕ, we can compute a finite number of $L_{BT}$ -sentences $ϕ_{1}, \dots, ϕ_{n}$ of the form $\exists \vec{x} [s = t]$ such that $\begin{matrix} T (L_{BT}) ⊧ ϕ \leftrightarrow ⋁_{i = 1}^{n} ϕ_{i} . \end{matrix}$ Since $\begin{matrix} T (L_{BT}) ⊧ (s_{1} = t_{1} \land s_{2} = t_{2}) \leftrightarrow ⟨ s_{1}, s_{2} ⟩ = ⟨ t_{1}, t_{2} ⟩ \end{matrix}$ it suffices to show that given a $L_{BT}$ -formula of the form $s \neq t$ , we can compute a finite number of atomic $L_{BT}$ -formulas $s_{1} = t_{1}, \dots, s_{k} = t_{k}$ such that $\begin{matrix} T (L_{BT}) ⊧ s \neq t \leftrightarrow ⋁_{j = 1}^{k} s_{j} = t_{j} . \end{matrix}$ This is the case since $\begin{matrix} s \neq t \Leftrightarrow s ⋢ t \lor t ⋢ s \Leftrightarrow t [s \mapsto ⟨ s, s ⟩] = t \lor s [t \mapsto ⟨ t, t ⟩] = s . \end{matrix}$ □

4. Computability on trees

This section is motivated by the following question: can we extend the existential interpretation in Section 3 of $(N, 0, 1, +, \times)$ to an existential interpretation of $(N, 0, 1, +, \times, exp)$ without relying on the solution to Hilbert’s 10th Problem? We give a positive answer by encoding computations by Turing machines.

The work of Matiyasevich, Robinson, Davis and Putnam not only settles Hilbert’s 10th problem but also gives a nice characterization of the subsets of $N$ existentially definable in $(N, 0, 1, +, \times)$ : A set $A \subseteq N$ is computably enumerable if and only if there exist polynomials $p_{A} (t, \vec{x}), q_{A} (t, \vec{x}) \in N [t, \vec{x}]$ such that for all $n \in N$ , $n \in A$ if and only if $p_{A} (n, \vec{x}) = q_{A} (n, \vec{x})$ has a solution in $N$ . It is not clear to us whether an analogous result holds for $T (L_{BT})$ .

Open Problem 18.
Is every computably enumerable subset of H existentially definable in $T (L_{BT})$ ?

4.1. Regular tree grammars

We start by showing that regular tree languages in the signature ${⊥, ⟨ \cdot, \cdot ⟩}$ are existentially definable in $T (L_{BT})$ (see Gecseg & Steinby [5] for a survey of regular tree languages). It is not a priori obvious that this should be the case. Consider the following two relations on finite strings over an alphabet with two distinct letters 0 and 1: $(u, v) \in L$ if and only if u and v have the same length, and $(u, v) \in P$ if and only if the number of 0‘s in u is the same as the number of 0‘s in v. It follows easily from the proof of Theorem 2 of Büchi and Senger [1] that $(N, 0, 1, +, \times)$ is existentially interpretable in $({0, 1, 2}^{*}, ε, 0, 1, 2,^{⌢}, L, P)$ , the free monoid generated by ${0, 1, 2}$ extended with $L$ and $P$ . On the other hand, a minor modification to the proof of Theorem 16 of Karhumäki et al. [7] shows that the regular language ${0, 1}^{*}$ is not existentially definable in $({0, 1, 2}^{*}, ε, 0, 1, 2,^{⌢}, L, P)$ . The necessary changes will be obvious to a reader familiar with [7] and the details are therefore omitted. Theorem 16 of [7] is a pumping lemma-like result for finitely generated free semigroups.

A regular tree grammar is a system $G = (N, L, P, a_{0})$ where: (1) $L$ is a finite set of constant symbols and function symbols, (2) N is a finite set of constant symbols disjoint from $L$ , (3) $a_{0} \in N$ , (4) P is a finite set of rules of the form $a \to r$ where $a \in N$ and r is a variable-free term over the language $L \cup N$ . The one-step derivation relation $\Rightarrow_{G}$ is defined as follows: $s \Rightarrow_{G} t$ if and only if there exists a rule $a \to r$ of P such that we obtain t from s by replacing exactly one occurrence of a in s with r. We denote by $\Rightarrow_{G}^{*}$ the reflexive transitive closure of $\Rightarrow_{G}$ . The tree language $L (G)$ generated by G is the set of all variable-free $L$ -terms t such that $a_{0} \Rightarrow_{G}^{*} t$ . We give an example that will be important to us. We use the notation $α \to β_{1} | β_{2} | \dots | β_{n}$ for a finite list of rules $α \to β_{1}, \dots, α \to β_{n}$ (we interpret | as or). Recall that ⊑ denotes the subtree relation.

Example 19.
Let $A = {a_{1}, \dots, a_{n}}$ be a finite alphabet. Let $A^{}$ denote the set of all finite strings over A. Let $A^{+} = A^{} ∖ {ε}$ where ε denotes the empty string. For each natural number $i ⩾ 1$ , let $g_{i} \equiv ⟨ ⊥^{3 + i}, ⊥^{3 + i} ⟩$ . Let $α \in H$ be incomparable with $g_{i}$ with respect to ⊑ for all i. We define a one-to-one map $τ_{α} : A^{} \to H$ by recursion $\begin{matrix} τ_{α} (w) = \{\begin{array}{ll} α & if w = ε \\ ⟨ α, g_{i} ⟩ & if w = a_{i} \\ τ_{α} (w_{0}) [α \mapsto τ_{α} (w_{1})] & if w = w_{0} w_{1} and w_{0} \in A . \end{array} \end{matrix}$

Let c be a fresh constant symbol. The following regular tree grammar generates $τ_{α} (A^{})$ $\begin{matrix} c \to α | ⟨ c, g_{1} ⟩ | ⟨ c, g_{2} ⟩ | \dots | ⟨ c, g_{n} ⟩ . \end{matrix}$ Replacing the rule $c \to α$ with the n rules $c \to τ_{α} (a_{i})$ gives a regular tree grammar that generates $τ_{α} (A^{+})$ . Observe that reading $τ_{α} (s)$ bottom-up corresponds to reading s from right to left. The same grammar works if we use the dual definition where we read s from left to right.

We introduce the key technical device. We write $x ⊥ y$ for $x ⋢ y \land y ⋢ x$ .
Definition 20.
A regular binary tree grammar G is a finite list of rules $\begin{matrix} α_{1} \to β_{1, 1} | β_{1, 2} | \dots | β_{1, n_{1}}, \dots, α_{m} \to β_{m, 1} | β_{m, 2} | \dots | β_{m, n_{m}} \end{matrix}$ such that: (1) if $i \neq j$ , then $α_{i} ⊥ α_{j}$ , (2) $β_{k, j} ⋢ α_{ℓ}$ for all k, j, ℓ, (3) $β_{k_{0}, i} ⊥ β_{k_{1}, j}$ if $(k_{0}, i) \neq (k_{1}, j)$ , (4) there exists $γ \in H$ such that $γ ⊥ α_{k}$ and $γ ⊥ β_{k, i}$ for all k, i.

We write $s \Rightarrow_{G} t$ if there exists a rule $α \to β$ such that we obtain t from s by replacing exactly one occurrence of α in s with β. We denote by $\Rightarrow_{G}^{}$ the reflexive transitive closure of $\Rightarrow_{G}$ . We let $\begin{matrix} R (G) : = {(x, y) \in H^{2} : x \Rightarrow_{G}^{} y \land ⋀_{k = 1}^{m} ⋀_{j = 1}^{n_{k}} β_{k, j} ⋢ x} . \end{matrix}$

We proceed to prove existential definability in $T (L_{BT})$ of the relation $R (G)$ . We then show that this implies existential definability of those subsets of H that are regular tree languages. Recall that $⟨ x_{1}, x_{2}, \dots, x_{2 + k + 1} ⟩$ means $⟨ ⟨ x_{1}, x_{2}, \dots, x_{2 + k} ⟩, x_{2 + k + 1} ⟩$ (see Section 2.2).
Definition 21.
Let G be a regular binary tree grammar with rules $\begin{matrix} α_{1} \to β_{1, 1} | β_{1, 2} | \dots | β_{1, n_{1}}, \dots, α_{m} \to β_{m, 1} | β_{m, 2} | \dots | β_{m, n_{m}} . \end{matrix}$ Let $γ \in H$ be such that $γ ⊥ α_{ℓ}$ and $γ ⊥ β_{ℓ, i}$ for all ℓ, i. Let $W \in W (G, γ)$ if and only if there exists a sequence $W_{1}, W_{2}, \dots, W_{k} \in H$ such that $\begin{matrix} W = ⟨ γ, W_{k}, W_{k - 1}, \dots, W_{1} ⟩ \land γ ⋢ W_{k} \land ⋀_{ℓ = 1}^{m} ⋀_{j = 1}^{n_{ℓ}} β_{ℓ, j} ⋢ W_{k} \end{matrix}$ and for all $i \in {1, 2, \dots, k - 1}$ we obtain $W_{i + 1}$ from $W_{i}$ by simultaneously replacing an occurrence of $β_{ℓ, j}$ with $α_{ℓ}$ .

We show that $W (G, γ)$ is existentially definable (γ is a parameter such $γ ⊥ α_{ℓ}$ and $γ ⊥ β_{ℓ, i}$ for all ℓ, i). This implies existential definability of $R (G)$ since $(x, y) \in R (G)$ if and only if

$x = y \land ⋀_{k = 1}^{m} α_{k} ⋢ x \land ⋀_{k = 1}^{m} ⋀_{j = 1}^{n_{k}} β_{k, j} ⋢ x$ or

there exists γ and $W \in W (G, γ)$ such that y is the immediate right subtree of W and $⟨ γ, x ⟩ ⊑ W$ (such γ exists when $⋁_{k = 1}^{m} α_{k} ⊑ x$ and $⋀_{k = 1}^{m} ⋀_{j = 1}^{n_{k}} β_{k, j} ⋢ x$ : if $δ ⊥ α_{k}$ and $δ ⊥ β_{k, j}$ for all k, j, let $γ = δ^{ℓ}$ for large enough ℓ).

Recall that $x^{1} : = x$ , $x^{2} : = ⟨ x, x ⟩$ and $x^{2 + k + 1} : = ⟨ x^{2 + k}, x ⟩$ ; and $\begin{matrix} t [r_{1} \mapsto s_{1}, r_{2} \mapsto s_{2}, \dots, r_{k} \mapsto s_{k}] : = t [r_{1} \mapsto s_{1}] [r_{2} \mapsto s_{2}] \dots [r_{k} \mapsto s_{k}] . \end{matrix}$
Lemma 22.
Let G be a regular binary tree grammar with rules $\begin{matrix} α_{1} \to β_{1, 1} | β_{1, 2} | \dots | β_{1, n_{1}}, \dots, α_{m} \to β_{m, 1} | β_{m, 2} | \dots | β_{m, n_{m}} . \end{matrix}$ Let $γ \in H$ be such that $γ ⊥ α_{k}$ and $γ ⊥ β_{k, i}$ for all k, i. Let $δ_{k} = ⟨ γ^{3 + k}, γ^{3 + k} ⟩$ . Let $\begin{matrix} F_{α}^{δ} (x) : = x [δ_{1} \mapsto α_{1}, \dots,, δ_{m} \mapsto α_{m}] \end{matrix}$ and $\begin{matrix} F_{δ}^{β} (x) : = x [β_{1, 1} \mapsto δ_{1}, \dots, β_{1, n_{1}} \mapsto δ_{1}, \dots, β_{m, 1} \mapsto δ_{m}, \dots, β_{m, n_{m}} \mapsto δ_{m}] . \end{matrix}$ Let $W \in H$ . Then, $W \in W (G, γ)$ if and only if
there exists $X \in H$ such that $\begin{matrix} ⟨ γ, X ⟩ ⊑ W \land γ ⋢ X \land ⋀_{ℓ = 1}^{n} ⋀_{j = 1}^{n_{ℓ}} β_{ℓ, j} ⋢ X \end{matrix}$

there exist $V, T \in H$ such that $\begin{matrix} γ ⋢ T \land W = ⟨ V, T ⟩ \land V = F_{α}^{δ} F_{δ}^{β} (W [⟨ γ, X ⟩ \mapsto γ]) . \end{matrix}$

Proof.
The left-right implication is a straightforward. We focus on proving the right-left implication. Assume W satisfies (1)–(2). We need to show that $W \in W (G, γ)$ . By Definition, we need to show that there exist $W_{1}, \dots, W_{k} \in H$ such that
$W = ⟨ γ, W_{k}, W_{k - 1}, \dots, W_{1} ⟩$

$⋀_{ℓ = 1}^{m} ⋀_{j = 1}^{n_{ℓ}} β_{ℓ, j} ⋢ W_{k}$ and $γ ⋢ W_{k}$

for all $i \in {1, 2, \dots, k - 1}$ , we obtain $W_{i + 1}$ from $W_{i}$ by simultaneously replacing an occurrence of $β_{ℓ, j}$ with $α_{ℓ}$ .

Let X and T be binary trees that satisfy clauses (1)–(2). First, we prove by (backward) induction that if $⟨ γ, X ⟩ ⊑ U ⊑ W$ and $U = ⟨ U_{0}, U_{1} ⟩$ , then $\begin{matrix} (*) & U_{0} = F_{α}^{δ} F_{δ}^{β} (U [⟨ γ, X ⟩ \mapsto γ]) \end{matrix}$ and $\begin{matrix} (**) & γ ⋢ U_{1} . \end{matrix}$ The base case $U = W$ is Clause (2). So, assume $U = ⟨ V, U_{1} ⟩$ , $V = ⟨ V_{0}, V_{1} ⟩$ , $⟨ γ, X ⟩ ⊑ V ⊑ U ⊑ W$ and U satisfies (*) and (**). We need to show that V satisfies () and (). Since U satisfies (), $⟨ γ, X ⟩ ⋢ U_{1}$ . By the choice of γ, the binary tree $β_{ℓ, j}$ cannot equal a binary tree that has γ as a subtree. Hence, by () $\begin{array}{rcl} V & = & F_{α}^{δ} F_{δ}^{β} (U [⟨ γ, X ⟩ \mapsto γ]) \\ = & F_{α}^{δ} F_{δ}^{β} (⟨ V, U_{1} ⟩ [⟨ γ, X ⟩ \mapsto γ]) \\ = & F_{α}^{δ} F_{δ}^{β} (⟨ V [⟨ γ, X ⟩ \mapsto γ], U_{1} ⟩) \\ = & ⟨ F_{α}^{δ} F_{δ}^{β} (V [⟨ γ, X ⟩ \mapsto γ]), F_{α}^{δ} F_{δ}^{β} (U_{1}) ⟩ . \end{array}$ Thus, V satisfies (*) and (**). Thus, by induction, if $⟨ γ, X ⟩ ⊑ U ⊑ W$ and $U = ⟨ U_{0}, U_{1} ⟩$ , then U satisfies (*) and ().

Now, to prove that (A)–(C) hold, it suffices to prove by induction on the size of finite binary trees that if U is a subtree of W which is such that $⟨ γ, X ⟩ ⊑ U$ , then there exists a sequence $U_{1}, \dots, U_{m}$ such that
$U = ⟨ γ, U_{m}, U_{m - 1}, \dots, U_{1} ⟩$

$U_{m} = X$

$U_{i + 1} = F_{α}^{δ} F_{δ}^{β} (U_{i})$ for all $i \in {1, 2, \dots, m - 1}$ .
So, assume $⟨ γ, X ⟩ ⊑ U ⊑ W$ . If $U = ⟨ γ, X ⟩$ , then U satisfies (i)–(iii) trivially. Otherwise, by (), there exist V and $U_{1}$ such that $U = ⟨ V, U_{1} ⟩$ and $⟨ γ, X ⟩ ⊑ V$ . By the induction hypothesis, there exists a sequence $V_{1}, \dots, V_{m}$ such that
$V = ⟨ γ, V_{m}, V_{m - 1}, \dots, V_{1} ⟩$

$V_{m} = X$

$V_{i + 1} = F_{α}^{δ} F_{δ}^{β} (V_{i})$ for all $i \in {1, 2, \dots, m - 1}$ .
In particular $\begin{matrix} U = ⟨ V, U_{1} ⟩ = ⟨ γ, V_{m}, V_{m - 1}, \dots, V_{1}, U_{1} ⟩ . \end{matrix}$ By (v)–(vi) and (**), there can only be one occurrence of γ in U. Hence $\begin{matrix} U [⟨ γ, X ⟩ \mapsto γ] = ⟨ γ, V_{m - 1}, \dots, V_{1}, U_{1} ⟩ . \end{matrix}$ Then, by () and (vi) $\begin{array}{rcl} ⟨ γ, V_{m}, V_{m - 1}, \dots, V_{1} ⟩ & = & V \\ = & F_{α}^{δ} F_{δ}^{β} (U [⟨ γ, X ⟩ \mapsto γ]) \\ = & F_{α}^{δ} F_{δ}^{β} (⟨ γ, V_{m - 1}, \dots, V_{1}, U_{1} ⟩) \\ = & ⟨ γ, F_{α}^{δ} F_{δ}^{β} (V_{m - 1}), \dots, F_{α}^{δ} F_{δ}^{β} (V_{1}), F_{α}^{δ} F_{δ}^{β} (U_{1}) ⟩ \\ = & ⟨ γ, V_{m}, \dots, V_{2}, F_{α}^{δ} F_{δ}^{β} (U_{1}) ⟩ . \end{array}$ Hence $\begin{matrix} U = ⟨ γ, V_{m}, V_{m - 1}, \dots, V_{1}, U_{1} ⟩ \land V_{1} = F_{α}^{δ} F_{δ}^{β} (U_{1}) . \end{matrix}$ Thus, U satisfies (i)–(iii).

Thus, by induction, if U is a subtree of W which is such that $⟨ γ, X ⟩ ⊑ U$ , then U satisfies (i)–(iii). □
Theorem 23.
Let G be a regular binary tree grammar. Then,* $R (G)$ is existentially definable in $T (L_{BT})$ .

Regular tree languages have an equivalent definition in terms of deterministic bottom-up finite tree recognizers (see [5] [Proposition 6.2]). Such a recognizer is a triple $A = (A, F)$ where $A$ is a finite $L$ -structure with universe A and $F \subseteq A$ . We have the homomorphism $τ : H (L) \to A$ from the term algebra defined by $L$ to $A$ . The language recognized by A is the set $L (A)$ of all variable-free $L$ -terms t such that $τ (t) \in F$ . Now, observe that for each $c \in F$ , we can define a regular tree grammar $G_{c}$ such that $L (A) = ⋃_{c \in F} L (G_{c})$ : let $G_{c} = (A, L, P, c)$ where $a \to f (a_{1}, \dots, a_{m})$ is a rule if and only if $a, a_{i} \in A$ , $f \in L$ and $f^{A} (a_{1}, \dots, a_{m}) = a$ . Thus, to prove existential definability of regular tree languages, it suffices to restrict to grammars of this form.
Theorem 24.
Assume $A \subseteq H$ is a regular tree language. Then, A is existentially definable in $T (L_{BT})$ .
Proof.
Let $L = {⊥, ⟨ \cdot, \cdot ⟩}$ . Given a deterministic bottom-up finite tree recognizer $A = (A, F)$ and $c \in F$ , let $G_{c} = (A, L, P, c)$ be as defined above. Consider the following regular binary tree grammar H: we enumerate $A = {a_{1}, \dots, a_{N}}$ . Let $σ (a_{k}) = ⟨ ⊥^{3 + k}, ⊥^{3 + k} ⟩$ . If $a_{k} \to r$ is a rule of P, we add to H the rule $σ (a_{k}) \to σ (r)$ where:
$σ (r) = ⟨ ⊥^{3 + N + 1}, ⊥^{3 + N + 1} ⟩$ if $r = ⊥$

$σ (r) = ⟨ σ (a_{i}), σ (a_{j}) ⟩$ if $r = ⟨ a_{i}, a_{j} ⟩$ for some i, j.
By Theorem 23, $L (H) : = {t \in H : σ (c) \Rightarrow_{H}^{} t \land ⋀_{k = 1}^{N} σ (a_{k}) ⋢ t}$ is existentially definable in $T (L_{BT})$ . Then, $T \in L (G_{c})$ if and only if there exists $S \in L (H)$ such that $\begin{matrix} T = S [⟨ ⊥^{3 + N + 1}, ⊥^{3 + N + 1} ⟩ \mapsto ⊥] . \end{matrix}$ □

We conclude this section by showing that Lemma 22 in fact gives existential definability of more than just the regular tree languages. Consider the height function $ρ : H \to H$ that maps a binary tree x to the binary tree $⊥^{m}$ where m is the number of nodes in a longest path $\begin{matrix} ρ (x) = \{\begin{array}{ll} ⊥ & if x = ⊥ \\ ⟨ ρ (y), ⊥ ⟩ & if x = ⟨ y, z ⟩ and ρ (z) ⊑ ρ (y) \\ ⟨ ρ (z), ⊥ ⟩ & if x = ⟨ y, z ⟩ and ρ (y) ⊑ ρ (z) . \end{array} \end{matrix}$ The set ${⟨ x, y ⟩ \in H : ρ (x) = y}$ is not a regular tree language (as can be shown with the pumping lemma, see Gecseg & Steinby [5] [Proposition 5.2]).
Theorem 25.
The set* ${⟨ x, y ⟩ \in H : ρ (x) = y}$ is existentially definable in $T (L_{BT})$ .
Proof.
We use that the set $N = {⊥^{m} : m ⩾ 1}$ is existentially definable. Let $α = ⟨ ⊥^{4}, ⊥^{4} ⟩$ , $β = ⟨ ⊥^{5}, ⊥^{5} ⟩$ and $γ = ⟨ ⊥^{6}, ⊥^{6} ⟩$ . Consider the regular binary tree grammar $\begin{matrix} G : = α \to ⟨ α, α ⟩, β \to ⟨ β, β ⟩ . \end{matrix}$ Let $\begin{matrix} F_{α} (x) = x [⊥ \mapsto α] and F_{β} (x) = x [⊥ \mapsto β] . \end{matrix}$ If $ρ (x) = y$ , then $⟨ α, β ⟩ \Rightarrow_{G}^{*} ⟨ F_{α} (x), F_{β} (y) ⟩$ , but the converse does not hold. We have $ρ (x) = y$ if and only if $y \in N$ and there exists $W \in W (G, γ)$ such that $\begin{array}{r} ⟨ γ, ⟨ α, β ⟩ ⟩ ⊑ W \land \exists U [W = ⟨ U, ⟨ F_{α} (x), F_{β} (y) ⟩] \land ⟨ ⟨ α, α ⟩, β ⟩ ⋢ W \land ⟨ α, ⟨ β, β ⟩ ⟩ ⋢ W . \end{array}$ □

Although we see that $T (L_{BT})$ has some expressive power, it is not clear to us whether all computable subsets of H are existentially definable in $T (L_{BT})$ . Problem 26.
Consider the function $ν : H \to H$ that maps a binary tree x to the binary tree $⊥^{m}$ where m is the number of nodes in x. Is the set ${⟨ x, y ⟩ \in H : ν (x) = y ⟩}$ existentially definable in $T (L_{BT})$ ?

4.2. Term substitution grammars

We modify regular binary tree grammars to get grammars where we can easily keep track of the rules used in a derivation. Recall that $u ⊥ v$ means that u and v are incomparable with respect to the subtree relation ⊑.

Definition 27.
A Term Substitution Grammar $G : = α \to β_{1} | β_{2} | \dots | β_{n}$ is a finite list of rules $α \to β_{k}$ where $α, β_{k} \in H$ and: (1) $α ⊑ β_{k}$ and $β_{k} ⋢ α$ for all $k \in {1, 2, \dots, n}$ , (2) if $i \neq j$ , then $β_{i} ⊥ β_{j}$ , (3) there exists $γ \in H$ such that $γ ⊥ α$ and $γ ⊥ β_{k}$ for all k. We write $s ⇉_{G} t$ if there exists $k \in {1, \dots, n}$ such that $t = s [α \mapsto β_{k}]$ . We denote by $⇉_{G}^{}$ the reflexive transitive closure of the relation $⇉_{G}$ .

We give an example, a representation of natural numbers different from that in Section 3.
Example 28.
We define a one-to-one map $υ : N \to H$ by recursion: $υ (0) = ⊥$ and $υ (n + 1) = ⟨ υ (n), υ (n) ⟩$ . Choose a binary tree α of height at least three. Consider the one-rule term substitution grammar $G : = α \to ⟨ α, α ⟩$ . Let $L (G) = {t \in H : α ⇉_{G}^{} t}$ . Then, $x \in υ (N)$ if and only if there exists $y \in L (G)$ such that $x = y [α \mapsto ⊥]$ .

As mentioned, we are interested in keeping track of the rules used in a derivation. We define the key relation and show that it is existentially definable. Definition 29.
Let $G : = α \to β_{1} | β_{2} | \dots | β_{n}$ be a term substitution grammar. Consider an alphabet $B = {b_{1}, b_{2}, \dots, b_{n}}$ . Let $B^{}$ denote the set of all finite strings over B, including the empty string ε. Given $γ, θ \in H$ , we define the map $σ_{θ}^{γ} : B^{} \to H$ by $\begin{matrix} σ_{θ}^{γ} (w) = \{\begin{array}{ll} ⟨ γ, θ ⟩ & if w = ε \\ ⟨ σ_{θ}^{γ} (ε), ⟨ γ^{3 + k}, γ^{3 + k} ⟩ ⟩ & if w = b_{k} \\ σ_{θ}^{γ} (w_{0}) [σ_{θ}^{γ} (ε) \mapsto σ_{θ}^{γ} (w_{1})] & if w = w_{0} w_{1} and w_{0} \in B . \end{array} \end{matrix}$ We define the relation $⊩_{G}$ by recursion: for $γ, θ \in H$ such that $γ ⋢ θ$ , $⋀_{k = 1}^{n} β_{k} ⋢ θ$ , $γ ⊥ α$ and $γ ⊥ β_{k}$ for all $k \in {1, \dots, n}$
$σ_{θ}^{γ} (ε) ⊩_{G} θ$

$σ_{θ}^{γ} (w b_{k}) ⊩_{G} t$ if and only if $σ_{θ}^{γ} (w) ⊩_{G} t [β_{k} \mapsto α]$ and $β_{k} ⊑ t$ .

Theorem 30.
Let G be a regular term substitution grammar. Then, the relation $⊩_{G}$ is existentially definable in $T (L_{BT})$ .
Proof.
Let $G : = α \to β_{1} | β_{2} | \dots | β_{n}$ . Let H denote the regular binary tree grammar with the same rules as G. Assume $⋀_{k = 1}^{n} β_{k} ⋢ θ$ . Choose $γ \in H$ such that $γ ⋢ θ$ , $γ ⊥ α$ and $γ ⊥ β_{k}$ for all $k \in {1, 2, \dots, n}$ . By Lemma 22, $W (H, γ)$ is existentially definable (γ is a parameter). If $θ ⇉_{G}^{} t$ , then there exists an element of $W (H, γ)$ that witnesses this, but the converse is not true. We need to identify those elements of $W (H, γ)$ that witness a $⇉_{G}^{}$ -derivation. An element of $W (H, γ)$ is of the form $W = ⟨ γ, W_{k}, W_{k - 1}, \dots, W_{1} ⟩$ and witnesses a derivation $W_{k} \Rightarrow_{G}^{} W_{1}$ . To simplify matters, we identify $W (H, γ)$ with the subset of those W’s such that $W_{k} \neq W_{k - 1}$ , i.e., $⟨ γ, W_{k}, W_{k} ⟩ ⋢ W$ . The binary tree W fails to witness $W_{k} ⇉_{G}^{} W_{1}$ if there is some $W_{ℓ}$ and distinct indexes i, j such that $β_{i} ⊑ W_{ℓ}$ and $β_{j} ⊑ W_{ℓ}$ . We define another regular binary tree grammar K that allows us to pick out those elements of $W (H, γ)$ that witness a $⇉_{G}^{}$ -derivation.

Let $σ_{θ}^{γ} : B^{} \to H$ be as in Definition 29. We know that $σ_{θ}^{γ} (B^{})$ is existentially definable. We identify $b_{k}$ with $⟨ γ^{3 + k}, γ^{3 + k} ⟩$ . Let $F_{k} (x) = x [α \mapsto b_{k}]$ . Let $\hat{W} (H, γ)$ consist of those $V \in H$ such that $\begin{matrix} \exists W \in W (H, γ) [V = W [β_{1} \mapsto F_{1} (β_{1}), β_{2} \mapsto F_{2} (β_{2}), \dots, β_{n} \mapsto F_{n} (β_{n})]] . \end{matrix}$ From $W = ⟨ γ, W_{k}, W_{k - 1}, \dots, W_{1} ⟩$ we get $V = ⟨ γ, V_{k}, V_{k - 1}, \dots, V_{1} ⟩$ where we obtain $V_{ℓ}$ from $W_{ℓ}$ by replacing an occurrence of α contained in an occurrence of $β_{j}$ with $b_{j}$ . We define a regular binary tree grammar K such that if $X \in σ_{θ}^{γ} ({b_{1}, b_{2}, \dots, b_{n}}^{})$ , then $X \Rightarrow_{K}^{} V$ if and only if $W_{k} ⇉_{G}^{} W_{1}$ , which then shows that $⊩_{G}$ is existentially definable. We let K be defined by the rules $\begin{matrix} b_{i} \to F_{i} (β_{j}) for i, j \in {1, 2,, \dots, n} . \end{matrix}$ Assume we have $W_{ℓ}$ and two distinct indexes i, j such that $β_{i} ⊑ W_{ℓ}$ and $β_{j} ⊑ W_{ℓ}$ . Then, $b_{i} ⊑ V_{ℓ}$ and $b_{j} ⊑ V_{ℓ}$ . Now, for $X \in σ_{θ}^{γ} ({b_{1}, b_{2}, \dots, b_{n}}^{})$ , we cannot have $X \Rightarrow_{K}^{} V$ since each $F_{i} (β_{j})$ has exactly one $b_{r}$ as a subtree. □

4.3. Undecidability proof

We now have everything in place to encode computations by Turing machines. We show that given a Turing machine M, we can find an existential formula $ϕ_{M} (x)$ with one free variable x such that M halts on input w if and only if the sentence $ϕ_{M} (τ (w))$ is true in $T (L_{BT})$ , the map τ is any suitable encoding of the input alphabet of the Turing machine.

The reduction is straightforward. Given a Turing machine M, we capture computations by M with a modified version of Post‘s Correspondence Problem. First, we extend the input alphabet with fresh letters, including a special letter e. We construct a finite set of pairs (dominos) of finite strings in the extended alphabet $(a_{1}, b_{1})$ , $(a_{2}, b_{2}), \dots, (a_{n}, b_{n})$ . Then, M halts on input w if and only if there exists a nonempty finite sequence $i_{1}, \dots, i_{m}$ of indices such that $\begin{matrix} (*) & e a_{i_{1}} a_{i_{2}} \dots a_{i_{m}} = e w e b_{i_{1}} b_{i_{2}} \dots b_{i_{m}} . \end{matrix}$ The construction can be found in Sipser [13] [Section 5.2] and the details are therefore omitted. We simply illustrate the idea by showing how we can compute the exponential function $x \mapsto 2^{x}$ this way. We consider the alphabet $Γ = {0, 1, a, b, c, d}$ . Given two natural numbers k and m, we consider the following dominos $\begin{matrix} [\frac{a}{a b 0^{k} c 1^{m}}] [\frac{b 0}{b}] [\frac{0}{0}] [\frac{c}{c}] [\frac{11}{1}] [\frac{b c 1 d}{d}] \end{matrix}$ Then, $2^{k} = m$ if and only we can list the dominos starting with the first domino and with repetition allowed such that we get a configuration where the string on top matches the bottom string. The first domino encodes the input. The second encodes subtraction by one. The fifth domino encodes division by two.

All that remains is to show how encode a finite sequence $(a_{1}, b_{1})$ , $(a_{2}, b_{2}), \dots, (a_{n}, b_{n})$ as a pair of term substitution grammars. For simplicity, we assume the $a_{i}$ ’s and $b_{j}$ ’s are binary string. Consider a sequence $C = (c_{1}, c_{2}, \dots, c_{n})$ of nonempty binary strings. Since the $c_{i}$ ’s may overlap, we associate each $c_{i}$ with a strings over a larger alphabet ${0, 1, μ_{1}, μ_{2}, \dots, μ_{n}}$ where the letter $μ_{i}$ represents the last letter of $c_{i}$ . Assume for example $c_{1} = 110$ , $c_{2} = 011$ and $c_{3} = 1010$ . Then, we associate the binary string $c_{2} c_{1} c_{3}$ with the string $01 μ_{2} 11 μ_{1} 101 μ_{3}$ . Let $τ : {0, 1, μ_{0}, μ_{1}, \dots, μ_{n}}^{*} \to H$ be the encoding in Example 19. We let $\begin{matrix} \frac{c_{i}}{C} \equiv τ (w_{i} μ_{i}) where c_{i} = w_{i} d \land w_{i} \in {0, 1}^{*} \land d \in {0, 1} . \end{matrix}$ We associate $c_{i_{1}} c_{i_{2}} \dots c_{i_{m}}$ with a finite binary tree in $τ ({0, 1, μ_{0}, μ_{1}, \dots, μ_{n}}^{*})$ as follows $\begin{matrix} \frac{c_{i_{1}} c_{i_{2}} \dots c_{i_{m}}}{C} \equiv τ (w_{i_{1}} μ_{i_{1}} w_{i_{2}} μ_{i_{2}} \dots w_{i_{m}} μ_{i_{m}}) . \end{matrix}$ We let $\frac{ε}{C} \equiv τ (ε)$ . See Fig. 10 for a visualization of $\frac{c_{1}}{C}$ , $\frac{c_{2}}{C}$ , $\frac{c_{1} c_{2}}{C}$ , $\frac{c_{2} c_{1}}{C}$ when $c_{1} = 110$ and $c_{2} = 011$ .

Figure 10.

Visualization of $\frac{c_{1}}{C}$ , $\frac{c_{2}}{C}$ , $\frac{c_{1} c_{2}}{C}$ , $\frac{c_{2} c_{1}}{C}$ , respectively, when $c_{1} = 110$ , $c_{2} = 011$ . The binary tree α is as in Example 19.

Everything is now in place. We associate the sequence $A = (a_{1}, a_{2}, \dots, a_{n})$ with the term substitution grammar $\begin{matrix} A : = \frac{ε}{A} \to \frac{a_{1}}{A} | \frac{a_{2}}{A} | \dots | \frac{a_{n}}{A} \end{matrix}$ and the sequence $B = (b_{1}, b_{2}, \dots, b_{n})$ with the term substitution grammar $\begin{matrix} B : = \frac{ε}{B} \to \frac{b_{1}}{B} | \frac{b_{2}}{B} | \dots | \frac{b_{n}}{B} . \end{matrix}$ We fix $γ \in H$ that is incomparable with $τ (ε)$ and $τ (d)$ for each $d \in {0, 1, μ_{0}, μ_{1}, \dots, μ_{n}}$ . Using the notation of Definition 29, (*) is equivalent to truth in $T (L_{BT})$ of the existential sentence which states that:

there exist $θ_{1}$ , s and u such that $\begin{matrix} θ_{1} = τ (μ_{0}) \land s \in σ_{θ_{1}}^{γ} ({b_{1}, b_{2}, \dots, b_{n}}^{*}) \land s ⊩_{A} u \end{matrix}$

there exist $θ_{2}$ , t and v such that $\begin{matrix} θ_{2} = τ (e w μ_{0}) \land t \in σ_{θ_{2}}^{γ} ({b_{1}, b_{2}, \dots, b_{n}}^{*}) \land t ⊩_{B} v \end{matrix}$

$t = s [σ_{θ_{1}}^{γ} (ε) \mapsto σ_{θ_{2}}^{γ} (ε)]$

with $d_{i}$ denoting the last letter of $a_{i}$ and $g_{j}$ denoting the last letter of $b_{j}$ . $\begin{matrix} u [μ_{0} \mapsto e, μ_{1} \mapsto d_{1}, \dots, μ_{n} \mapsto d_{n}] = v [μ_{0} \mapsto e, μ_{1} \mapsto g_{1}, \dots, μ_{n} \mapsto g_{n}] . \end{matrix}$

Clauses (I) and (II) encode two strings

e a_{i_{1}} a_{i_{2}} \dots a_{i_{m}}

and

e w e b_{j_{1}} b_{j_{2}} \dots b_{j_{k}}

, respectively. Clause (III) tells us that

k = m

and

i_{ℓ} = j_{ℓ}

for all

ℓ \in {1, 2, \dots, m}

. Before we can test for the equality in (*), we need to replace the

μ_{i}

‘s with what they actually represent. This is what (IV) does.

References

J.R.

Büchi and

Senger , Definability in the existential theory of concatenation and undecidable extensions of this theory, Mathematical Logic Quarterly34(4) (1988), 337–342. doi:10.1002/malq.19880340410.

J.H.

Conway , Unpredictable iterations, in: Number Theory Conference, Univ. of Colorado, Boulder, 1972, pp. 49–52.

Davis , Hilbert’s tenth problem is unsolvable, The American Mathematical Monthly80(3) (1973), 233–269. doi:10.1080/00029890.1973.11993265.

Davis ,

Putnam and

Robinson , The decision problem for exponential Diophantine equations, Annals of Mathematics74(3) (1961), 425–436. doi:10.2307/1970289.

Gecseg and

Steinby , Tree languages, in: Handbook of Formal Languages, Vol. 3 Beyond Words,

Rozenberg and

Salomaa , eds, Springer, Berlin Heidelberg, 1997, pp. 1–68, Chapter 1.

Hodges , Model Theory, Cambridge University Press, 1993.

Karhumäki ,

Mignosi and

Plandowski , The expressibility of languages and relations by word equations, Journal of the ACM47(3) (2000), 483–505. doi:10.1145/337244.337255.

Kristiansen and

Murwanashyaka , First-order concatenation theory with bounded quantifiers, Archive for Mathematical Logic60(1–2) (2021), 77–104. doi:10.1007/s00153-020-00735-6.

S.A.

Kurtz and

Simon , The undecidability of the generalized Collatz problem, in: TAMC 2007-Theory and Applications of Models of Computation,

J.Y.

Cai ,

S.B.

Cooper and

Zhu , eds, Lecture Notes in Computer Science, Vol. 4484, 2007, pp. 542–553. doi:10.1007/978-3-540-72504-6_49.

10.

G.S.

Makanin , The problem of solvability of equations in a free semigroup, Mathematics of the USSR. Sbornik32(2) (1977), 129–198. doi:10.1070/SM1977v032n02ABEH002376.

11.

Murwanashyaka , Hilbert’s tenth problem for term algebras with a substitution operator, in: Revolutions and Revelations in Computability, CiE 2022,

Berger ,

J.N.Y.

Franklin ,

Manea and

Pauly , eds, Lecture Notes in Computer Science, Vol. 13359, 2022, pp. 196–207. doi:10.1007/978-3-031-08740-0_17.

12.

E.L.

Post , A variant of a recursively unsolvable problem, Bulletin (new Series) of the American Mathematical Society52(4) (1946), 264–268. doi:10.1090/S0002-9904-1946-08555-9.

13.

Sipser , Introduction to the Theory of Computation, 3rd edn, Cengage Learning, 2013.

14.

Venkataraman , Decidability of the purely existential fragment of the theory of term algebras, Journal of the ACM34(2) (1987), 492–510. doi:10.1145/23005.24037.

Hilbert’s tenth problem for term algebras with a substitution operator

Abstract

Keywords

1. Introduction

Open Problem 1. Construct a Turing reduction of the existential theory of T ( L BT ) to the existential theory of ( N , 0 , 1 , + , × ) which does not rely on the solution to Hilbert’s 10th Problem. 2. Bounded quantifiers

Open Problem 2. Is the fragment Σ 1 , 0 , 1 T ( L T ) undecidable? 2.1. Finite sets of finite binary trees

Proposition 9. Let A , B and C be first-order structures in finite languages. If A is ∃-interpretable in B and B is ∃-interpretable in C , then A is ∃-interpretable in C . If A is ∃-interpretable in B and Th ∃ ( B ) is decidable, then Th ∃ ( A ) is decidable. 3.1. Numbers

Open Problem 18. Is every computably enumerable subset of H existentially definable in T ( L BT ) ? 4.1. Regular tree grammars

References

Open Problem 1.
Construct a Turing reduction of the existential theory of $T (L_{BT})$ to the existential theory of $(N, 0, 1, +, \times)$ which does not rely on the solution to Hilbert’s 10th Problem.

2. Bounded quantifiers

Open Problem 2.
Is the fragment $Σ_{1, 0, 1}^{T (L_{T})}$ undecidable?

2.1. Finite sets of finite binary trees

Open Problem 18.
Is every computably enumerable subset of H existentially definable in $T (L_{BT})$ ?

4.1. Regular tree grammars