Punctually presented structures I: Closure theorems

Abstract

We study the primitive recursive content of various closure results in algebra and model theory, including the algebraic, the real, and the differential closure theorems. In the case of ordered fields and their real closures, our result settles a question recently raised by Selivanova and Selivanov.

Keywords

Primitive recursion algebraic closure constructive models

1. Introduction

The paper contributes to the study of the primitive recursive content of proofs and processes in algebra, analysis, and infinite combinatorics initiated in [33]. The main idea of such studies is eliminating unbounded search from various abstract algorithms performed on infinite mathematical structures. Abstract Turing computable algorithms are in the core of computable structure theory [6,22,43]. The simple idea of eliminating unbounded search from such abstract algorithms led to many rather technically non-trivial and often unexpected results. For foundations of the theory of primitive recursive (and ‘punctual’) structures, we cite the surveys [5,7,21]. For various recent results related to the present paper, and for further technical background, we cite [9,20,42,50]. We also note that primitive recursive algebra is very closely technically related to polynomial time algebra; see, e.g., [1,3,13,14]. The main definitions in the theory are as follows. An algebraic structure is primitive recursive if its domain is a primitive recursive subset of natural numbers and the operations and relations are represented by primitive recursive functions. This definition can be traced back to Mal’cev [38]. If we replace ‘primitive recursive’ with ‘computable’ throughout the definition, we will obtain the standard notion of a computable structure [6,22]. Kalimullin, Melnikov and Ng [33] suggested to use the following, more restricted notion. Say that a structure is fully primitive recursive or punctual if it is primitive recursive and its domain is the set of all natural numbers (or its initial segment). This seemingly minor variation in the basic definition provided valuable insights into the sub-recursive aspects of algebra and analysis. There has been much research focused on the following fundamental problems:

Describe punctually presented structures in common classes.

Compare different presentations of an algebraic structure.

Investigate the primitive recursive content of classical algebraic results.

For many recent theorems, examples, and non-trivial counter-examples related to these problems see the papers cited above, and also the very recent papers [10,19,27,34,47]. The main theorem of the present paper is related to (a) and (c), but we will also suggest several further results that attack (b). For more results related to (b), we cite the satellite paper [17].

We now discuss the main result of the paper. Recall that every field can be embedded into its algebraic closure, every abelian group is contained in its divisible hull, and every ordered field can be expanded to its real closure. More generally, many natural classes admit a suitable notion of (existential or algebraic) closure. (We shall not attempt to formally define what exactly ‘closure’ means in general since it is a bit too technical. For the purposes of this paper it could be done using prime models of certain theories; for a general abstract definition of a closure see, e.g., [22].) The computability-theoretic content of such algebraic closure results had been studied extensively; e.g., [30,44,49]; for a detailed exposition and a general meta-theorem we cite the book [22]. The study of the primitive recursive content of such results has been initiated by Selivanov and Selivanova [47] who gave a primitive recursive way of embedding a primitive recursive Archimedean ordered field into its primitive recursive real closure (under a mild extra effectiveness condition on the field). The general case was left open. The main goal of the present paper is to give a systematic primitive recursive analysis of primitive recursive closure theorems in algebra. The main result of the paper is the following theorem which, in particular, answers the aforementioned question raised in [47] by Selivanov and Selivanova.

Theorem 1.1.
In each of the following classes, every punctual structure from the class can be punctually embedded into its punctual (existential, algebraic) closure:
Boolean algebras;

fields;

ordered fields;

differential fields of characteristic zero.

In each case, the closure is defined naturally; e.g., it is the ‘smallest’ atomless extension in (1), the algebraic closure in (2), the real closure in (3), and the differential closure in (4). We state the theorem for punctual structures but it also holds for primitive recursive structures in these classes; see Remark 4.3 for an explanation.

We now go over the items of the theorem and discuss the respective class, the closure result, and the techniques used to prove it. We also state several further related results that we prove in the present paper.
1.1. Boolean algebras

The case of Boolean algebras serves mainly as an example. It illustrates how general (Turing) computability compares to punctual computability in the context of calculating existential closures. The respective classical result for Boolean algebras is folklore, and indeed one does not need much effort to construct their existential closure ‘by hand’ without any reference to the model-theoretic techniques. If $B$ is a Boolean algebra, define its existential closure $A (B)$ by replacing every atom of $B$ by a copy of the atomless Boolean algebra. Then $A (B)$ is ‘unique’ and ‘minimal’ over $B$ in the right sense, just as expected from any properly defined closure. (We shall clarify what we mean in the relevant section.) The respective computability-theoretic version of this fact also follows quite easily. The punctual analogy (namely, (1) of Theorem 1.1) is also rather elementary. To illustrate the difference between the punctual and the computable closures we prove the following, certainly less elementary, theorem:

Theorem 1.2.

For a computable Boolean algebra $B$ , $A (B)$ is computably unique over $B$ if, and only if, the atom relation is decidable in $B$ .

For a punctual Boolean algebra $B$ , $A (B)$ has infinitely many punctual copies that are not punctually isomorphic (over $B$ ).

It should be clear that the computable uniqueness of $A (B)$ over $B$ means that any two computable versions of the closure of $B$ are computably isomorphic over $B$ . The punctual uniqueness is defined similarly, but using primitive recursive isomorphisms having primitive recursive inverse. (The formal definitions will be given in the relevant section. We also note that in the proof of Theorem 2.8 that will appear later we will in fact not necessarily require the inverse to be primitive recursive, and thus we will obtain an even more than stated in Theorem 2.8.) The computable clause of the theorem appears to be new; it strongly resembles similar results about computable fields (with operators), abelian groups, and other structures; see [32,44,49]. It follows from Theorem 1.2 that, in the class of computable Boolean algebras, the computable uniqueness of their respective closure is equivalent to 1-decidability of the structure, i.e., the decidability of its ∃-diagram. We cite [2,11] where 1-decidability is studied from the perspective of primitive recursive mathematics. For more about 1-decidable and punctually 1-decidable structures, see the satellite paper [17].

In contrast, the punctual uniqueness of $A (B)$ over $B$ is equivalent to $B$ being the smallest possible structure, the 2-element BA. We therefore conjecture that in the standard natural classes, the punctual uniqueness of the existential closure of M over M tends to imply that M is, in some sense, trivial. We leave the verification of this conjecture in other standard classes as an open problem.

We now discuss fields.
1.2. Fields and ordered fields

It is well-known that every computable field can be computably embedded into its computable algebraic closure; see Rabin [44]. A similar result holds for ordered fields as well; this was established by Ershov [23] and, independently, Madison [37]. In the case of computable fields (without order), the punctual version of Rabin’s theorem is not too different from its original (Turing) computable version. We conjecture that already Rabin’s original proof needs only minor adjustments to give (2) of Theorem 1.1, since it seems Rabin uses only bounded search throughout. However, in the case of ordered fields it is not at all clear whether brute-force methods are sufficient to produce a punctual version of the real closure result. Recently, Selivanov and Selivanova [47] proved a restricted version of Theorem 1.1(3) for primitively recursively Archimedean fields; we omit the definition. The general case was left as an open question; we settle the question in a rather strong sense. More specifically, it follows that we obtain a punctually decidable copy of the closure in each case. That is, the Skolem function is primitive recursive. Primitive recursive Skolem functions have been investigated in, e.g., [2,10,33]. (It is not that hard to see that in (1) we also get a punctually decidable closure; we leave the verification of this to the reader.)

Our proof of (2) and (3) of Theorem 1.1 uses the Henkin construction and the (primitive recursive) quantifier elimination in $ACF$ and $RCF$ , respectively, to construct the closure. It was noted in [7] that the Henkin construction is primitive recursive (in the right sense), but the sketch contained in [7] is actually incomplete. We give a complete and detailed proof in the relevant section, and then we combine the result with the respective quantifier elimination procedure. The idea of using Henkin to produce algebraic and real closures is not new (e.g., Simpson [48]), but the primitive recursive version of this result is new. In particular, we prove much more than stated in (2) and (3) of Theorem 1.1. We note that with some effort (2) and (3) of Theorem 1.1 can be further extended to show that the respective closure results hold in ${PRA}^{2}$ in reverse mathematics; this has been announced in [8]. Some further results about primitive recursive fields can be found in [4,35].

We conjecture that, much in the spirit of Theorem 1.2 for Boolean algebras, effective uniqueness of the closure should perhaps correspond to the field being trivial (in some sense). Our intuition is further supported by the main result of [35]. However, we shall not verify this conjecture in the present paper.

1.3. Differential fields

A differential field [24] is a field $K$ together with a derivation operator $δ : K \to K$ . A differentially closed field is an existentially closed differential field. Robinson and Blum [12,45] gave a first-order axiomatization for differentially closed fields of characteristic zero ( ${DCF}_{0}$ ). It is well-known that every differential field can be isomorphically embedded into a differentially closed field. Specifically, Blum [12] showed that any model $A$ of ${DF}_{0}$ (i.e., any differential field of characteristic zero) has a prime differential closure, that is, ${DCF}_{0} \cup Diag (A)$ has a prime model.

Harrington [30] showed that every computable differential field can be computably embedded into a computable presentation of its differential closure. Differentially closed fields have some further nice computability-theoretic properties including the low property and the (recursion-theoretic) Mal’cev property; see, e.g., [31,41]. The primitive recursive content of Harrington’s result has not yet been investigated.

The Henkin construction alone is no longer enough to produce the punctual version of Harrington’s theorem. To prove (4) of Theorem 1.1 we establish the following analogy of the computable prime model theorem [26,30]:

Theorem 1.3.
Let T be a complete theory with a primitive recursive decision procedure. Then the following are equivalent:
T has a punctually decidable prime model.

T has a prime model and the set of all principal types of T is uniformly punctual.

All terms will be clarified in Section 5 which contains the proof of Theorem 1.3. Assuming the theorem, Theorem 1.1(4) can be derived combining the ideas of Harrington and using some other results from the literature that apparently were not known to Harrington when he published [30].

Finally, we note that Theorem 1.3 and the punctual version of Henkin’s construction could be used to establish the closure theorem for, e.g., Boolean algebras, but it would be an overkill. We conjecture that several other ‘closure’ theorems, such as the already cited earlier computable divisible closure theorem for abelian groups [49], also hold primitively recursively. Some of these closure theorems may require model-theoretic techniques, and some other perhaps can be done directly with the structure avoiding a Henkin-style construction or some other general methods. For instance, we leave open whether the general machinery (the ‘kernel’ theorem) established in [22] can be adjusted to produce primitive recursive ‘closures’.

The rest of the paper is split into several sections, with each section containing enough background about the respective class. The main results stated above will be restated in the relevant sections, and sometimes in a stronger form. However, the reader should have no problem navigating through the paper.
2. Boolean algebras

Let $B$ be a Boolean algebra. (We assume that $0^{B} \neq 1^{B}$ throughout.) We first prove that the following two definitions are equivalent, thus, the notion of ‘closure’ is robust for countable Boolean algebras.

Definition 2.1.
Let $A (B) \supseteq B$ be a minimal atomless superstructure, i.e., the superstructure derived from $B$ by substitution of each of its atoms by an infinite atomless ideal. We call $A (B)$ a deatomisation of $B$ .
Definition 2.2.
Let $A^{} (B) \supseteq B$ be an atompless Boolean algebra such that for any atomless $U \supseteq B$ there is an isomorphic embedding $θ : A^{} (B) \to U$ over $B$ (this means that the embedding is the identity when restricted to $B$ ).
Proposition 2.3.
$A (B)$ satisfies Definition 2.2 . For any $A^{} (B)$ satisfying Definition* 2.2 , $A (B)$ and $A^{} (B)$ are isomorphic over* $B$ .
Proof.
Let us show that $A (B)$ satisfies Definition 2.2. Let $U ⩾ B$ be an atomless superstructure. We construct an isomorphic embedding $θ : A (B) \to U$ . Define $θ (b) = b$ for $b \in B$ . For every $b \in A t (B)$ denote $A_{b} = {x \in A (B) | x ⩽_{A (B)} b}$ and $U_{b} = {x \in U | x ⩽_{U} b}$ . Each of the $A_{b}$ and $U_{b}$ can be viewed as an atomless Boolean algebra. Then there is an isomorphism $θ_{b} : A_{b} \to U_{b}$ . For any $x \in A_{b}$ define $θ (x) = θ_{b} (x)$ . Now we can define θ on the rest of the elements that can be represented as $x = b \lor x_{1} \lor \dots \lor x_{n}$ for some $b \in B$ , $x_{i} ⩽ b_{i}$ , $b_{i} \in A t (B)$ . Define $θ (x) = θ (b) \lor θ (x_{1}) \lor \dots \lor θ (x_{n})$ . By construction, θ is an isomorphic embedding.

Now we prove that for any $A^{} (B)$ there is an isomorphism $φ : A^{} (B) \to A (B)$ . Let $θ : A^{} (B) \to A (B)$ be an isomorphic embedding from Definition 2.2. Consider $x \in A^{} (B)$ and let $y = θ (x) \in A (B)$ . Then there exist elements $\begin{matrix} b, y_{0}, \dots, y_{n}, b_{1}, \dots, b_{n} \end{matrix}$ such that $b \in B$ , $b_{i} \in A t (B)$ , $y_{i} <_{A (B)} b_{i}$ and $y = b \lor y_{0} \lor \dots \lor y_{n}$ . We show that $b ⩽_{A^{} (B)} x$ . Suppose $b ≰_{A^{} (B)} x$ . Then $x \neq b \lor x$ . Since θ is an isomorphic embedding then $y = θ (x) \neq θ (b \lor x) = θ (b) \lor θ (x) = b \lor y = y$ . Contradiction. Then $b ⩽_{A^{} (B)} x$ . Let $x^{'} = x ∖ b$ . Since $y_{1} \lor \dots \lor y_{n} < b_{1} \lor \dots \lor b_{n}$ , then $x_{A^{} (B)}^{'} < b_{1} \lor \dots \lor b_{n}$ and $x^{'} = (x^{'} \land b_{1}) \lor \dots \lor (x^{'} \land b_{n})$ . Thus, every $x \in A^{} (B)$ can be presented as $x = b \lor x_{1} \lor \dots \lor x_{n}$ where $b \in B$ , $x_{i} <_{A^{} (B)} b_{i}$ for some $b_{i} \in A t (B)$ .

Let $A_{b}^{} = {x | x \in A^{} (B) & x ⩽_{A^{} (B)} b}$ and $A_{b} = {x | x \in A (B) & x ⩽_{A (B)} b}$ for $b \in A t (B)$ . Then $A_{b}^{}$ and $A_{b}$ are atomless Boolean algebras and there are isomorphisms $φ_{b} : A_{b}^{} \to A_{b}$ . Define $φ (x) = b \lor φ_{b_{1}} (x_{1}) \lor \dots \lor φ_{b_{n}} (x_{n})$ for $x = b \lor x_{1} \lor \dots \lor x_{n}$ where $b \in B$ , $x_{i} <_{A^{} (B)} b_{i} \in A t (B)$ . □

For a given computable Boolean algebra $B$ , we call a pair $(A (B), ψ)$ a computable deatomisation of $B$ if $A (B)$ is a computable atomless Boolean algebra satisfying Definition 2.1 and $ψ : B \to A (B)$ is a computable isomorphic embedding. (Strictly speaking, we should’ve used $A (ψ (B))$ here since $ψ (B)$ does not have to be computable in $A (ψ (B))$ .) We call a pair $(A (B), ψ)$ a punctual deatomisation of a punctual $B$ if $A (B)$ is punctual and $ψ : B \to A (B)$ is a primitive recursive isomorphic embedding. Theorem 2.4.
Let $B$ be a computable Boolean algebra. Then $B$ can be computably embedded into a computable copy of $A (B)$ .
Proof.
Since $B$ is computable, we can effectively build a binary generating tree $T_{B}$ for $B$ in the sense of [25]. (Every node in the tree is a non-zero element of the Boolean algebra, the root of 1, and x and y are children of z if $x \lor y = z$ and $x \land y = 0$ .)

Simultaneously we construct a binary tree $T_{A}$ without dead ends and a computable isomorphic embedding $ψ_{T} : T_{B} \to T_{A}$ . Then any element $b \in B$ can be introduced as $b = b_{0} \lor \dots \lor b_{n}$ for some $b_{i} \in T_{B}$ , $i ⩽ n$ . Let $A$ be a Boolean algebra generated by $T_{A}$ . Define $ψ (b) = ψ_{T} (b_{0}) \lor \dots \lor ψ_{T} (b_{n})$ . Thus $(A, ψ)$ is a computable deatomisation of $B$ . □
Theorem 2.5.
Let $B$ be a computable Boolean algebra. Then $A t (B)$ is a computable relation iff any two computable deatomisations $(A_{1}, ψ_{1})$ and $(A_{2}, ψ_{2})$ of $B$ are computably isomorphic (over $B$ ).
Proof.
Suppose that $A t (B)$ is computable and $(A_{1}, ψ_{1})$ , $(A_{2}, ψ_{2})$ are two computable deatomisations of $B$ . Definition 2.6.
Let $(A, ψ)$ be a deatomisation of a Boolean algebra $B$ . A representation of $a \in A$ over $B$ is the set $\begin{matrix} {b, b_{0}, \dots, b_{n}, a_{0}, \dots, a_{n}} \end{matrix}$ such that $b \in B$ , $b_{0}, \dots, b_{n} \in A t (B)$ , $a_{0}, \dots, a_{n} \in A$ , $a_{i} < ψ (b_{i})$ , $b_{i} \neq b$ , $b_{i} \neq b_{j}$ , $i, j ⩽ n$ , $i \neq j$ , and $a = ψ (b) \lor a_{0} \lor \dots \lor a_{n}$ .

It is not difficult to see that such a representation is actually unique (in the right sense). We omit the details since we actually do not need uniqueness in the rest of the proof below. We need the following lemma. Lemma 2.7.
Let $(A, ψ)$ be a computable deatomisation of a computable Boolean algebra $B$ with a computable set of atoms. Then for every $a \in A$ we can effectively find its representation.
Proof.
By Proposition 2.3, such $b \in B$ , $b_{0}, \dots, b_{n} \in A t (B)$ , $a_{0}, \dots, a_{n} \in A$ exist. We simply search for such elements. □

If the set of atoms is computable in $B$ , and $A_{1}$ and $A_{2}$ are two deatomisations of $B$ , then it is easy to compute an isomorphism between $A_{1}$ and $A_{2}$ over $B$ . Given an atom a of $B$ , we can uniformly compute the back-and-forth isomorphism $θ_{a}$ between the atomless principal ideals of $A_{1}$ and $A_{2}$ generated by $ψ_{1} (a)$ and $ψ_{2} (a)$ , respectively. By Lemma 2.7, this can be extended to an isomorphism between $A_{1}$ and $A_{2}$ over $B$ .

Suppose that any two computable deatomisations $A_{1}$ and $A_{2}$ of $B$ are computably isomorphic over $B$ . We build $(A_{1}, ψ_{1})$ and $(A_{2}, ψ_{2})$ using the procedure described in Theorem 2.4, but also incorporate the following diagonalization attempt into this procedure. The idea is to wait for a potential isomorphism $φ_{e}$ to converge on elements of the diatomisation (say, of $A_{1}$ ) below an element $b \in B$ , assuming that b currently looks like it might be an atom. If the isomorphism converges before b ‘splits’ into two non-zero elements, then we have the opportunity to make sure that this map is wrong by adjusting the definition of the embedding $ψ_{2}$ in the second copy. (In some sense, we do ‘the opposite’ in $A_{2}$ by perhaps swapping the elements under b in $A_{2}$ .) Suppose $φ_{e}$ is the actual isomorphism over $B$ and e is the least such index) and it has converged on elements below b, we know that b has to be an atom.

Let $φ_{0}, φ_{1}, \dots$ be an effective list of all computable functions and $\begin{matrix} I [s] = {φ_{i} | i ⩽ s, φ_{i} [s] : A_{1} [s] \to A_{2} [s] is a partial isomorphic embedding} . \end{matrix}$ Continue building $(A (B), ψ)$ into $(A_{1}, ψ_{1})$ and $(A_{2}, ψ_{2})$ along the lines of the procedure described in Theorem 2.4. Let b be an atom in $B [s]$ that has never been used in the construction and choose $a <_{A_{1}} ψ_{1} (b)$ . Start computing $φ_{i} (a)$ for every $φ_{i} \in I [s]$ . Suppose there is $b^{'} <_{B} b$ such that $b^{'}$ appears in $B$ after some $φ_{i} \in I [s]$ has been computed on a. Let i be the least index of such functions. Define $ψ_{1} (b^{'}) = a$ and $ψ_{2} (b^{'}) = ψ_{2} (b) \land \neg φ_{i} (a)$ , where $\neg x$ denotes the (Boolean algebra) complement of x. If there no such $φ_{i}$ , define $ψ_{2} (b^{'}) = a^{'}$ for some $a^{'} <_{A_{2}} ψ_{2} (b)$ .

The resulting $(A_{1}, ψ_{1})$ and $(A_{2}, ψ_{2})$ are computable deatomisations by construction. By the assumption, there is a computable isomorphism $φ_{e} : (A_{1}, ψ_{1}) \to (A_{2}, ψ_{2})$ over $B$ , where e is the least index of a computable isomorphism over $B$ . We never diagonalise against $φ_{e}$ . After a certain stage, say t, all $φ_{i}$ with $i < e$ will either be diagonalised against or we will never have to act for the sake of diagonalising against $ϕ_{i}$ after this stage t. It means that, after this stage t, if some b is not an atom in $B$ then some $b^{'} <_{B} b$ has to appear in $B$ before $φ_{e}$ is computed on a below b. This makes $A t_{B}$ a co-c.e. relation. Since $A t_{B}$ is naturally also a c.e. relation, it follows that $A t_{B}$ is computable. □
Theorem 2.8.
Let $B$ be a punctual Boolean algebra. Then its primitive recursive deatomisation $(A (B), ψ)$ has infinitely many punctual copies that are not punctually isomorphic (over $B$ ).
Proof.
We will build infinitely many punctual deatomisations $\begin{matrix} (A_{0}, ψ_{0}), (A_{0}, ψ_{1}), \dots \end{matrix}$ so that they meet the following requirements: $\begin{matrix} R_{e, k, m} : p_{e} : A_{k} \to A_{m} is not an isomorphism over B, \end{matrix}$ where ${(p_{e})}_{e \in ω}$ is the uniformly computable list of all primitive recursive functions. We arrange R-requirements in some effective list. Unless the current stage is 0, suppose that we just met some requirement at stage $s - 1$ and proceed to the next requirement $R_{e, k, m}$ . In the case when the Boolean algebra is trivial (i.e., is the two-element Boolean algebra), the theorem is equivalent to saying that the atomless Boolean algebra has infinitely many punctual copies that are not punctually isomorphic; this is known [18]. (In fact, in this case they are not even primitively recursively isomorphic.) We thus assume that $B$ has more than two elements. Consider two cases:
$B$ has an atom b; fix it non-uniformly. Build generating trees $T_{A_{i}}$ everywhere except below b, as in the proof of Theorem 2.4. Below b, do the following. Temporarily do not split elements in $A_{m}$ below b, but in $A_{k}$ keep splitting b into more and more elements thus making progress towards making the element atomless. (Meanwhile, keep building $A_{m}$ below the complement of b.) Suppose that currently there are exactly n distinct elements below b in $A_{m}$ . Wait for $p_{e}$ to converge on b and on at least $n + 1$ elements below b in $A_{k}$ . Then $p_{e}$ cannot possibly be an isomorphism, as witnessed at this stage by these finitely many elements and their images. We then resume building $A_{m}$ below b for a few more stages until at some later stage we need to temporarily ‘freeze’ this principal ideal for the sake of some other requirement.

Assume $B$ is atomless. Then, for instance, $(B, id)$ is a punctual deatomisation for $B$ . (This case is almost the same as showing that the atomless Boolean algebra is has infinitely many punctual copies, though it is formally not quite the same. Here $B$ is fixed.) In the construction, unless we need to diagonalise, we build each $A_{⟩}$ to be the identical copy of $B$ , and we let $f_{i} : B \to A_{i}$ to be the identity. To diagonalise against $p_{e} : A_{k} \to A_{m}$ at stage s, introduce a non-zero $x \in A_{k}$ and keep it outside the range of $f_{k}$ . This is done as follows. We embed the generating tree of $B$ (as in Theorem 2.4) into $A_{m}$ . Every time we add new elements into $A_{k}$ and thus extend the tree, we choose the leftmost atom (terminal node) a in $T_{A_{k}} [s]$ and declare that $x < a$ . We extend the diagram of $A_{k}$ accordingly. (This way we push the current interpretation of x further down the left-most infinite path along the tree.) Wait for $p_{e}$ to converge on x, say $p_{e} (x) = b \in A_{m}$ . In particular, b has to be a finite Boolean combination of elements that are currently nodes of the generating tree of $A_{m}$ . Recall that this tree is (essentially) the tree of $B$ , up to the identity map. However, currently x is either strictly less than or is incompatible with any such Boolean combination. For $p_{e}$ to be an isomorphism over $B$ , it has to be the identity map, which is impossible. We recover by setting x equal to (the image of) the first found element in $B$ below the current atom currently bounding x, and proceed to the next requirement.

In each case, in the corresponding construction we let the strategies act one after another according to their instructions. It should be clear that each $(A_{i}), ψ_{i})$ , $i \in ω$ , is a punctual deatomisation, and that these deatomisations are punctually (and indeed, primitively recursively) pairwise non-isomorphic over $B$ . □

3. Algebraically closed fields

Theorem 3.1.
Let F be a punctual field. There is a punctual presentation $A$ of the algebraic closure of F and a primitive recursive embedding $h : F \to A$ .
Proof.
The proof is split into several lemmas. Definition 3.2.
A structure $A$ is punctually decidable if it is punctual and there is a primitive recursive function h such that for every tuple $\bar{a} \in A$ and every first-order formula $φ (\bar{a})$ (identified with its index) $\begin{matrix} h (φ, \bar{a}) = \{\begin{array}{ll} \bar{b}, & if φ (\bar{a}) = \exists \bar{x} ψ (\bar{x}, \bar{a}) and A ⊨ ψ (\bar{b}, \bar{a}); \\ - 1, & otherwise . \end{array} \end{matrix}$
Lemma 3.3 ([7]).

A theory T with a primitive recursive decision procedure has a punctually decidable model $M$ .

Proof.
The proof sketch in [7] is incomplete and misses one important step. We therefore give a detailed proof here. Let $C = {c_{i} | i \in ω}$ be a set of new constants and ${τ_{i} | i \in ω}$ be a primitive recursive list of all sentences of the language $L (T) \cup C$ .

We construct a model $N$ in stages, and a complete primitively recursively decidable theory $Q = {ϕ_{0}, ϕ_{1}, \dots}$ in $L (T) \cup C$ in stages. Let $ϕ_{0}$ denote $(c_{0} = c_{0})$ .

At stage $s = 2 e + 1$ if $ϕ_{e}$ is of the form $\exists x θ (x)$ , as usual find the least k with $c_{k}$ not occurring in $Q_{s}$ . Let $ϕ_{s} = θ (c_{k})$ so that we realize the formula.

At stage $s = 2 e + 2$ , let $\bar{c}$ denote the constants in $Φ = (⋀_{ϕ_{i} \in Q_{s}} ϕ_{i}) \to τ_{e}$ . Let $\bar{x}$ denote the first tuple of variables of the same length as $\bar{c}$ not occurring in Φ. We punctually check whether T proves $\forall \bar{x} Φ [\bar{x} / \bar{c}]$ . If so, let $ϕ_{s} = τ_{e}$ , and if not, $ϕ_{s} = \neg τ_{e}$ .

Recall that the resulting algebraic object upon the constants $c_{i}$ is a pre-structure, since the theory Q can potentially contain statements of the form $c_{i} = c_{j}$ for some $i \neq j$ . However, we can primitively recursively check whether $c_{i} = c_{j} \in Q$ , and if not, then $c_{i} \neq c_{j} \in Q$ . The domain $| N |$ of the structure $N$ is set equal to the indices of those $c_{i}$ that do correspond to new elements: $\begin{matrix} | N | = {i | \forall j < i (c_{i} \neq c_{j} \in Q)}, \end{matrix}$ which is a primitive recursive subset of $N$ . Then, $N$ is a primitive recursive structure that realises the theory Q.

The below lemma is folklore and was noted by many researchers (including Alaev). Lemma 3.4.
Suppose $A$ is a primitive recursive structure and there is a primitive recursive injective function p such that $p (ω) \subset A$ . Then there is a punctual $B$ isomorphic to $A$ .

Let us show that there is a primitive recursive function p that satisfies the conditions of lemma for $N$ . We also build a primitive recursive function $q : ω \to C$ . Let $q (0) = c_{0}$ and $p (0) = c_{0}^{N}$ . To define $p (k + 1)$ find primitively recursively the index of the formula $τ_{i}$ that denotes $\exists x (x \neq q (0) & \dots & x \neq q (k))$ and find the constant $c_{m}$ that realises it. Find the least index n such that $c_{m} = c_{n} \in Q$ and define $q (k + 1) = c_{n}$ and $p (k + 1) = c_{n}^{N}$ . The function p is primitive recursive and it satisfies the condition of the lemma. Then, there is a punctual $M$ isomorphic to $N$ , consequently, a theory T has a punctually decidable model $M$ . □

By $Diag (F)$ we denote the atomic diagram of F, the set of all atomic sentences and negations of atomic sentences of $L_{F} = L \cup {a | a \in F}$ that hold in F. Lemma 3.5.
Let F be a punctual field of the language L, $T^{'}$ be the theory of algebraically closed fields. Then $T^{'} \cup Diag (F)$ has a punctual model $M$ such that there is a primitive recursive isomorphic embedding f from F into $M$ .
Proof.
We build a (complete) primitively recursively decidable theory T such that $T ⊢ T^{'} \cup Diag (F)$ . (It should be clear that such a completion T has to be unique; it will also follow from the explanation given below.)

Since every field F has an algebraic closure $Cl (F)$ and $Cl (F) ⊨ Diag (F)$ , T is consistent. As it is known, the theory of algebraically closed fields has a quantifier elimination, i.e. for every first-order formula σ in the language of fields augmented with constants naming the elements of F, we can find an open σ such that $T^{'} ⊢ σ \equiv σ^{'}$ . Moreover, we can find such $σ^{'}$ primitively recursively, and indeed within ${(N d)}^{n (2 a + 2)}$ stages, where N is a number of polynomials occurring in σ, d is an upper bound on the degrees of polynomials, n is a number of variables, a is a number of quantifier alternations (in the prefix form) [15]. For every σ find an open $σ^{'}$ such that $T^{'} ⊢ σ \equiv σ^{'}$ . Add $σ^{'}$ in T iff $σ^{'} \in Diag (F)$ . Note the latter can be decided primitively recursively.

By Lemma 3.3, T has a punctually decidable model $M$ . For every $a \in F$ we can primitively recursively find an index k and a constant $c_{k}$ such that $c_{k} = a$ , and thus there is a primitive recursive isomorphic embedding f from F into $M$ . □

Note that a model of T does not actually have to be equal to the algebraic closure of $M$ , as it can potentially have elements transcendental over $M$ . To obtain the punctually decidable algebraic closure of F, simply take the algebraic closure of the image of F inside $M$ . Since $M$ is punctually decidable, this process is primitive recursive. □
4. Real closed fields

Theorem 4.1.
Let F be a punctual ordered field. There is a punctual presentation $A$ of the real closure of F and a primitive recursive embedding $h : F \to A$ .

Proof.
Lemma 4.2.
Let F be a punctual ordered field and $T^{'}$ be the theory of real closed fields. Then $T^{'} \cup Diag (F)$ has a punctual model $M$ , and there is a primitive recursive isomorphic embedding f from F into $M$ .
Proof.
Firstly, we build a (complete) primitively recursively decidable theory T such that $T ⊢ T^{'} \cup Diag (F)$ . Since every ordered field F is contained in its real closure R, T is consistent. It is well-known that the theory of real closed fields admits quantifier elimination (with parameters). Moreover, this quantifier elimination is primitive recursive as explained in, e.g., [16]. For every σ in the language of ordered fields with parameters from F, find an open $σ^{'}$ such that $T^{'} ⊢ σ \equiv σ^{'}$ . Add $σ^{'}$ in T iff $σ^{'} \in Diag (F)$ . The latter is primitive recursive, by our assumption.

By Lemma 3.3, T has a punctually decidable model $M$ . For every $a \in F$ we can primitively recursively find k such that $c_{k} = a$ which gives a primitive recursive isomorphic embedding f from F into $M$ . □

To obtain the real closure of F, take the algebraic closure of (the image of) F within $M$ . □ Remark 4.3.
Clearly any ordered field has characteristic 0. Using the associated copy of $Q$ (which is furthermore primitively recursively ordered) for ‘padding’, it is not hard to show that for every primitive recursive ordered field F there is a punctual P and a primitive recursive isomorphism mapping F onto P. Thus, the punctual real closure theorem still holds for primitive recursive fields that are not necessarily punctual.

It is not difficult to see that the algebraic closure theorem also holds for primitive recursive fields. Lemma 3.3 still works if we assume that the domain of the field is a merely primitive recursive subset of $N$ . To see why, name the elements of the field by constants but allow repetition, in the sense that $c_{i}, c_{j} \in Diag (F)$ can denote the same element. We can make sure that it is primitive recursive to tell whether $c_{i} = c_{j}$ (use ‘padding’). Thus, $Diag (F)$ , which will contain statements of the form $c_{i} = c_{j}$ , remains primitive recursive. Lemma 3.3 still works in this case without any further modification. Thus, we can still produce a primitively recursively decidable closure (which has to be punctual). The embedding of F into its closure is primitive recursive as well, and via the same proof.

5. Differentially closed fields

5.1. The punctual prime model theorem

We assume that the reader is familiar with the basic notions of elementary model theory, including the notions of a type, principal type, a complete formula, and the prime model. These standard notions can be found in, e.g., [40]. (We will however include the definitions related to differential fields since these definitions are certainly not quite as well-known.)

Definition 5.1.
We say that a family of types ${(Γ_{i})}_{i \in ω}$ is uniformly primitive recursive if there is a primitive recursive function $p (x, y)$ such that for every $i \in ω$ , $\begin{matrix} p (i, ν (φ)) = \{\begin{array}{ll} 1, & if φ \in Γ_{i}; \\ 0, & otherwise . \end{array} \end{matrix}$

A uniformly primitive recursive family of types $(Γ_{i})$ is uniformly punctual if for every formula $φ (\bar{x})$ , we can uniformly primitively recursively produce an index $i \in ω$ such that $φ (\bar{x}) \in Γ_{i}$ , and returns $- 1$ if no such i exists.
Lemma 5.2.
Suppose $A$ is a punctually decidable structure. Then the family of all types of its theory realized by tuples in $A$ is uniformly punctual.
Proof.
Primitively recursively list all tuples of $A$ in some order, and let $\bar{a}$ be the ith tuple. The ith type $Γ_{i}$ is the collection of all formulae $φ (\bar{x})$ such that $A ⊨ φ (\bar{a})$ . Since $A$ is punctually decidable, the types are uniformly primitive recursive. To see why the types are uniformly punctual, given $φ (\bar{x})$ , define $ψ = \exists \bar{x} φ (\bar{x})$ . Use h from Definition 3.2 to search for a tuple $\bar{a}$ realizing $φ (\bar{x})$ if it exists. The index of the type is determined by the index of the tuple primitively recursively. □

Recall that Theorem 1.3 states that, for a complete theory T with a primitive recursive decision procedure, the following are equivalent:
T has a punctually decidable prime model.

T has a prime model and the set of all principal types of T is uniformly punctual.
Proof of Theorem 1.3.
(a) ⇒ (b) follows from Lemma 5.2.

Now suppose that (b) is true. We follow the argument for the computable case [29, Theorem 7.4] pretty closely making the necessary adjustments.

Let $C = {c_{0}, c_{1}, \dots}$ be a set of new constants, and let $σ_{0}, σ_{1}, \dots$ be a primitive recrusive list of all sentences in $L (T) \cup C$ . As in Lemma 3.3, the domain will be ${c_{0}, c_{1}, \dots}$ from which we later remove repetitions (just as in the proof of Lemma 3.3). The resulting structure will be denoted $A$ .

We build $A$ so that for every $n ⩾ 0$ , $(c_{0}, c_{1}, \dots, c_{n})$ realizes a primitive recursive principal type of T. Then, every finite sequence of elements in $A$ will satisfy some principal type.

We will construct a full diagram Ψ of $A$ by stages. At every stage s, we construct a finite set of sentences $Ψ^{s}$ such that $Ψ^{s - 1} \subset Ψ^{s}$ and $Ψ = ⋃_{s \in ω} Ψ^{s}$ .

Let $ψ^{s} = \land Ψ^{s}$ . If $ψ^{s} = ψ^{s} (c_{0}, \dots, c_{n_{s}})$ , then for every $e ⩽ n_{s}$ , we set $\begin{matrix} ψ_{e}^{s} = \exists y_{e + 1} \dots \exists y_{n_{s}} ψ^{s} (c_{0}, \dots, c_{e}, [y_{e + 1} / c_{e + 1}], \dots, [y_{n_{s}} / c_{n_{s}}]), \end{matrix}$ where ‘ $w / b$ ’ stands for the substitution of b by w (here and throughout the rest of the proof). This transformation of formulae is clearly uniformly primitive recursive.

For every e, at almost every stage s, we define a primitive recursive principal type $Ω_{e}^{s}$ which is a candidate for a primitive recursive principal type realized by $(c_{0}, c_{1}, \dots, c_{e})$ . In finite number of stages $Ω_{e}^{s}$ can be undefined. Because of the consistency property, if $Ω_{e}^{s}$ is defined then $ψ_{e}^{s} (\bar{x} / \bar{c}) \in Ω_{e}^{s}$ . The construction will satisfy the following requirements for every $e ⩾ 0$ . $\begin{array}{c} P_{e}^{1} : σ_{e} \in Ψ or \neg σ_{e} \in Ψ; \\ P_{e}^{2} : If σ_{e} = \exists x θ (x) \in Ψ, then θ (c) \in Ψ for some c \in C; \\ Q_{e} : (c_{0}, c_{1}, \dots, c_{e}) realizes a principal type of T . \end{array}$

The priority ranking of the requirements in the decreasing order is: $\begin{matrix} P_{0}^{1}, P_{0}^{2}, Q_{0}, P_{1}^{1}, P_{1}^{2}, Q_{1}, \dots \end{matrix}$ We attempt to satisfy the requirements in the order of their priority. We say that at stage $s > 0$ :
$P_{e}^{1}$ requires attention if $σ_{e}, \neg σ_{e} \notin Ψ^{s - 1}$ ;

$P_{e}^{2}$ requires attention if $σ_{e} \in Ψ^{s - 1}$ and $σ_{e} = \exists x θ (x)$ for some θ such that $θ (c) \notin Ψ^{s - 1}$ for every $c \in C$ ;

$Q_{e}$ requires attention if $Ω_{e}^{s - 1}$ is undefined.
Once satisfied at some stage, requirements $P_{e}^{1}$ and $P_{e}^{2}$ are never injured later. However, we say that $Q_{e}$ is injured at stage $s > 0$ if $Ω_{e}^{s - 1}$ is defined but $ψ_{e}^{s} (\bar{x} / \bar{c}) \notin Ω_{e}^{s - 1}$ .

Construction
Stage 0:

Let $Ψ^{0} = \emptyset$ and let $Ω_{e}^{0}$ be undefined for every $e \in ω$ .

Stage $s > 0$ :

Let Req be the highest priority requirement that requires attention at stage s. We now satisfy Req as follows.

Suppose $Req = P_{e}^{1}$ .
If $T ⊢ \forall \bar{x} [(ψ^{s - 1} \to σ_{e}) (\bar{x} / \bar{c})]$ , then $Ψ^{s} = Ψ^{s - 1} \cup {σ_{e}}$ .

If $T ⊢ \forall \bar{x} [(ψ^{s - 1} \to \neg σ_{e}) (\bar{x} / \bar{c})]$ , then $Ψ^{s} = Ψ^{s - 1} \cup {\neg σ_{e}}$ .
(The properties on the left-hand side of (a) and (b) can be checked primitively recursively because T is primitively recursively decidable.)
If neither (a) nor (b) is satisfied, we add either $σ_{e}$ or $\neg σ_{e}$ to $Ψ^{s - 1}$ such that if some Q-requirement must be injured, then the requirement is of the lowest priority possible. We uniformly primitively recursively check whether some $Q_{n}$ is injured at stage s. (Note only finitely many $Q_{n}$ have ever acted before this stage.) Let $n_{0}$ be the least such n, if it exists. For every $n ⩾ n_{0}$ , set $Ω_{n}^{s}$ undefined.
Let $Req = P_{e}^{2}$ . Thus, $σ_{e} \in Ψ_{s - 1}$ and $σ_{e} = \exists x θ (x)$ for some θ. Let c be the first constant in C which has not been used in the construction before stage s. We define $Ψ^{s} = Ψ^{s - 1} \cup {θ (c)}$ .

Let $Req = Q_{e}$ . Thus, $Ω_{e}^{s - 1}$ is undefined. Using uniform punctuality of the type, find n such that $ψ_{e}^{s - 1} (x_{0} / c_{0}, \dots, x_{e} / c_{e}) \in Γ_{n}$ . There are only finitely many $i < n$ and n is computed (uniformly) primitively recursively, and these $Γ_{i}$ are also uniformly primitive recursive. Thus, without loss of primitive recursiveness we can pick n that is the least with this property. Set $Ω_{e}^{s} = Γ_{n} (x_{0}, \dots, x_{e})$ .

Before we proceed to the verification, note that every step of the construction was performed (uniformly) primitively recursively. The verification is quite similar to the verification in the proof of [29, Theorem 7.4]; we sketch it to make the paper (more) self-contained. We compress the parts of the verification that are more related to finite injury or to model theory (since they are literally the same as in the computable case), but we emphasise where primitive recursiveness of the theory and the uniform punctuality of the principal types are used to conclude that the resulting structure is punctually decidable. Lemma 5.3.
For every e, $Ω_{e} ⇌ {lim}_{s} Ω_{e}^{s}$ exists. (Hence, $Q_{e}$ is satisfied.)

(We remark that we do not claim that the rate of convergence stated in the lemma is primitive recursive, nor that the principal formula of the resulting type can be found primitively recursively.) Proof.
Assume that $e = 0$ . Let $t_{0}$ be the least stage such that $Ω_{0}^{t_{0}}$ is defined. Let $Ω_{0}^{t_{0}} = Γ_{n_{0}}$ . Then $ψ_{0}^{t_{0} - 1} (x_{0} / c_{0}) \in Γ_{n_{0}}$ . Hence, by the construction, $Q_{0}$ will never be injured, so $Ω_{0} = Γ_{n_{0}}$ .

Assume $e = 1$ . Let $ξ_{0}$ be a complete formula such that $ξ_{0} \in Ω_{0} (= Γ_{n_{0}})$ . Choose the least stage $s_{0}$ such that $ξ_{0} (c_{0}) \in Ψ^{s_{0}}$ . Let $t_{1}$ be the least stage $> s_{0}$ such that $Ω_{1}^{t_{1}}$ is defined. Then $ψ_{1}^{t_{1} - 1} (x_{0} / c_{0}, x_{1} / c_{1}) \in Ω_{1}^{t_{1}}$ . Since every formula consistent with $Ψ^{s_{0}} (\bar{x} / \bar{c})$ is also consistent with $Ω_{0}$ , it follows that $Q_{1}$ is not injured after $t_{1}$ .

The general proof is by induction on e. If $e > 0$ , choose the least s such that
$\forall t > s (Ω_{e - 1}^{t} = Ω_{e - 1}^{s} = Ω_{e - 1})$ ,

$ψ_{e - 1}^{s} (x_{0} / c_{0}, \dots, x_{e - 1} / c_{e - 1}) is a complete formula for Ω_{e - 1}$ ,

$Ω_{e}^{s} is defined.$
Let $t > s$ . It follows that $Ω_{e}^{t} = Ω_{e}^{s}$ since $ψ_{e - 1}^{s} (x_{0} / c_{0}, \dots, x_{e - 1} / c_{e - 1}) \in Ω_{e}^{s}$ . □

Now we show that the constructed structure $A$ is punctually decidable. For that we build a primitive recursive function h from Definition 3.2. Suppose that $φ (\bar{a}) = \exists \bar{x} ψ (\bar{x}, \bar{a})$ . Find e such that $σ_{e} (\bar{c}) = \exists \bar{x} ψ (\bar{x}, \bar{c})$ , where constants $\bar{c}$ are realized by $\bar{a}$ in $A$ . Let s be the least stage when the requirement $P_{e}^{2}$ is already met. Note such requirements are never injured, and thus we can primitively recursively compute the stage of the construction at which such a requirement is met. It is crucial here that each stage of the construction is finished within a pre-computed uniformly primitive recursive bound. This is essentially the only step of the proof where we needed the types to be uniformly punctual and not merely uniformly primitive recursive or uniformly computable. (As we already mentioned earlier, we never actually need to compute, let alone primitively recursively compute, the complete formulae for these types.) Thus, we can primitively recursively find $\bar{c^{'}}$ such that $A ⊨ ψ (\bar{c^{'}}, \bar{a})$ . Let $h (φ, \bar{a}) = {\bar{c}}^{'}$ (strictly speaking, we really mean the equivalence class of ${\bar{c}}^{'}$ in $A$ ). Since our construction is primitive recursive, the function h is also primitive recursive. □

5.2. The finite basis property

In this subsection we prove the punctual version of a technical fact established in [30]. This fact will be used later to apply the theorem established in the previous subsection to primitive recursive differential fields. The following definitions are taken directly from [30].

Definition 5.4.
A theory T has the finite basis property if, for any collection S of atomic formulas in n variables, there is a finite subset F of S such that T, $F ⊢ S$ .
Definition 5.5.
We call a quantifier free formula $φ (\bar{x})$ in $L (T)$ constrained if, for every atomic formula $θ (\bar{x})$ , either T, $φ (\bar{x}) ⊢ θ (\bar{x})$ or T, $φ (\bar{x}) ⊢ \neg θ (\bar{x})$ .
Lemma 5.6.
Let a theory T have a primitive recursive decision procedure and a primitive recursive quantifier elimination algorithm. Assume that T has the finite basis property and every quantifier free constrained formula of $L (T)$ is complete. Then T has a punctually decidable prime model.
Proof.
Let $φ (\bar{x})$ be consistent with T. Since T has quantifier elimination we can find a quantifier free formula $ψ (\bar{x})$ such that $T ⊢ φ (\bar{x}) \leftrightarrow ψ (\bar{x})$ .

Construct a primitive recursive collection S of atomic formulas in the variable x as follows: $S_{0} = {ψ (\bar{x})}$ . Given $S_{n}$ , let $θ (\bar{x})$ be the nth atomic formula in the variables $\bar{x}$ . If $T \cup S_{n} \cup {θ (\bar{x})}$ is consistent, let $S_{n + 1} = S_{n} \cup {θ (\bar{x})}$ . Otherwise, let $S_{n + 1} = S_{n}$ . Let $S = ⋃_{n \in ω} S_{n}$ .

By the finite basis property there is a finite subset F of S such that F generates S. For any atomic formula $θ (\bar{x})$ , either $θ (\bar{x}) \in S$ or $T \cup S ⊢ \neg θ (\bar{x})$ . Thus the conjunction of F is a quantifier free constrained formula. Now consider the following type $Γ_{φ}$ . Let a formula $ξ (\bar{x}) \in Γ_{φ} \Leftrightarrow T \cup S ⊢ ξ^{'} (\bar{x})$ , where $ξ^{'} (\bar{x})$ is an equivalent to $ξ (\bar{x})$ quantifier free formula. Then $Γ_{φ}$ is primitively recursive, since T has quantifier elimination and for quantifier free $ξ^{'}$ we can primitively recursively decide whether $T \cup S ⊢ ξ^{'} (\bar{x})$ or not. Besides, $Γ_{φ}$ is a principal type since the conjunction of F is a complete formula for $Γ_{φ}$ .

Let $(Γ_{φ})$ be the uniformly primitive recursive family of principal types defined by the procedure above, where φ ranges over all first-order formulae in the language of T consistent with T. This family includes all principal types of T; indeed, if φ is complete for a principal type Γ, then $Γ = Γ_{φ}$ . According to the uniformly primitive recursive procedure described in the previous paragraph, given φ we can uniformly primitively recursively produce $Γ_{φ}$ that contains φ, making the family $(Γ_{φ})$ uniformly punctual.

Thus by Theorem 1.3, T has a primitively recursively presentable prime model. □

5.3. Punctual differential closure

A differential field is a field K equipped with a derivation $δ : K \to K$ ; recall that this means that, for $x, y \in K$ , we have $δ (x + y) = δ (x) + δ (y)$ and $δ (x y) = x δ (y) + y δ (x)$ . If K is a differential field, we define $K {X_{1}, \dots, X_{n}}$ , the ring of differential polynomials over K, to be the following polynomial ring in infinitely many variables: $\begin{matrix} K [X_{1}, \dots, X_{n}, δ (X_{1}), \dots, δ (X_{n}), \dots, δ^{m} (X_{1}), \dots, δ^{m} (X_{n}), \dots] . \end{matrix}$ A differential field K is differentially closed if, whenever $f, g \in K {X}$ , g is nonzero and the order of f is greater than the order of g, there is $a \in K$ such that $f (a) = 0$ and $g (a) \neq 0$ . The following facts can be found in, e.g., [39]. The theory of differential fields of characteristic 0, ${DF}_{0}$ , in the language $L = {+, -, \cdot, δ, 0, 1}$ is given by the axioms for fields of characteristic zero and the axioms $\begin{array}{c} \forall x \forall y δ (x + y) = δ (x) + δ (y), \\ δ (x y) = x δ (y) + y δ (x) . \end{array}$ The theory ${DCF}_{0}$ of differentially closed fields of characteristic zero is axiomatized by ${DF}_{0}$ and the set of axioms $φ_{m, d_{0}, d_{1}}$ , for all m, $d_{0}$ , $d_{1}$ , where $φ_{m, d_{0}, d_{1}}$ is a sentence of language $L$ that asserts that if f is a differential polynomial of order m and degree at most $d_{0}$ and g is a nonzero differential polynomial of order less than m and degree at most $d_{1}$ , then there is a solution to $f (X) = 0$ and $g (X) \neq 0$ .

Corollary 5.7.

A primitive recursive differential field $A$ of characteristic 0 can be punctually isomorphically embedded into its punctually decidable differential closure.

Proof.

Robinson [45] showed that the theory ${DF}_{0}$ of differential fields of characteristic zero has a model completion ${DCF}_{0}$ . ${DCF}_{0}$ is complete and substructure complete. For every substructure complete theory T, every quantifier free constrained formula of $L (T)$ is complete; see [46]. Blum [12] showed that any model of ${DF}_{0}$ has a prime differential closure, that is, ${DCF}_{0} \cup Diag (A)$ has a prime model. For any $M ⊨ {DF}_{0}$ , ${DCF}_{0} \cup Diag (M)$ has the finite basis property; see [36]. The theory ${DCF}_{0}$ has a primitive recursive quantifier elimination algorithm [28]. Then, the theory ${DCF}_{0} \cup Diag (A)$ is also primitively recursively decidable. Thus, by Lemma 5.6, given a punctual model $A ⊨ {DF}_{0}$ , we can construct a punctually decidable prime model $B ⊨ Diag (A) \cup {DCF}_{0}$ . □

Footnotes

Acknowledgements

This work was partially supported by Rutherford Discovery Fellowship (RDF-VUW1902) and Marsden Fund of New Zealand (VUW2015), Royal Society Te Apārangi. The work of Melnikov was partially supported by Grant No. AP19676989, Ministry of Science and Higher Education of the Republic of Kazakhstan. We are also grateful to Dave Marker who provided us with several useful bibliographical references.

References

P.E.

Alaev , Existence and uniqueness of structures computable in polynomial time, Algebra and Logic55(1) (2016), 72–76. doi:10.1007/s10469-016-9377-6.

P.E.

Alaev , Categoricity for primitively recursive and polynomial Boolean algebras, Algebra Logika57(4) (2018), 389–426. doi:10.1007/s10469-018-9498-1.

P.E.

Alaev , Finitely generated structures computable in polynomial time, Sib. Math. J.63(5) (2022), 801–818. doi:10.1134/S0037446622050019.

P.E.

Alaev and

V.L.

Selivanov , Fields of algebraic numbers computable in polynomial time. II, Algebra Logic60(6) (2021), 349–359. doi:10.1007/s10469-022-09661-3.

P.E.

Alaev and

V.L.

Selivanov , Searching for applicable versions of computable structures, in: Connecting with Computability, Lecture Notes in Comput. Sci., Vol. 12813, Springer, Cham, 2021, pp. 1–11.

Ash and

Knight , Computable Structures and the Hyperarithmetical Hierarchy, Studies in Logic and the Foundations of Mathematics, Vol. 144, North-Holland Publishing Co., Amsterdam, 2000.

Bazhenov ,

Downey ,

Kalimullin and

Melnikov , Foundations of online structure theory, Bull. Symb. Log.25(2) (2019), 141–181. doi:10.1017/bsl.2019.20.

Bazhenov ,

Fiori-Carones ,

Liu and

Melnikov , Primitive recursive reverse mathematics, Preprint.

Bazhenov ,

Harrison-Trainor ,

Kalimullin ,

Melnikov and

Meng Ng , Automatic and polynomial-time algebraic structures, J. Symb. Log.84(4) (2019), 1630–1669. doi:10.1017/jsl.2019.26.

10.

Bazhenov ,

Kalimullin ,

Melnikov and

Meng Ng , Online presentations of finitely generated structures, Theoret. Comput. Sci.844 (2020), 195–216. doi:10.1016/j.tcs.2020.08.021.

11.

K.V.

Blinov , Primitively recursively categorical linear orderings, Sibirsk. Mat. Zh.60(1) (2019), 28–36. doi:10.33048/smzh.2019.60.103.

12.

Blum , Generalized algebraic structures: A model theoretic approach, PhD thesis, Massachussetts Institute of Technology, Cambridge, MA, 1968.

13.

D.A.

Cenzer and

J.B.

Remmel , Polynomial-time versus recursive models, Ann. Pure Appl. Logic54(1) (1991), 17–58. doi:10.1016/0168-0072(91)90008-A.

14.

D.A.

Cenzer and

J.B.

Remmel , Polynomial-time Abelian groups, Ann. Pure Appl. Logic56(1–3) (1992), 313–363. doi:10.1016/0168-0072(92)90076-C.

15.

A.L.

Chistov and

D.Y.

Grigor’ev , Complexity of quantifier elimination in the theory of algebraically closed fields, in: Mathematical Foundations of Computer Science, 1984, Prague, 1984, Lecture Notes in Comput. Sci., Vol. 176, Springer, Berlin, 1984, pp. 17–31. doi:10.1007/BFb0030287.

16.

J.H.

Davenport and

Heintz , Real quantifier elimination is doubly exponential, J. Symbolic Comput.5(1–2) (1988), 29–35. doi:10.1016/S0747-7171(88)80004-X.

17.

Dorzhieva ,

Downey ,

Hammatt ,

Melnikov and

K.M.

Ng , Punctually presented structures II: Comparing presentations, Preprint.

18.

M.V.

Dorzhieva ,

A.A.

Issakhov ,

B.S.

Kalmurzayev ,

R.A.

Kornev and

M.V.

Kotov , Punctual dimension of algebraic structures in certain classes, Lobachevskii J. Math.42(4) (2021), 716–725. doi:10.1134/S1995080221040089.

19.

Downey ,

Greenberg ,

Melnikov ,

Meng Ng and

Turetsky , Punctual categoricity and universality, J. Symb. Log.85(4) (2020), 1427–1466. doi:10.1017/jsl.2020.51.

20.

Downey ,

Harrison-Trainor ,

Kalimullin ,

Melnikov and

Turetsky , Graphs are not universal for online computability, J. Comput. System Sci.112 (2020), 1–12. doi:10.1016/j.jcss.2020.02.004.

21.

Downey ,

Melnikov and

Meng Ng , Foundations of online structure theory II: The operator approach, Log. Methods Comput. Sci.17(3) (2021), 6.

22.

Ershov and

Goncharov , Constructive Models. Siberian School of Algebra and Logic, Consultants Bureau, New York, 2000.

23.

Y.L.

Ershov , Numbered fields, in: Methodology and Philosophy of Science III,

Van Rootselaar and

J.F.

Staal , eds, Studies in Logic and the Foundations of Mathematics, Vol. 52, North-Holland Publishing Co., Amsterdam, 1968, pp. 31–34.

24.

Fels Ritt , Differential Algebra, American Mathematical Society Colloquium Publications, Vol. XXXIII, American Mathematical Society, New York, NY, 1950.

25.

Goncharov , Countable Boolean Algebras and Decidability. Siberian School of Algebra and Logic, Consultants Bureau, New York, 1997.

26.

S.S.

Goncharov and

A.T.

Nurtazin , Constructive models of complete decidable theories, Algebra i Logika12(125–142) (1973), 243.

27.

Greenberg ,

Harrison-Trainor ,

Melnikov and

Turetsky , Non-density in punctual computability, Ann. Pure Appl. Logic172(9) (2021), 102985. doi:10.1016/j.apal.2021.102985.

28.

D.Y.

Grigor’ev , Complexity of quantifier elimination in the theory of ordinary differential equations, in: EUROCAL ’87, Leipzig, 1987, Lecture Notes in Comput. Sci., Vol. 378, Springer, Berlin, 1989, pp. 11–25. doi:10.1007/3-540-51517-8_81.

29.

V.S.

Harizanov , Pure computable model theory, in: Handbook of Recursive Mathematics, Stud. Logic Found. Math., Vol. 1, North-Holland, Amsterdam, 1998, pp. 3–114.

30.

Harrington , Recursively presentable prime models, J. Symbolic Logic39 (1974), 305–309. doi:10.2307/2272643.

31.

Harrison-Trainor ,

Melnikov and

Montalbán , Independence in computable algebra, J. Algebra443 (2015), 441–468. doi:10.1016/j.jalgebra.2015.06.004.

32.

Harrison-Trainor ,

A.G.

Melnikov and

Miller , On computable field embeddings and difference closed fields, Canadian Journal of Mathematics69(6) (2017), 1338–1363. doi:10.4153/CJM-2016-044-7.

33.

Kalimullin ,

Melnikov and

Meng Ng , Algebraic structures computable without delay, Theoret. Comput. Sci.674 (2017), 73–98. doi:10.1016/j.tcs.2017.01.029.

34.

Kalimullin ,

Melnikov and

Montalban , Punctual definability on structures, Ann. Pure Appl. Logic172(8) (2021), 102987. doi:10.1016/j.apal.2021.102987.

35.

I.S.

Kalimullin and

Miller , Primitive recursive fields and categoricity, Algebra and Logic58(1) (2019), 95–99. doi:10.1007/s10469-019-09527-1.

36.

Kaplansky , An Introduction to Differential Algebra, Publ. Inst. Math. Univ. Nancago, Vol. 5, Hermann, Paris, 1957.

37.

E.W.

Madison , A note on computable real fields, The Journal of Symbolic Logic35(2) (1970), 239–241. doi:10.2307/2270515.

38.

Mal’cev , Constructive algebras. I, Uspehi Mat. Nauk16(3) (1961), 3–60.

39.

Marker , Model theory of differential fields, in: Model Theory, Algebra, and Geometry, Math. Sci. Res. Inst. Publ., Vol. 39, Cambridge Univ. Press, Cambridge, 2000, pp. 53–63.

40.

Marker , Model Theory: An Introduction, Graduate Texts in Mathematics, Springer, 2002.

41.

Marker and

Miller , Turing degree spectra of differentially closed fields, J. Symb. Log.82(1) (2017), 1–25. doi:10.1017/jsl.2016.73.

42.

Melnikov and

Meng Ng , A structure of punctual dimension two, Proc. Amer. Math. Soc.148(7) (2020), 3113–3128. doi:10.1090/proc/15020.

43.

Montalbán , Computable Structure Theory – Within the Arithmetic. Perspectives in Logic, Cambridge University Press, Cambridge; Association for Symbolic Logic, Ithaca, NY, 2021.

44.

M.O.

Rabin , Computable algebra, general theory and theory of computable fields, Transactions of the American Mathematical Society95(2) (1960), 341–360. doi:10.1090/S0002-9947-1960-0113807-4.

45.

Robinson , On the concept of a differentially closed field, Bull. Res. Council Israel Sect. F8F (1959), 113–128.

46.

G.E.

Sacks , Saturated Model Theory, 2nd edn, World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ, 2010.

47.

V.L.

Selivanov and

Selivanova , Primitive recursive ordered fields and some applications, in: Computer Algebra in Scientific Computing, CASC 2021,

Boulier ,

England ,

T.M.

Sadykov and

E.V.

Vorozhtsov , eds, Lecture Notes in Computer Science, Vol. 12865, Springer, Cham, 2021, pp. 353–369. doi:10.1007/978-3-030-85165-1_20.

48.

Simpson , Subsystems of Second Order Arithmetic. Perspectives in Logic, 2nd edn, Cambridge University Press, Cambridge, 2009.

49.

Smith , Two theorems on autostability in p-groups, in: Logic Year 1979–80 (Proc. Seminars and Conf. Math. Logic, Univ. Connecticut, Storrs, Conn., 1979/80), Lecture Notes in Math., Vol. 859, Springer, Berlin, 1981, pp. 302–311. doi:10.1007/BFb0090954.

50.

M.V.

Zubkov ,

I.S.

Kalimullin ,

A.G.

Mel’nikov and

A.N.

Frolov , Punctual copies of algebraic structures, Sibirsk. Mat. Zh.60(6) (2019), 1271–1285. doi:10.33048/smzh.2019.60.607.