Some new results in monadic second-order arithmetic

Abstract

Let σ be a signature and $A$ a σ-structure with domain $N$ . Say that a monadic second-order σ-formula is $Π_{n}^{1}$ iff it has the form $\forall X_{1} \exists X_{2} \forall X_{3} \dots X_{n} ψ$ with $X_{1}, \dots, X_{n}$ set variables and ψ containing no set quantifiers. Consider the following properties:

for each positive integer n, the set of $Π_{n}^{1}$ -σ-sentences true in $A$ is $Π_{n}^{1}$ -complete;

for each positive integer n, if a set of natural numbers is $Π_{n}^{1}$ -definable (i.e. by a $Π_{n}^{1}$ -formula) in the standard model of arithmetic and closed under automorphisms of $A$ , then it is $Π_{n}^{1}$ -definable in $A$ .

We use ∣ and ⊥ to denote the divisibility relation and the coprimeness relation respectively. Given a prime p, let

{bc}_{p}

be the function which maps every pair

(x, y)

of natural numbers into

(\binom{x + y}{x}) mod p

. In this article we prove:

⟨ N, ∣ ⟩

and all

⟨ N, {bc}_{p}, = ⟩

have both

ACP

and

ADP

; in effect, even

⟨ N, ⊥ ⟩

has

ACP

. Notice – these results readily generalise to arbitrary arithmetical expansions of the corresponding structures, provided that the extended signature is finite.

Keywords

Monadic second-order arithmetic complexity definability

1. Introduction

Let $f_{0}, f_{1}, \dots$ be a list of all computable functions and $R_{0}, R_{1}, \dots$ be a list of all computable relations. Then the standard model $N$ of arithmetic expands to $T : = ⟨ N, f_{0}, f_{1}, \dots, R_{0}, R_{1}, \dots ⟩ .$ The paper is devoted to monadic second-order properties of natural reducts of $T$ – which are considerably less studied than first-order properties of such structures (see [2, 6, 10] for further information and references). More precisely, we shall concentrate on issues of computability and definability.

For each $n > 0$ , consider the class $A_{n}$ of $Π_{n}^{1}$ -sets. From now on assume all $Π_{n}^{1}$ -formulas are monadic and contain exactly n set quantifiers.

Folklore.
For any $A \subseteq N$ and $n > 0$ , the following hold:
$A \in A_{n}$ iff A is definable in $N$ by a $Π_{n}^{1}$ -formula;

$A \in A_{n}$ iff A is m-reducible to the set of $Π_{n}^{1}$ -sentences true in $N$ .

This fact is closely connected with the fundamental properties we shall be interested in, i.e. $ACP$ and $ADP$ . Given the reduct $A$ of $T$ to a finite signature, they say (for all A and n):
one can replace $N$ in (ii) by $A$ ;

whenever A is closed under automorphisms of $A$ , one can replace $N$ in (i) by $A$ .
The article illustrates an attractive general approach to proving that certain structures have $ACP$ and/or $ADP$ (actually the first steps towards our present framework were already taken in [14]) – these properties can be employed for establishing complexity lower bounds in the context of the analytical hierarchy, for example, cf. [15].

Certain naturally arising reducts of $T$ have gained much popularity in logic and computer science over the last several generations. The research programme focuses on
issues of computability and definability in the first-order setting, and

issues of computability and definability in the monadic second-order setting.
Substantial progress has been made in (1). While (2) remain largely unstudied. One of the most important exceptions deals with the successor function $s$ :
Theorem (from [5]).

The monadic second-order theory of $⟨ N, s, = ⟩$ is decidable.

The same holds for $⟨ N, < ⟩$ . And the analogous result for the binary tree can be found in [12]. The situation with + points towards degrees of undecidability, however.

Theorem (from [7]).

The set of $Π_{1}^{1}$ -sentences true in $⟨ N, +, = ⟩$ is $Π_{1}^{1}$ -complete.

Halpern’s proof, being designed for this special complexity result, could not shed much light on $ADP$ or $ACP$ with $n > 1$ . Luckily a very different line of reasoning leads to

Theorem (from [14]).

$⟨ N, +, = ⟩$ has $ACP$ and $ADP$ . $⟨ N, \times, = ⟩$ has $ACP$ .

As expected, we shall analyse (2) with the help of (1) – keeping in mind that $N$ can be identified with every arithmetical structure in which + and × are first-order definable (but for applications to $ACP$ and the like, interpretability should suffice). The reader may consult [10] for a collection of such structures. In particular those discovered by A. Bès, I. Korec and D. Richard will play a role.

A few words about the reducts we shall be concerned with are in order. Structures associated with the divisibility relation ∣ and the coprimeness relation ⊥ have achieved quite a lot of attention since [13]. Intuitively, our theorems below may be contrasted with the well-known decidability results obtained in [5, 12]. Modular Pascal’s triangles were intensively explored during the 1990s. We list them as $B_{2}, B_{3}, \dots,$ where for any $k ⩾ 2$ , $B_{k}$ denotes the algebra whose only operation is given by ${bc}_{k} (x, y) = (\binom{x + y}{x}) mod k .$ As a matter of fact, it will turn out that – in view of some earlier contributions of A. Bès, I. Korec and the author – we only need to investigate every $⟨ N, {bc}_{p}, = ⟩$ with p prime.

Among other things, we shall answer the questions emerging from [14]: $\begin{array}{l} Does ⟨ N, \times, = ⟩ have ADP ? Does ⟨ N, ∣ ⟩ have ACP and ADP ? \end{array}$

The rest of the paper is organised as follows. Section 2 consists of preliminary material. In Section 3 we develop our basic ideas into an efficient tool, which is used to prove $⟨ N, ∣ ⟩$ has $ACP$ and $ADP$ . Section 4 presents a slight variant of our technique, yielding $ACP$ and $ADP$ for each $⟨ N, {bc}_{p}, = ⟩$ . In Section 5 we show how one can derive sharper complexity results by exploiting the notion of (first-order) interpretability instead of that of definability (but the price paid for this is that such arguments do not take $ADP$ into account): even $⟨ N, ⊥ ⟩$ has $ACP$ . We conclude the article with a few general comments.

2. Preliminaries

In monadic second-order arithmetic we have

individual variables $x, y, z, \dots$ (intended to range over $N$ ) and

set variables $X, Y, Z, \dots$ (intended to range over all subsets of $N$ ).

Accordingly we distinguish between individual and set quantifiers:

\forall x, \exists x, \forall y, \exists y, \forall z, \exists z, \dots and \forall X, \exists X, \forall Y, \exists Y, \forall Z, \exists Z, \dots .

Let σ be a signature, i.e. a collection of constant, function and predicate symbols, each of which is assigned an arity. Monadic second-order σ-formulas are built up from first-order atomic σ-formulas and expressions of the form

t \in X

with t a (first-order) σ-term and X a set variable using connective symbols and quantifiers in the customary way. In effect, it will sometimes be convenient to treat unary predicate symbols as set variables.

A monadic second-order σ-formula is $Π_{n}^{1}$ , where $n \in N ∖ {0}$ , iff it has the form $\underset{n - 1 alternations}{\underset{︸}{\forall X_{1} \exists X_{2} \forall X_{3} \dots X_{n}}} ψ$ with $X_{1}, \dots, X_{n}$ set variables and ψ containing no set quantifiers. Still, throughout this text ‘definable’ and ‘formula’ mean ‘first-order definable’ and ‘first-order formula’ respectively, unless otherwise indicated (like in ‘defined by a $Π_{n}^{1}$ -formula’ or ‘ $Π_{n}^{1}$ -definable’).

For a σ-structure $A$ with domain $N$ , we bring in the following notation: $\begin{array}{l} Def (A) : = the collection of all sets definable in A, \\ Aut (A) : = the collection of all automorphisms of A, \\ {Th}^{1} (A) : = the first-order theory of A, and \\ {Th}^{*} (A) : = the monadic second-order theory of A . \end{array}$ We shall be concerned with two fundamental properties:

for every $n \in N ∖ {0}$ , the set of $Π_{n}^{1}$ -σ-sentences true in $A$ is $Π_{n}^{1}$ -complete;

for every $n \in N ∖ {0}$ , if $A \subseteq N$ is $Π_{n}^{1}$ -definable in $N : = ⟨ N, 0, s, +, \times, = ⟩$ and closed under $Aut (A)$ , then A is $Π_{n}^{1}$ -definable in $A$ .

Intuitively, the letters

A

C

D

and

P

stand for ‘analytical’ (which reminds us of the analytical hierarchy), ‘complexity’, ‘definability’ and ‘property’. For example,

\begin{array}{l} ⟨ N, +, = ⟩ and ⟨ N, \times, = ⟩ have ACP and ⟨ N, +, = ⟩ has ADP, \end{array}

as was shown in [14].

We also use the binary predicate symbols ∣ and ⊥ to denote the divisibility relation and the coprimeness relation respectively – in other words, for any ${x, y} \subset N$ , $\begin{array}{l} x ∣ y ⟺ x divides y and \\ x ⊥ y ⟺ x and y have no common prime divisor . \end{array}$ Given $k ⩾ 2$ , let ${bc}_{k}$ be the function which maps each $(x, y) \in N \times N$ into the remainder of integer division of the binomial coefficient $(\binom{x + y}{x})$ by k, i.e. $(\binom{x + y}{x}) mod k = \frac{(x + y)!}{x! \times y!} mod k .$ In the present work we shall concentrate on the structures $N : = ⟨ N, ∣ ⟩, C : = ⟨ N, ⊥ ⟩ and B_{k} : = ⟨ N, {bc}_{k}, = ⟩,$ where $k ⩾ 2$ . And primes will play a key role in our study. For $n \in N ∖ {0}$ , define $P_{n} : = {p^{n} ∣ p is a prime} and ⊏_{n} : = the restriction of < to ⋃_{i = 1}^{n} P_{n} .$ Occasionally we write $P$ instead of $P_{1}$ . In the limit, one gets $\overline{P} : = ⋃_{n = 1}^{\infty} P_{n} and ⊏ : = ⋃_{n = 1}^{\infty} ⊏_{n} .$ Several results are worth mentioning here:

if $k \notin \overline{P}$ , then + and × are definable in $B_{k}$ (see [8]);

if $k \in \overline{P} ∖ P$ , then + is definable in $B_{k}$ and ${Th}^{1} (B_{k})$ is decidable (see [1]).

Thus for every

k \notin P

B_{k}

has

ACP

and

ADP

. On the other hand, if

p \in P

, then

${Th}^{1} (B_{p})$ is decidable (see [9]) and

neither + nor × is definable in $B_{p}$ (see [3]).

Further, we shall employ the relational signature $σ_{⋆} : = {=^{2}, Γ_{0}^{1}, Γ_{s}^{2}, Γ_{+}^{3}, Γ_{\times}^{3}},$ paying special attention to the conjunction $A_{⋆}$ of the following $σ_{⋆}$ -sentences:

$\forall x (x = x)$ ;

$\forall x \forall y (x = y \to y = x)$ ;

$\forall x \forall y \forall u ((x = y \land y = u) \to x = u)$ ;

$\forall x \forall y \forall u \forall v ((x = u \land y = v \land Γ_{s} (x, y)) \to Γ_{s} (u, v))$ ;

$\forall x \forall y \forall z \forall u \forall v \forall w ((x = u \land y = v \land z = w \land Γ_{+} (x, y, z)) \to Γ_{+} (u, v, w))$ ;

$\forall x \forall y \forall z \forall u \forall v \forall w ((x = u \land y = v \land z = w \land Γ_{\times} (x, y, z)) \to Γ_{\times} (u, v, w))$ ;

$\forall x \forall y (\exists u \exists v (Γ_{s} (x, u) \land Γ_{s} (y, v) \land u = v) \to x = y)$ ;

$\forall x \forall y \forall u ((Γ_{0} (x) \land Γ_{s} (y, u)) \to \neg x = u)$ ;

$\forall x (Γ_{0} (x) \lor \exists y \exists u (Γ_{s} (y, u) \land x = u))$ ;

$\forall x \forall y (Γ_{0} (y) \to \exists u (Γ_{+} (x, y, u) \land u = x))$ ;

$\forall x \forall y \forall z \forall u \forall v \forall w ((Γ_{s} (y, z) \land Γ_{+} (x, z, u) \land Γ_{+} (x, y, v) \land Γ_{s} (v, w)) \to u = w)$ ;

$\forall x \forall y (Γ_{0} (y) \to \exists u (Γ_{\times} (x, y, u) \land u = y))$ ;

$\forall x \forall y \forall z \forall u \forall v \forall w ((Γ_{s} (y, z) \land Γ_{\times} (x, z, u) \land Γ_{\times} (x, y, v) \land Γ_{+} (v, x, w)) \to u = w)$ ;

$\exists x (Γ_{0} (x) \land \forall y (Γ_{0} (y) \leftrightarrow y = x))$ ;

$\forall x \exists y Γ_{s} (x, y) \land \forall x \forall y \forall u ((Γ_{s} (x, y) \land Γ_{s} (x, u)) \to y = u)$ ;

$\forall x \forall y \exists u Γ_{+} (x, y, u) \land \forall x \forall y \forall u \forall v ((Γ_{+} (x, y, u) \land Γ_{+} (x, y, v)) \to u = v)$ ;

$\forall x \forall y \exists u Γ_{\times} (x, y, u) \land \forall x \forall y \forall u \forall v ((Γ_{\times} (x, y, u) \land Γ_{\times} (x, y, v)) \to u = v)$ .

Certainly

A_{⋆}

is a reformulation of Robinson arithmetic. Henceforth we identify

N

with its

σ_{⋆}

-version. So in particular, the

σ_{⋆}

-formula

γ_{<} (x, y) : = \exists u (Γ_{+} (x, u, y) \land \neg Γ_{0} (u))

expresses < in

N

. For convenience, we also introduce

N^{'} : = N ∖ {0}, F : = {k! ∣ k \in N} and σ^{†} : = σ \cup {U^{1}},

where U is a fresh unary predicate symbol. Remark that Sections 3–5 involve some ‘local notation’ as well: for instance, σ stands for the signature in question and (♯) for a very special list of formulas in

σ^{†}

(possibly augmented by individual constants).

3. The case of the natural lattice

Assume $σ = {∣^{2}}$ . Throughout this section we shall be concerned with the σ-structure $N$ .

Clearly the constants 0 and 1, the equality relation =, the sets $P$ and $\overline{P}$ , the coprimeness relation ⊥ and the least common multiple operation $lcm$ are all definable in $N$ : $\begin{array}{l} x = 0 ⟺ \neg x ∣ x, \\ x = 1 ⟺ \forall y (x ∣ y), \\ x = y ⟺ (x = 0 \land y = 0) \lor (x ∣ y \land y ∣ x), \\ x \in P ⟺ \neg x = 0 \land \neg x = 1 \land \forall y (y ∣ x \to (y = 1 \lor y = x)), \\ x \in \overline{P} ⟺ \exists y (y \in P \land y ∣ x \land \forall u ((u \in P \land u ∣ x) \to u = y)), \\ x ⊥ y ⟺ \neg \exists u (\neg u = 1 \land u ∣ x \land u ∣ y) and \\ z = lcm (x, y) ⟺ x ∣ z \land y ∣ z \land \forall u ((x ∣ u \land y ∣ u) \to z ∣ u) . \end{array}$ Furthermore, each $P_{n}$ belongs to $Def (N)$ as well – because $x \in P_{n} ⟺ x \in \overline{P} \land \exists y_{0} \dots \exists y_{n} (y_{n} = x \land ⋀_{i = 0}^{n - 1} (y_{i} | y_{i + 1} \land \neg y_{i + 1} | y_{i}) \land \forall u (u | x \to (⋁_{i = 0}^{n} u = y_{i}))) .$ In what follows $x = y$ , $x = 0$ , etc. in σ- and $σ^{†}$ -formulas should be understood merely as convenient abbreviations. Also we shall exploit two specific σ-formulas: $x ≺ y : = x ∣ y \land \neg x ∣ y and x ⋖ y : = x ≺ y \land \neg \exists u (x ≺ u \land u ≺ y)$ – so the latter can be viewed as a covering relation for the former.

Proposition 3.1.
For every $n \in N^{'}$ , $⊏_{n}$ is definable in $⟨ N, F ⟩$ .
Proof.
Since $x < y$ is equivalent to $x! ≺ y!$ for any x and y in $N^{'}$ , it suffices to establish the definability of a (partial) function which maps each $k \in P_{1} \cup \dots \cup P_{n}$ into $k!$ .

Provided that $x \in N^{'}$ and $y \in P$ , the σ-formula $φ_{1} (x, y, z) : = x ⋖ z \land \forall u ((u \in \overline{P} \land u ∣ x \land y ∣ u) \to \exists v (v \in \overline{P} \land v ∣ z \land u ⋖ v))$ says ‘ $z = x \times y$ ’, and more generally, for every $k \in {1, \dots, n}$ , the σ-formula $\begin{array}{l} φ_{k} (x, y, z) : = & \exists v_{0} \dots \exists v_{k} (v_{0} = x \land v_{k} = z \land ⋀_{i = 0}^{k - 1} v_{i} ⋖ v_{i + 1}) \\ \land \forall u ((u \in \overline{P} \land u ∣ x \land y ∣ u) \to \exists v_{0} \dots \exists v_{k} (v_{k} \in \overline{P} \land v_{k} ∣ z \land v_{0} = u \land ⋀_{i = 0}^{k - 1} v_{i} ⋖ v_{i + 1})) \end{array}$ says ‘ $z = x \times y^{k}$ ’. On the other hand, assuming $x \in F ∖ {1}$ , the $σ^{'}$ -formula $φ_{} (x, y) : = U (y) \land y ≺ x \land \forall u ((U (u) \land u ≺ x) \to u ∣ y)$ expresses that y is the predecessor of x in $F$ , i.e. $y = (k - 1)!$ whenever $x = k!$ . Obviously, for all $x \in P_{1} \cup \dots \cup P_{n}$ we have $y = x! ⟺ y belongs to F, y is not equal to 1, and the predecessor of y multiplied by x equals y;$ thus one can define in $⟨ N, F ⟩$ a function with the required property by an appropriate $σ^{'}$ -formula using $φ_{1}$ , …, $φ_{n}$ and $φ_{}$ . The rest is straightforward. □

As was proved in [4], + and × are definable in $⟨ N, ∣, ⊏ ⟩ .$ Aiming to obtain the same for some expansion of $N$ to $σ^{†}$ , let $K$ denote ${p^{k} \times q^{m} ∣ {p, q} \subset P, p < q, {k, m} \subset N^{'}, p^{k} < q^{m} and \max {k, m} ⩾ 4} .$ Then $E : = F \cup K$ encodes ⊏ in the following sense.
Proposition 3.2.
⊏ is definable in $⟨ N, E ⟩$ .
Proof.
First observe that $\begin{array}{l} A : = {(p^{k}, q^{m}) ∣ {p, q} \subset P, p \neq q, {k, m} \subset N^{'} and \max {k, m} ⩾ 4} and \\ B : = {k \times m ∣ (k, m) \in A} \end{array}$ are defined in $N$ by the σ-formulas $\begin{array}{l} φ_{A} (x, y) : = x \in \overline{P} \land y \in \overline{P} \land x ⊥ y \land \exists u (u \in P_{4} \land (u ∣ x \lor u ∣ y)) and \\ φ_{B} (x) : = \exists u \exists v (φ_{A} (u, v) \land x = lcm (u, v)) . \end{array}$ Consequently – since $F \subset N ∖ B$ and $K \subset B$ – the $σ^{†}$ -formulas $φ_{F} (x) : = x \in U \land \neg φ_{B} (x) and φ_{K} (x) : = x \in U \land φ_{B} (x)$ define $F$ and $K$ , respectively, in $⟨ N, E ⟩$ . So in particular – remembering Proposition 3.1 – $⊏_{3}$ is expressible. Hence $\begin{array}{l} φ_{⊏} (x, y) : = x \in \overline{P} \land y \in & \overline{P} \land x ≺ y \lor x ⊏_{3} y \\ \lor (φ_{A} (x, y) \land \exists u \exists v (u ∣ x \land v ∣ y \land u ⊏_{1} v \land φ_{K} (lcm (x, y)))) \\ \lor (φ_{A} (x, y) \land \exists u \exists v (u ∣ x \land v ∣ y \land v ⊏_{1} u \land \neg φ_{K} (lcm (x, y)))) \end{array}$ defines ⊏ in $⟨ N, E ⟩$ , as can be readily checked. □

Combining this with the result of A. Bès and D. Richard, we immediately get
Corollary 3.3.
+ and × are definable in $⟨ N, E ⟩$ .

We are now ready to establish
Theorem 3.4.
$N$ has $ACP$ .
Proof.
Pick an infinite $A \subseteq N ∖ E$ from $Def (N)$ – for instance, $A : = P_{2}$ – and let $θ (x)$ be a σ-formula defining A in $N$ . By Corollary 3.3, we can find $σ^{†}$ -formulas $φ_{=} (x, y), φ_{0} (x), φ_{s} (x, y), φ_{+} (x, y, z) and φ_{\times} (x, y, z)$ (♯) which define =, 0, $s$ , + and ×, respectively, in $⟨ N, E ⟩$ . Consider the modified list $ψ_{=} (x, y), ψ_{0} (x), ψ_{s} (x, y), ψ_{+} (x, y, z) and ψ_{\times} (x, y, z)$ (♮) obtained from (♯) by replacing each occurrence of the form $u \in U$ by $u \in U \land \neg θ (u)$ . Thus (♮) plays the role of (♯) for every $σ^{†}$ -structure $⟨ N, E \cup B ⟩$ with $B \subseteq A$ .

Next, given a second-order $σ_{⋆}$ -formula φ, take $τ φ : = the result of replacing =, Γ_{0}, Γ_{s}, Γ_{+} and Γ_{\times} in φ by ψ_{=}, ψ_{0}, ψ_{s}, ψ_{+} and ψ_{\times} respectively .$ Some expansions of $N$ to $σ^{†}$ can induce, via (♮), non-standard models even when $τ A_{⋆}$ is satisfied. To avoid this, it suffices to ensure that $ψ_{s}$ behaves in the standard manner, i.e. $ψ_{s} always expresses a relation isomorphic to ⟨ N, s ⟩ .$ Choose a $σ_{⋆}$ -formula $ϕ (x, y)$ defining the obvious isomorphism between $⟨ N, s ⟩ and ⟨ {2^{k} ∣ k \in N^{'}}, ⋖ ⟩$ (viewed as ${Γ_{s}}$ -structures) – viz. the numerical function $y = 2^{x}$ – in $N$ . Let $χ_{st}$ denote the conjunction of the following $σ^{†}$ -sentences:
$\forall x \forall u \forall v ((τ ϕ (x, u) \land τ ϕ (x, v)) \to ψ_{=} (u, v))$ ;

$\forall x \forall y \forall u ((τ ϕ (x, u) \land τ ϕ (y, u)) \to ψ_{=} (x, y))$ ;

$\exists x (x \in P \land \forall y \exists v (v \in \overline{P} \land x ∣ v \land τ ϕ (y, v)) \land \forall v ((v \in \overline{P} \land x ∣ v) \to \exists y τ ϕ (y, v)))$ ;

$\forall x \forall y \exists u \exists v (τ ϕ (x, u) \land τ ϕ (y, v) \land (ψ_{s} (x, y) \leftrightarrow u ⋖ v))$ .
With any expansion $A$ of $N$ to $σ^{†}$ we associate, via (♮), the $σ_{⋆}$ -structure $A_{⋆}$ with domain $N$ , such that $\begin{matrix} A_{⋆} ⊨ k = m \Leftrightarrow A ⊨ ψ_{=} (k, m), A_{⋆} ⊨ Γ_{0} (k) \Leftrightarrow A ⊨ ψ_{0} (k), etc. \end{matrix}$ Clearly if $A$ satisfies $τ A_{⋆} \land χ_{st}$ , then $A_{⋆}$ is isomorphic (although not necessarily identical) to $N$ . Fix a $σ_{⋆}$ -formula $ϑ (x, y)$ defining in $N$ some function f mapping $N$ one-one onto A – and let $χ_{tr}$ be the conjunction of the following $σ^{†}$ -sentences:
$\forall x \forall u \forall v ((τ ϑ (x, u) \land τ ϑ (x, v)) \to ψ_{=} (u, v))$ ;

$\forall x \forall y \forall u ((τ ϑ (x, u) \land τ ϑ (y, u)) \to ψ_{=} (x, y))$ ;

$\forall x \exists u (θ (u) \land τ ϑ (x, u)) \land \forall u (θ (u) \to \exists x τ ϑ (x, u))$ .
So $A ⊨ χ_{tr}$ implies that $τ ϑ$ expresses a one-one function from $N$ onto A in $A$ .

Further, given a second-order $σ_{⋆}$ -formula φ, take $ι φ : = the result of replacing each u \in U in φ by \exists v (ϑ (u, v) \land v \in U),$ where v is the first variable not occurring in φ. Then for an arbitrary $Π_{n}^{1}$ - $σ_{⋆}$ -sentence $\forall X_{1} \exists X_{2} \dots ψ (X_{1}, X_{2}, \dots)$ with $X_{1} = U$ and ψ containing no second-order quantifiers – by the properties of f and ι – we have $\begin{array}{l} N ⊨ \forall U \exists X_{2} \dots ψ & ⟺ N ⊨ \forall U \exists X_{2} \dots ι ψ (f (U), X_{2}, \dots) \\ ⟺ N ⊨ \forall U \exists X_{2} \dots ι ψ (U \cap A, X_{2}, \dots) \\ ⟺ N ⊨ \forall U \exists X_{2} \dots ι ψ (U, X_{2}, \dots) . \end{array}$ Observe that by the construction of (♮), for all subsets C and D of $N$ , $C ∖ A = D ∖ A ⟹ the associated σ_{⋆} -structures {⟨ N, C ⟩}_{⋆} and {⟨ N, D ⟩}_{⋆} coincide .$ Hence we can use $x \in U \land θ (x)$ as a free unary predicate without changing the inner layer of the isomorphic copy of $N$ in question. It is straightforward to verify now that $N ⊨ \forall U \exists X_{2} \dots ι ψ (U, X_{2}, \dots) ⟺ N ⊨ \forall U \exists X_{2} \dots ((τ A_{⋆} \land χ_{st} \land χ_{tr}) \to τ ι ψ (U, X_{2}, \dots)),$ which completes the argument. □

Note that whenever a set is second-order definable in $N$ (without parameters), it has to be closed under $Aut (N)$ – hence we cannot express, for instance, $x \in A$ with A a proper non-empty subset of $P$ . However, a minor modification of the above argument yields
Theorem 3.5.
$N$ has $ADP$ .
Proof.
Let $γ_{Dvs} (x, y)$ denote the $σ_{⋆}$ -formula $\exists u (Γ_{\times} (x, u, y) \land \neg Γ_{0} (x))$ . The idea is simply to add the $σ^{†}$ -sentence
$\forall x \forall y (x ∣ y \leftrightarrow τ γ_{Dvs} (x, y))$
to the conjunction of (S1)–(S4), thus updating $χ_{st}$ to $χ_{st}^{}$ . Suppose $A ⊨ τ A_{⋆} \land χ_{st}^{}$ . Then there exists an isomorphism f between $A_{⋆}$ and $N$ . For any ${k, m} \subseteq N$ , we have $\begin{array}{l} k divides m & \overset{(S5)}{⟺} A ⊨ τ γ_{Dvs} (k, m) ⟺ A_{⋆} ⊨ γ_{Dvs} (k, m) \\ ⟺ N ⊨ γ_{Dvs} (f (k), f (m)) ⟺ f (k) divides f (m) . \end{array}$ So $f \in Aut (N)$ . Consequently, for each natural number k and each $Π_{n}^{1}$ - $σ_{⋆}$ -formula $\forall X_{1} \exists X_{2} \dots ψ (X_{1}, X_{2}, \dots, x)$ with $X_{1} = U$ and ψ containing no set quantifiers, $\begin{array}{l} N ⊨ \forall U \exists X_{2} \dots ψ (U, X_{2}, \dots, f (k)) for all f \in Aut (N) \\ ⟺ f (N) ⊨ \forall U \exists X_{2} \dots ψ (U, X_{2}, \dots, k) for all f \in Aut (N) \\ ⟺ C ⊨ \forall U \exists X_{2} \dots ((τ A_{⋆} \land χ_{st}^{} \land χ_{tr}) \to τ ι ψ (U, X_{2}, \dots, k)), \end{array}$ where $f (N)$ is the $σ_{⋆}$ -structure with domain $N$ , such that $N ⊨ R (i_{1}, \dots, i_{m}) ⟺ f (N) ⊨ R (f (i_{1}), \dots, (i_{m}))$ for any m-ary $R \in σ_{⋆}$ and $(i_{1}, \dots, i_{m}) \in N^{m}$ (certainly $N$ and $f (N)$ are isomorphic). □

Given $n \in N^{'}$ , it is not hard to construct $Π_{n}^{1}$ -complete sets closed under $Aut (N)$ . But if one wants to turn $Aut (N)$ into ${id}$ , where $id$ is the identity function, some extra information has to be incorporated into the structure. For example, consider $N_{\circ} : = ⟨ N, ∣, ⊏_{1} ⟩$ in the signature $σ^{‡} : = σ \cup {⊏_{1}^{2}}$ . Since, as was proved earlier in [11], the first-order theory of $⟨ N, =, \times, ⊏_{1} ⟩$ is decidable, so is ${Th}^{1} (N_{\circ})$ . Furthermore, one easily checks that each non-trivial $f \in Aut (N)$ permutes at least two primes; thus $Aut (N_{\circ}) = {id}$ .
Corollary 3.6.
Let* $n \in N^{'}$ . Every $Π_{n}^{1}$ -set is $Π_{n}^{1}$ -definable in $N_{\circ}$ .

Assume the intended interpretation of the binary predicate symbol ∥ is ${(k, m) \in N \times N ∣ k ∣ m or m ∣ k} .$ We finish with a relatively simple yet interesting fact about $D : = ⟨ N, ∥ ⟩$ . Proposition 3.7.
$N$ and $D$ are interdefinable.
Proof.
It is a routine matter to verify that $\begin{array}{l} x = 0 & ⟺ \neg x ∥ x, \\ x = 1 & ⟺ \forall u (x ∥ u), \\ x = y & ⟺ \forall u (x ∥ u \leftrightarrow y ∥ u), \\ x \in \overline{P} & ⟺ \neg x = 0 \land \neg x = 1 \land \exists u (\neg x = u \land x ∥ u \land \forall v (u ∥ v \to x ∥ v)) \end{array}$ and the compound formula $\begin{array}{l} x = & 1 \lor (x \in \overline{P} \land y \in \overline{P} \land \forall u (y ∥ u \to x ∥ u)) \\ \lor (\neg x = 0 \land \neg x \in \overline{P} \land \neg y = 1 \land \neg y \in \overline{P} \land \forall u ((u \in \overline{P} \land x ∥ u) \to y ∥ u)) \end{array}$ (where $x \in \overline{P}$ , $x = 0$ , etc. are understood as abbreviations) defines $x ∣ y$ in $D$ .

The other direction is trivial. □

4. The case of modular Pascal’s triangles

As has been observed earlier, we need only consider $B_{n}$ with n prime, assuming $σ = {{bc}_{n}^{2}, =^{2}}$ .

Fix $p \in P$ . By a p-ary expansion of $x \in N$ we mean any $(x_{0}, \dots, x_{k}) \in {0, 1, \dots, p - 1}^{k}$ for which $\sum_{i = 0}^{k} x_{i} \times p^{i} = x$ , written $x = {[x_{k}, \dots, x_{0}]}_{p}$ . Of course, each number has infinitely many p-ary expansions: $x = {[x_{k}, \dots, x_{0}]}_{p} ⟺ x = {[0, \dots, 0, x_{k}, \dots, x_{0}]}_{p} .$ So given ${x, y} \subset N$ , we can always find expansions of x and y with the same length. Now for $x = {[x_{k}, \dots, x_{0}]}_{p}$ and $y = {[y_{k}, \dots, y_{0}]}_{p}$ , let $x ⋐ y ⟺ x \neq y and x_{i} ⩽ y_{i} for all i \in {0, \dots, k} .$ Intuitively, ⋐ is a sort of ‘multiset inclusion’. In effect, I. Korec [8] showed that:

the relation ⋐ and the set $G_{p} : = {p^{k} ∣ k \in N^{'}}$ belong to $Def (B_{p})$ ;

+ and × are definable in $⟨ B_{2}, Sq ⟩$ where $Sq$ denotes ${k^{2} ∣ k \in N}$ .

Furthernore, as was proved in [3], (ii) holds for each

⟨ B_{p}, Sq ⟩

For our present purposes, it is useful to introduce $A_{p} : = {p + p^{2 + k} ∣ k \in N} .$ Certainly there exists a σ-formula $θ_{p} (x, v)$ such that for every $m \in N$ , $m \in A_{p} ⟺ B_{p} ⊨ θ_{p} (m, p)$ (think of v as a parameter). To be more precise, define $θ_{p} (x, v) : = v ⋐ x \land \exists u (u \in G_{p} \land \neg u = v \land u ⋐ x \land \neg \exists z (v ⋐ z \land u ⋐ z \land z ⋐ x)) .$ We also employ the signature $σ^{‡} : = σ^{†} \cup {c}$ including an extra constant symbol c whose role is similar to that of v in the above discussion. Accordingly we write $⟨ B_{p}, B, k ⟩$ for the $σ^{‡}$ -structure obtained from $B_{p}$ by interpreting U as B and c as k.

Theorem 4.1.
$B_{p}$ has $ACP$ .
Proof.
Take $A : = A_{p}$ – evidently $A \cap Sq = \emptyset$ – and let $θ (x)$ be the formula $θ_{p} (x, c)$ . By analogy with the proof of Theorem 3.4, we obtain the new (♯), (♮) and τ.

To avoid “non-standard” expansions of $B_{p}$ to $σ^{‡}$ , it suffices to ensure that $τ γ_{<} always expresses a relation embeddable in ⋐$ – because the latter is well-founded. Choose a $σ_{⋆}$ -formula $ϕ (x, y)$ defining the numerical function $y = \sum_{k = 1}^{x} p^{k}$ – which embeds $⟨ N, < ⟩$ into $⟨ N, ⋐ ⟩$ , obviously – in $N$ . Next, let ρ be a σ-formula defining ⋐ in $B_{p}$ , and denote by $χ_{st}$ the conjunction of:
$\forall x \forall u \forall v ((τ ϕ (x, u) \land τ ϕ (x, v)) \to u = v)$ ;

$\forall x \forall y \forall u ((τ ϕ (x, u) \land τ ϕ (y, u)) \to x = y)$ ;

$\forall x \exists u τ ϕ (x, u)$ ;

$\forall x \forall y \exists u \exists v (τ ϕ (x, u) \land τ ϕ (y, v) \land (τ γ_{<} (x, y) \leftrightarrow ρ (u, v)))$ .
As before, with every expansion $A$ of $B_{p}$ to $σ^{‡}$ we associate, via (♮), the $σ_{⋆}$ -structure $A_{⋆}$ . Suppose $A ⊨ τ A_{⋆} \land χ_{st}$ but $A_{⋆}$ is not isomorphic to $N$ . Then there exists a chain $k_{0}, k_{1}, \dots$ of pairwise distinct natural numbers with the property: $A_{⋆} ⊨ γ_{<} (k_{m + 1}, k_{m}) – and hence A ⊨ τ γ_{<} (k_{m + 1}, k_{m}) – for each m \in N .$ Thus we get an infinite descending chain in $⟨ N, ⋐ ⟩$ , contradicting the well-foundedness of ⋐. Let ϑ, $χ_{tr}$ and ι be as in the proof of Theorem 3.4. We have the following:
$⟨ B_{p}, B, k ⟩ ⊨ χ_{tr}$ implies that $τ ϑ$ defines a one-one function from $N$ onto $Θ_{k} : = {m \in N ∣ B_{p} ⊨ θ_{p} (m, k)}$ (which may or may not be identical to A) in $⟨ B_{p}, B, k ⟩$ ;

for all $k \in N$ , $C \subseteq N$ and $D \subseteq N$ , $C ∖ Θ_{k} = D ∖ Θ_{k} ⟹ the associated σ_{⋆} -structures {⟨ B_{p}, C, k ⟩}_{⋆} and {⟨ B_{p}, D, k ⟩}_{⋆} coincide.$
Viewing c as an individual variable, it is now straightforward to check that $N ⊨ \forall U \exists X_{2} \dots ψ (U, X_{2}, \dots) ⟺ B_{p} ⊨ \forall U \exists X_{2} \dots \forall c ((τ A_{⋆} \land χ_{st} \land χ_{tr}) \to τ ι ψ (U, X_{2}, \dots)),$ where ψ contains no second-order quantifiers. □

As a matter of fact, for $p \neq 2$ , one can also take $A : = {2 \times p^{k} ∣ k \in N}$ which is directly definable in $B_{p}$ (without parameters). Unfortunately, this will not work for $p = 2$ . Theorem 4.2.
$B_{p}$ has $ADP$ .
Proof.
Fix a $σ_{⋆}$ -formula $γ_{p} (x, y, z)$ defining ${bc}_{p}$ in $N$ , and add the $σ^{‡}$ -sentence
$\forall x \forall y \forall z ({bc}_{p} (x, y) = z \leftrightarrow τ γ_{p} (x, y, z))$
to the conjunction of (S1)–(S4), i.e. $χ_{st}$ . Now proceed as in the proof of Theorem 3.5. □

5. About the coprimeness relation

Assume $σ = {⊥^{2}}$ . Of course, we shall focus our attention on the σ-structure $C$ .

Obviously 0, 1 and $\overline{P}$ are definable in $C$ – because $\begin{array}{l} x = 1 & ⟺ \forall u (u ⊥ x), \\ x = 0 & ⟺ \forall u (u ⊥ x \to u = 1) and \\ x \in \overline{P} & ⟺ \neg x = 1 \land \forall u \forall v ((\neg u ⊥ x \land \neg v ⊥ x) \to \neg u ⊥ v) . \end{array}$

By analogy with the previous section, we also introduce $σ^{‡} : = σ^{†} \cup {c}$ .

As was proved in [4], $N$ is first-order interpretable in $N_{∙} : = ⟨ N, ⊥, ⊏_{2} ⟩,$ and A. Bès and D. Richard employed an infinite collection of primes with the usual ordering to play the role of $N$ here. Naturally the same holds for the substructure $S$ of $N_{∙}$ with domain $S : = {0} \cup {k \in N ∣ 2 ⊥ k and 3 ⊥ k} .$

For our present purposes, consider the function $h : S \to N$ given by $h (k) : = \{\begin{matrix} 2 \times k & if k \in P_{2} \cap S, \\ 3 \times k & if k \in (\overline{P} ∖ (P \cup P_{2})) \cap S, \\ k & otherwise. \end{matrix}$ Certainly $S$ is isomorphic to $H = ⟨ H, ⊥^{h}, ⊏_{2}^{h} ⟩$ where $\begin{array}{l} H : = h (S), ⊥^{h} : = {(h (k), h (m)) ∣ {k, m} \subset S and k ⊥ m} and \\ ⊏_{2}^{h} : = {(h (k), h (m)) ∣ {k, m} \subset S and k ⊏_{2} m} . \end{array}$ Notice that $h (x) = x$ for all $x \in P \cap S$ . Let $X$ , $Y$ and $O$ denote $\begin{array}{l} h (P_{2} \cap S), h ((\overline{P} ∖ (P \cup P_{2})) \cap S) and \\ {p^{k} \times q^{m} ∣ {p, q} \subset P, 3 < p < q, {k, m} \subset N^{'} and p^{2} > q} \end{array}$ respectively. Then $D : = P \cup (F ∖ {6, 24}) \cup X \cup Y \cup O$ encodes $H$ as follows.

Proposition 5.1.
H, $⊥^{h}$ and $⊏_{2}^{h}$ are definable in $⟨ C, D, 2 ⟩$ .
Proof.
First observe that $B : = {p^{k} \times q^{m} ∣ {p, q} \subset P, p \neq q and {k, m} \subset N^{'}}$ is defined in $C$ by the σ-formula $φ_{B} (x) : = \neg x = 0 \land \exists u \exists v (u \in \overline{P} \land v \in \overline{P} \land u ⊥ v \land \neg u ⊥ x \land \neg v ⊥ x \land \neg \exists w (w \in \overline{P} \land w ⊥ u \land w ⊥ v \land \neg w ⊥ x)) .$ Consequently – since $D \cap \overline{P} = P, D \cap B = X \cup Y \cup O and D \cap (N ∖ (B \cup \overline{P})) = F ∖ {2, 6, 24}$ – the $σ^{‡}$ -formulas $\begin{array}{l} φ_{P} (x) : = x \in U \land x \in \overline{P}, \\ φ_{2} (x) : = φ_{P} (x) \land \neg x ⊥ c, \\ φ_{X} (x) : = x \in U \land φ_{B} (x) \land \neg x ⊥ c, \\ φ_{3} (x) : = φ_{P} (x) \land \forall u (φ_{X} (u) \to x ⊥ u), \\ φ_{Y} (x) : = x \in U \land φ_{B} (x) \land \exists u (φ_{3} (u) \land \neg x ⊥ u), \\ φ_{O} (x) : = x \in U \land φ_{B} (x) \land x ⊥ c \land \exists u (φ_{3} (u) \land x ⊥ u) and \\ φ_{\tilde{F}} (x) : = x \in U \land \neg φ_{B} (x) \land \neg x \in \overline{P} \end{array}$ define $P$ , 2, $X$ , 3, $Y$ , $O$ and $F ∖ {2, 6, 24}$ , respectively, in $⟨ C, D, 2 ⟩$ . Hence $φ_{H} (x) : = φ_{X} (x) \lor φ_{Y} (x) \lor ((φ_{P} (x) \lor \neg x \in \overline{P}) \land x ⊥ c \land \exists u (φ_{3} (u) \land x ⊥ u))$ expresses H. Now $(x, y) \in ⊥^{h}$ can be written as $φ_{H} (x) \land φ_{H} (y) \land \neg \exists u (φ_{P} (u) \land \neg φ_{2} (u) \land \neg φ_{3} (u) \land \neg u ⊥ x \land \neg u ⊥ y) .$ Further, for any ${x, y} \subset P$ , $x < y ⟺ x divides y! but not vice versa;$ so the restriction of < to $P \cap S$ is expressed by $\begin{array}{l} φ_{{\tilde{⊏}}_{1}} (x, y) : = & \neg φ_{2} (x) \land \neg φ_{3} (x) \land φ_{P} (x) \land φ_{P} (y) \\ \land \forall u (({\tilde{φ}}_{F} (u) \land \neg y ⊥ u) \to \neg x ⊥ u) \land \exists v ({\tilde{φ}}_{F} (v) \land \neg x ⊥ v \land y ⊥ v) . \end{array}$ Finally, one easily sees that $\begin{array}{l} φ_{{\tilde{⊏}}_{1}} (x, y) \lor (φ_{P} (x) \land φ_{X} (y) \land \exists v (φ_{P} (v) \land \neg v ⊥ y \land φ_{{\tilde{⊏}}_{1}} (x, v))) \\ \lor (φ_{X} (x) \land φ_{X} (y) \land \exists u \exists v (φ_{P} (u) \land φ_{P} (v) \land \neg u ⊥ x \land \neg v ⊥ y \land φ_{{\tilde{⊏}}_{1}} (u, v))) \\ \lor (φ_{X} (x) \land φ_{P} (y) \land \exists u (φ_{P} (u) \land \neg u ⊥ x \land φ_{{\tilde{⊏}}_{1}} (u, y)) \land \neg \exists z (φ_{O} (z) \land \neg x ⊥ z \land \neg y ⊥ z)) \\ \lor (φ_{P} (x) \land φ_{X} (y) \land \exists v (φ_{P} (v) \land \neg v ⊥ y \land φ_{{\tilde{⊏}}_{1}} (v, x)) \land \exists z (φ_{O} (z) \land \neg x ⊥ z \land \neg y ⊥ z)) \end{array}$ defines $⊏_{2}^{h}$ in $⟨ C, D, 2 ⟩$ . □

This time we immediately get
Corollary 5.2.
$N$ is first-order interpretable in $⟨ C, D, 2 ⟩$ .

In other words, there exist $σ^{‡}$ -formulas $φ_{N} (x), φ_{=} (x, y), φ_{0} (x), φ_{s} (x, y), φ_{+} (x, y, z) and φ_{\times} (x, y, z)$ (♯) satisfying the following requirements:
$M : = {k \in N ∣ ⟨ C, D, 2 ⟩ ⊨ φ_{N} (k)}$ is non-empty;

$N$ is isomorphic to the $σ_{⋆}$ -structure $M$ with domain M, such that

for any k-ary $Γ_{R} \in σ_{⋆}$ and $(m_{1}, \dots, m_{k}) \in M^{k}$ , $M ⊨ Γ_{R} (m_{1}, \dots, m_{k}) ⟺ ⟨ C, D, 2 ⟩ ⊨ φ_{R} (m_{1}, \dots, m_{k}),$

and for all $(m_{1}, m_{2}) \in M \times M$ , $M ⊨ m_{1} = m_{2} ⟺ ⟨ C, D, 2 ⟩ ⊨ φ_{=} (m_{1}, m_{2}) .$
Moreover, as has been already remarked, we can (and will) assume that $M \subseteq P ∖ {2, 3} and γ_{<} defines in M the restriction of < to M .$

In conclusion, we establish
Theorem 5.3.
$C$ has $ACP$ .
Proof.
Consider the σ-formula $α (x, y) : = \neg x = 0 \land \neg x = 1 \land \neg x \in \overline{P} \land \neg φ_{B} (x) \land x ⊥ y$ with $φ_{B}$ taken from the proof of Proposition 5.1. Evidently $A : = {k \in N ∣ C ⊨ α (k, 2)}$ is a subset of $N ∖ D$ , so let $θ (x)$ be $α (x, c)$ . Accordingly we shall exploit the list $ψ_{N} (x), ψ_{=} (x, y), ψ_{0} (x), ψ_{s} (x, y), ψ_{+} (x, y, z) and ψ_{\times} (x, y, z)$ (♮) obtained from (♯) by replacing each occurrence of the form $u \in U$ by $u \in U \land \neg θ (u)$ .

Next, given a second-order formula φ in $σ_{⋆}$ , take $\begin{array}{l} τ φ : = & the result of replacing =, Γ_{0}, Γ_{s}, Γ_{+} and Γ_{\times} in φ by ψ_{=}, ψ_{0}, ψ_{s}, ψ_{+} and ψ_{\times} \\ respectively, and then relativising all individual quantifiers to ψ_{N} . \end{array}$ Similarly to before, with any expansion $A$ of $C$ to $σ^{‡}$ we associate, using (♮), the $σ_{⋆}$ -structure $A_{⋆}$ with domain ${k \in N ∣ A ⊨ ψ_{N} (k)}$ , such that $\begin{array}{l} A_{⋆} ⊨ k = m \Leftrightarrow A ⊨ ψ_{=} (k, m), A_{⋆} ⊨ Γ_{0} (k) \Leftrightarrow A ⊨ ψ_{0} (k), etc. \end{array}$ For $A$ satisfying $τ A_{⋆}$ we have $A_{⋆} is isomorphic to N ⟺ γ_{<} defines a well-founded relation in A_{⋆} .$ By construction, $ψ_{N} (x) \land ψ_{N} (y) \land τ γ_{<} (x, y)$ defines in $⟨ C, D, 2 ⟩$ the restriction of < to M. Also we know that $F ∖ {2, 6, 24}$ is defined in $⟨ C, D, 2 ⟩$ by the $σ^{‡}$ -formula $ϕ (x) : = x \in U \land \neg θ (x) \land \neg φ_{B} (x) \land \neg x \in \overline{P} .$ Let $χ_{st}$ denote the conjunction of the following $σ^{†}$ -sentences:
$\forall x (ψ_{N} (x) \to (x \in \overline{P} \land x ⊥ c))$ ;

$\forall x \forall y ((ψ_{N} (x) \land ψ_{N} (y) \land τ γ_{<} (x, y)) \to x ⊥ y)$ ;

$\forall x (x \in \overline{P} \to \exists y (\neg y = 0 \land ϕ (y) \land \neg x ⊥ y))$ ;

$\forall x \forall u \forall v ((ϕ (x) \land ψ_{N} (u) \land ψ_{N} (v) \land \neg x ⊥ v \land τ γ_{<} (u, v)) \to \neg x ⊥ u)$ .
Suppose $A ⊨ τ A_{⋆} \land χ_{st}$ but the relation defined in $A_{⋆}$ by $γ_{<}$ is not well-founded, i.e. there exists a chain $k_{0}, k_{1}, \dots$ of pairwise coprime elements of $\overline{P}$ with the property: $A ⊨ ψ_{N} (k_{m}) \land ψ_{N} (k_{m + 1}) \land τ γ_{<} (k_{m + 1}, k_{m}) for all m \in N .$ Applying (S3), we find a positive integer K such that $A ⊨ ϕ (K)$ and $\neg k_{0} ⊥ K$ . Thus by (S4), K has infinitely many prime divisors, a contradiction.

Now consider an arbitrary $Π_{n}^{1}$ - $σ_{⋆}$ -sentence $\forall X_{1} \exists X_{2} \dots ψ (X_{1}, X_{2}, \dots)$ with $X_{1} = U$ and ψ containing no set quantifiers. To get $ψ_{}$ from ψ:
replace each $u \in U$ in ψ by $\exists x \exists y (Γ_{s} (u, x) \land Γ_{s} (x, y) \land \exists v (v \in U \land θ (v) \land \neg y ⊥ v))$ where v is the first individual variable not occurring in ψ – remember the requirements (S1)–(S2);

then replace =, $Γ_{0}$ , $Γ_{s}$ , $Γ_{+}$ and $Γ_{\times}$ by $ψ_{=}$ , $ψ_{0}$ , $ψ_{s}$ , $ψ_{+}$ and $ψ_{\times}$ respectively;

finally, relativise all individual quantifiers except those containing v to $ψ_{N}$ .
It is straightforward to check that $N ⊨ \forall U \exists X_{2} \dots ψ ⟺ C ⊨ \forall U \exists X_{2} \dots \forall c ((τ A_{⋆} \land χ_{st}) \to ψ_{})$ (here we view c as an individual variable). □

Still, the argument does not show how to get an analogue of Theorem 3.5.
6. Further discussion

Certainly we come to

Hypothesis.

$C$ has $ADP$ .

It would be nice to prove this by adapting the method developed in the article, because

the above results readily generalise to all possible arithmetical expansions of the corresponding structures (provided that the extended signature is finite).

For example we can pass from $N$ to $⟨ N, \times, = ⟩$ in Theorem 3.5. On a technical note – there are two simple modifications worth mentioning:

in $ADP$ one can take $N^{k}$ (with $k ⩾ 1$ ) instead of $N$ ;

in $ADP$ one can add to both $N$ and $A$ parameters for sets closed under $Aut (A)$ .

Of course, perfectly analogous arguments apply here. Obviously all translations in the proofs are computable (so in particular

{Th}^{*} (N)

is many-one equivalent to

{Th}^{*} (C)

, as well as to each

{Th}^{*} (B_{k})

Footnotes

Acknowledgements

I would like to thank Alexis Bès for his useful comments. The research was supported by the Alexander von Humboldt Foundation.

References

[1]

Bès, On Pascal triangles modulo a prime power, Annals of Pure and Applied Logic 89 (1997), 17–35.

[2]

Bès, A survey of arithmetical definability, in: A Tribute to Maurice Boffa,

Crabbé et al., eds, Société Mathématique de Belgique, 2002, pp. 1–54.

[3]

Bès and

Korec, Definability within structures related to Pascal’s triangle modulo an integer, Fundamenta Mathematicae 156 (1998), 111–129.

[4]

Bès and

Richard, Undecidable extensions of Skolem arithmetic, Journal of Symbolic Logic 63 (1998), 379–401.

[5]

J.R.

Büchi, On a decision method in restricted second order arithmetic, in: Logic, Methodology and Philosophy of Science,

Nagel,

Suppes and

Tarski, eds, Stanford University Press, 1962, pp. 1–11.

[6]

Cegielski, Definability, decidability, complexity, Annals of Mathematics and Artificial Intelligence 16 (1996), 311–341.

[7]

J.Y.

Halpern, Presburger arithmetic with unary predicates is

Π_{1}^{1}

complete, Journal of Symbolic Logic 56 (1991), 637–642.

[8]

Korec, Definability of arithmetic operations in Pascal triangle modulo an integer divisible by two primes, Grazer Mathematische Berichte 318 (1993), 53–62.

[9]

Korec, Elementary theories of structures containing generalized Pascal triangles modulo a prime, in: Discrete Mathematics and Applications, Blagoevgrad/Predel, 1994,

Shtrakov and

Mirchev, eds, Blagoevgrad, 1995, pp. 91–102.

10.

[10]

Korec, A list of arithmetical structures complete with respect to the first-order definability, Theoretical Computer Science 257 (2001), 115–151.

11.

[11]

Maurin, The theory of integer multiplication with order restricted to primes is decidable, Journal of Symbolic Logic 62 (1997), 123–130.

12.

[12]

M.O.

Rabin, Decidability of second-order theories and automata on infinite trees, Transactions of the American Mathematical Society 141 (1969), 1–35.

13.

[13]

Robinson, Definability and decision problems in arithmetic, Journal of Symbolic Logic 14 (1949), 98–114.

14.

[14]

S.O.

Speranski, A note on definability in fragments of arithmetic with free unary predicates, Archive for Mathematical Logic 52 (2013), 507–516.

15.

[15]

S.O.

Speranski, Quantifying over events in probability logic: an introduction, Mathematical Structures in Computer Science (2015), accepted for publication.