Feasible set functions have small circuits

Abstract

The Cobham Recursive Set Functions (CRSF) provide an analogue of polynomial time computation which applies to arbitrary sets. We give three new equivalent characterizations of CRSF. The first is algebraic, using subset-bounded recursion and a form of Mostowski collapse. The second is our main result: the CRSF functions are shown to be precisely the functions computed by a class of uniform, infinitary, Boolean circuits. The third is in terms of a simple extension of the rudimentary functions by transitive closure and subset-bounded recursion.

Keywords

Computational complexity primitive recursive set functions circuit complexity Cobham recursive set functions

1. Introduction

Computability over the natural numbers has over the years been successfully extended to robust notions of computability on ordinals, on objects of finite type and on sets in general (see for example Sacks’ book [10]). Our goal is to develop an analogous, robust extension of computational complexity to arbitrary sets. This is the third of a series of papers exploring the model for polynomial-time computation on arbitrary sets given by the Cobham recursive set functions (CRSF) [4,5]. A broader and promising future programme is to carry this out for other notions from complexity theory. This paper is largely self-contained. In particular, as it relies on a different definition of CRSF, it can be read independently of [4] and [5].

The class CRSF was introduced in [4] to capture the notion of feasible, polynomial time computation on arbitrary sets. In particular, it coincides with the usual polynomial time functions on finite binary strings, if strings in ${0, 1}^{k}$ are identified with the corresponding set-theoretic functions in $^{k} 2$ .

The definition of CRSF in [4] is as a function algebra, based on a generalization of Cobham recursion on notation to arbitrary sets. A proof-theoretic characterization of CRSF, in terms of a version of Kripke-Platek set theory, is given in [5]. Furthermore, as shown in [4], the CRSF functions are closely connected to the Predicatively Computable Set Functions (PCSF) defined by Arai [2], which give a different characterization of polynomial time functions on sets. The PCSF functions are defined using safe recursion on notation, which was earlier used in [3] to define the larger class of Safe Recursive Set Functions (SRSF). A related notion of polynomial time on certain infinite sets was defined by Schindler [12]; see [3] for connections between this and SRSF. Sazonov [11] introduced a class of polynomial time functions on hereditarily finite sets, which we compare to CRSF in [4].

In [4] we take ∈-recursion as the basic model for computation on sets. The innovation is that the power of ∈-recursion is restricted by allowing new functions to be introduced only if their output is no more complex than the output of a function already known to be in CRSF, in the style of Cobham’s definition of polynomial time [6]. Here a set a is no more complex than a set b if a is embeddable in b in a certain sense (which we describe later). To allow a limited, “polynomial” increase in complexity [4] adapts the smash function # of bounded arithmetic into an operation on sets, namely a kind of cartesian product on Mostowski graphs, and includes this as one of the initial functions.

We introduce here three alternative characterizations of CRSF. These all take ∈-recursion as fundamental, but they restrict its strength in different ways, and one of them does not use the smash function. That they all give rise to the same class of functions gives more evidence that CRSF is natural.

The first characterization is similar to [4]. The class ${CRSF}_{\subseteq}$ is formed by taking some basic initial functions, including the smash function, and closing under composition and subset-bounded recursion: if g and h are in the class, then so is the function f defined by the recursion $\begin{matrix} f (\vec{a}, b) = g (\vec{a}, b, {f (\vec{a}, c) : c \in b}) \cap h (\vec{a}, b) . \end{matrix}$ We call this “subset-bounded” because it allows defining a function f by recursion only if we have in hand a function h such that $f (\vec{a}, b) \subseteq h (\vec{a}, b)$ . The main difference between this and the definition in [4] is the use of this simpler kind of recursion instead of the rather complicated “embedding-bounded” recursion of [4], of which it is a special case. The disadvantage is that ${CRSF}_{\subseteq}$ functions are limited in what they can output, because any output value must look more or less like a subset of (some basic function of) the input.

To deal with this we use a system for coding sets as subsets. A standard way to represent a finite graph in computer science is as a subset of $n \times n$ (coded as a binary string of length $n^{2}$ ) giving the edge relation, where n is a size parameter. Similarly we can take a set, represent a copy of its Mostowski graph as a subset E of $a \times a$ , where a is some suitable set, and then recover the original set from E using Mostowski collapse. It turns out that we still get a robust system of coding if we restrict the kinds of subset E that can appear (by only allowing edges consistent with the ordering induced by ∈), and that then we do not need the full strength of Mostowski collapse but can make do with a limited, “feasible” version of it.

We define ${CRSF}_{\subseteq}^{+}$ by adding this limited Mostowski collapse function to ${CRSF}_{\subseteq}$ . We show that ${CRSF}_{\subseteq}^{+}$ and the original $CRSF$ are the same, and in particular that for every $CRSF$ function $f (\vec{x})$ there is a ${CRSF}_{\subseteq}$ function which computes a code for $f (\vec{x})$ . It follows that we can compute $f (\vec{x})$ in ${CRSF}_{\subseteq}^{+}$ with only a single use of Mostowski collapse, and also that ${CRSF}_{\subseteq}$ and $CRSF$ contain the same relations, that is, the same 0/1 valued functions.

Our second characterization takes a very different approach, by describing a Boolean circuit model of computation on sets. We define (possibly infinite) circuits, which act on Boolean (0/1) values and have the usual conjunction, disjunction and negation gates. To allow these to input and output sets, we use the method of coding outlined above. For example, if we want to take as input sets which can be coded as a subset E of $a \times a$ , we include an input node for each member u of $a \times a$ , and assign it the value 1 if $u \in E$ and 0 otherwise – and as is usual in circuit complexity, we will need a different circuit for each size parameter a. We show that CRSF can be precisely characterized as the functions which can be computed by strongly uniform families of small Boolean circuits, where “small” is defined in terms of the smash function. This is our main result, and shows that a basic property of polynomial time functions carries across smoothly to arbitrary sets.

There are several advantages to the Boolean circuit characterization. First, it is quite different from the earlier characterizations, thus providing more evidence of the robustness of CRSF. Second, it makes clear that CRSF is, in part, a model of parallel computation. This fact is obscured in the earlier development in [4], as that work focused on the equivalence with polynomial time computation. Third, it allows tools from the usual theory of Boolean circuit complexity to be applied to CRSF. As an example, using the Hastad switching lemma about the inexpressibility of parity in ${AC}^{0}$ [8], we can show a version of $P \neq NP$ for CSRF. We hasten to mention that this does not say anything about whether the usual classes of P and NP are distinct.

Our third characterization is again as a function algebra, this time defined by extending the rudimentary functions in an elementary way. We take the class RS to be the rudimentary functions plus the transitive closure function, all closed under subset-bounded recursion. We do not add the smash function, and it is easy to see that smash is not in RS, which hence is different from CRSF. However we adapt our system of coding to RS and show that CRSF functions can be defined in RS via their codes, and thus that the classes are essentially the same except for issues of decoding. The key is to show that ∈-recursion in the presence of smash can be simulated by lexicographic ∈-recursion without smash.

There are several potential routes for future work. This paper, together with related work [2–4,12], shows that we have established a robust understanding of polynomial time in set theory. Obvious next steps are to find set theoretic analogues for other time, space or circuit complexity classes which are well-known and well-studied in the context of finite binary strings.

The outline is as follows. Section 2 discusses preliminary topics, and introduces our version of the Mostowski collapse and smash functions. Section 3 introduces subset-bounded recursion, defines our version of CRSF, and proves some basic properties of these definitions. Section 4 introduces a simple model of infinite-time Turing machine computation and shows that on finite and infinite binary strings, CRSF functions are the same as those computed by corresponding notions of polynomial time Turing machines. Section 5 introduces some technical material, in particular bisimilarity, which we will use to detect when two encodings of Mostowski graphs represent the same set. Section 6 defines infinite Boolean circuits, and also the notion of $Δ_{0}^{#}$ -uniform families of Boolean circuits. Section 7 proves a series of strong technical results about the power of $Δ_{0}^{#}$ -uniform circuits. Section 8 completes the proof that the CRSF functions are precisely the functions computable with $Δ_{0}^{#}$ -uniform circuits. It also gives a $P \neq NP$ style result for CRSF functions acting on hereditarily finite (HF) sets. Section 9 proves the equivalence of our version of $CRSF$ and $CRSF$ as defined in [4]. Section 10 shows that adding transitive closure and subset-bounded recursion to Jensen’s rudimentary functions gives another characterization of CRSF.

2. Preliminaries

2.1. Notational conventions

The partial ordering induced on sets by ∈ will play a fundamental role for us, analogous to the ordering on natural numbers. We therefore use the notation < for the transitive closure of the ∈ relation, and the notation ⩽ for the reflexive transitive closure. Writing $tc (b)$ for the transitive closure of b, this means that $a < b$ and $a ⩽ b$ are equivalent to $a \in tc (b)$ and $a \in tc ({b})$ , respectively. To further strengthen the analogy to the interval notation and because it will be convenient for the generalized notion of “binary string” defined below, we write $[a]$ for $tc ({a})$ (this was denoted ${tc}^{+} (a)$ in [4]). This notation is meant to suggest the “interval” $[0, a] = {x : \emptyset ⩽ x ⩽ a}$ .

We often code one set inside another set in a way that generalizes the usual notion of binary strings. We will stick as much as possible to the following convention. We treat some sets as “raw materials”, inside whose Mostowski graphs we will construct other objects. We write these “raw material” sets using small letters $a, b, \dots$ ; they are analogous to unary strings in complexity theory. We use capital letters $E, F, \dots$ or $U, V, \dots$ for objects we construct as subsets of the Mostowski graphs of sets of the first kind; these are analogous to binary strings. For ordinary binary strings, the analogy is precise: an ordinary unary string of length n is identified with the von Neumann integer $a = n$ , and an ordinary binary string of length n is then the subset U of a having as members the positions where a bit 1 appears in the string.

In a directed graph, if there is an edge from a node u to a node v we say that u is a predecessor of v. If there is a path (possibly of length 0) from u to v we say that u is an ancestor of v. We will usually be dealing with acyclic (in fact well-founded) directed graphs, and when we describe directed graphs we think of the edges as pointing upwards.

We define the ordered pair as $⟨ a, b ⟩ = {{a}, {a, b}}$ and extend this in the usual way to ordered k-tuples, with $⟨ a, b, c ⟩ = ⟨ a, ⟨ b, c ⟩ ⟩$ etc. and $⟨ \vec{a} ⟩ = a$ if $\vec{a}$ is a 1-tuple. We will write ${[a]}^{k}$ for the k-th cartesian power of $[a]$ , since we will need to refer to this often. But we do not use this notation for sets not written in the form $[a]$ to avoid confusion with ordinal exponentiation.

We identify the natural numbers with the finite von Neumann ordinals $\emptyset, {\emptyset}, \dots$ For the sake of consistency we will always write 0 instead of ∅.

2.2. Embedded Mostowski collapse

Recall that a directed graph with nodes U and edges E is well-founded if, for every non-empty subset S of U, there is a node y in S with no predecessors in S. It is extensional if no two distinct nodes have the same set of predecessors. We say that it is accessible pointed with sink a if there is a path from every node to a.1

¹
Aczel [1] defines an accessible pointed graph as one with a distinguished node from which every other node is reachable. Note that our paths run in the opposite direction.

The Mostowski graph of a set a is the directed graph $G (a) : = ⟨ [a], E ⟩$ with nodes $[a]$ and with edges $E = {⟨ x, y ⟩ \in {[a]}^{2} : x \in y}$ . Clearly $G (a)$ is well-founded, extensional and accessible pointed, with sink a. By well-foundedness and extensionality it also has exactly one source node, the empty set. On the other hand if G is any well-founded, extensional, accessible pointed graph then there is a unique set a, the Mostowski collapse of G, such that G is isomorphic to $G (a)$ . We denote this set a by $M (G)$ .

Definition 2.1.

A diagram is a pair $⟨ a, E ⟩$ of sets such that $⟨ x, y ⟩ \in E$ only if $x < y$ .

The diagram $⟨ a, E ⟩$ represents the graph with nodes $[a]$ and edges $E \cap {[a]}^{2}$ . We think of $⟨ a, E ⟩$ as a graph “embedded” in the Mostowski graph $G (a)$ of a, with edges that are forced to respect the ordering on $G (a)$ . An example of a diagram is the pair $⟨ a, \in ↾ {[a]}^{2} ⟩$ , representing $G (a)$ itself.

A diagram is automatically well-founded, by the condition on E. In general it is not accessible pointed or extensional; for example any nodes in $[a]$ outside the range of E will have the same, empty set of predecessors. However, if we restrict the graph to the set of nodes that are E-ancestors of a, then it is accessible pointed, with sink a. Furthermore, we can make it extensional by recursively collapsing together nodes with the same set of predecessors. We can then take the Mostowski collapse of the resulting graph. This procedure, which we call embedded Mostowski collapse, has a simple recursive definition:

Definition 2.2.

The embedded Mostowski collapse function $M (a, E)$ is defined by $\begin{matrix} M (a, E) = {M (b, E) : b < a \land ⟨ b, a ⟩ \in E} . \end{matrix}$

Notice that this is definable by ∈-recursion. We will almost always use Mostowski collapse in this form, so will often omit the word “embedded”.

We use $rank (x)$ to denote the von Neumann rank of the set x and $| x |$ to denote its cardinality.

Lemma 2.3.

$| [M (a, E)] | ⩽ | [a] |$ and $rank (M (a, E)) ⩽ rank (a)$ .

Definition 2.4.

We say b is embeddable in a if $b = M (a, E)$ for some E.

We interpret the embeddability of b in a as meaning that b is no more complex than a, in the sense that, for example, recursion over b is no more powerful than recursion over a. Lemma 9.4 shows that our notion of embeddability is the same as the one in [4].

2.3. The smash function

We repeat some definitions from [4].

Definition 2.5.
The set composition function $a ⊙ b$ is defined as follows. Given sets a and b, construct a graph H by drawing the graph $G (a)$ above the graph $G (b)$ and then identifying the source of $G (a)$ with the sink of $G (b)$ . Then $a ⊙ b = M (H)$ .

An equivalent recursive definition for set composition is: $\begin{matrix} a ⊙ b = \{\begin{matrix} b & if a = 0 \\ {x ⊙ b : x \in a} & if a \neq 0 . \end{matrix} \end{matrix}$
Definition 2.6.
The set smash function $a # b$ is defined as follows. Given sets a and b, construct a graph H by drawing a disjoint copy $G_{x}$ of $G (b)$ for every point $x \in G (a)$ , and then adding an edge from the sink of $G_{x}$ to the source of $G_{y}$ for every edge $⟨ x, y ⟩$ of $G (a)$ . Then $a # b = M (H)$ .

An equivalent recursive definition for set smash is $a # b = b ⊙ {x # b : x \in a}$ .

The smash function is a kind of cartesian product on Mostowski graphs. We introduce a corresponding “pairing function” $σ_{a, b} (x, y)$ , which we think of as taking nodes $x \in G (a)$ and $y \in G (b)$ and outputting the node corresponding to y in the x-th copy $G_{x}$ of $G (b)$ in H. Note that although we write a as a subscript in $σ_{a, b}$ we do not actually use a in the definition.
Definition 2.7.
We define $σ_{a, b} (x, y) = y ⊙ {z # b : z \in x}$ .
Lemma 2.8.
The function $⟨ x, y ⟩ \mapsto σ_{a, b} (x, y)$ is an order isomorphism between $[a] \times [b]$ , ordered lexicographically, and $[a # b]$ .
Definition 2.9.
We let $π_{1, a, b} : [a # b] \to [a]$ and $π_{2, a, b} : [a # b] \to [b]$ be projection functions inverting $σ_{a, b}$ , so that $σ_{a, b} (π_{1, a, b} (z), π_{2, a, b} (z)) = z$ for $z \in [a # b]$ .
Lemma 2.10.
For sets a and b,
$rank (a ⊙ b) = rank (b) + rank (a)$

$| tc (a ⊙ b) | = | tc (a) | + | tc (b) |$

$rank (a # b) + 1 = (rank (b) + 1) (rank (a) + 1)$

$| tc (a # b) | + 1 = (| tc (b) | + 1) (| tc (a) | + 1)$ , equivalently, $| [a # b] | = | [a] | \cdot | [b] |$ .

Definition 2.11.
A smash-term is a term built from variables, the constant 0 and the functions pairing, cartesian product, transitive closure, ⊙ and #.

Smash-terms will play the role usually played by polynomials in computational complexity, providing bounds for various complexity measures. Notice that the rank, and respectively the size of the transitive closure, of a smash-term is at most polynomially larger than those of its arguments. (The corresponding definition of #-term in [4] is stricter, only allowing variables, the constant 1, ⊙ and #.)
3. Subset-bounded recursion and CRSF

This section is modelled on the similar development of CRSF in [4].

Definition 3.1.
Let $g (\vec{a}, b, x)$ and $h (\vec{a}, b)$ be functions from sets to sets. The function $f (\vec{a}, b)$ is obtained from $g (\vec{a}, b, x)$ by subset-bounded recursion with bound $h (\vec{a}, b)$ if $\begin{matrix} f (\vec{a}, b) = g (\vec{a}, b, {f (\vec{a}, c) : c \in b}) \cap h (\vec{a}, b) . \end{matrix}$
Definition 3.2.
We take as initial functions
the constant 0

projection: $a_{1}, \dots, a_{n} \mapsto a_{j}$ for $1 ⩽ j ⩽ n$

pairing: $a, b \mapsto {a, b}$

union: $a \mapsto ⋃ a$

conditional: $\begin{matrix} {cond}_{\in} (a, b, c, d) = \{\begin{matrix} a & if c \in d \\ b & otherwise \end{matrix} \end{matrix}$

transitive closure: $a \mapsto tc (a)$

cartesian product: $a, b \mapsto a \times b$

set composition: $a, b \mapsto a ⊙ b$

set smash: $a, b \mapsto a # b$

embedded Mostowski collapse: $a, E \mapsto M (a, E)$ .

The above initial functions are roughly the same as the primitive symbols in the definition of Cobham recursive set functions given in [5], but with the addition of the embedded Mostowski collapse function.
Definition 3.3.
${CRSF}_{\subseteq}$ is defined as the closure of initial functions (1) to (9) under composition and subset-bounded recursion. ${CRSF}_{\subseteq}^{+}$ is defined as the closure of all of the initial functions above, including embedded Mostowski collapse, under composition and subset-bounded recursion.
Definition 3.4.
A ${CRSF}_{\subseteq}$ relation is a relation $φ (\vec{a})$ given by an expression of the form $g (\vec{a}) \neq 0$ where g is a ${CRSF}_{\subseteq}$ function. The ${CRSF}_{\subseteq}^{+}$ relations are defined similarly.
Lemma 3.5.
We derive some basic properties of ${CRSF}_{\subseteq}$ . These also hold with ${CRSF}_{\subseteq}^{+}$ in place of ${CRSF}_{\subseteq}$ .
${CRSF}_{\subseteq}$ contains the functions ${a}$ , $a \cup b$ and $\begin{matrix} {cond}_{=} (a, b, c, d) = \{\begin{matrix} a & if c = d \\ b & otherwise . \end{matrix} \end{matrix}$

The ${CRSF}_{\subseteq}$ relations are closed under Boolean operations.

${CRSF}_{\subseteq}$ is closed under separation. That is, if $φ (\vec{a}, c)$ is a ${CRSF}_{\subseteq}$ relation then the following function is also in ${CRSF}_{\subseteq}$ : $\begin{matrix} f (\vec{a}, b) = {c \in b : φ (\vec{a}, c)} . \end{matrix}$

The ${CRSF}_{\subseteq}$ relations are closed under $Δ_{0}$ quantification, in which quantifiers range over members of a given set.

${CRSF}_{\subseteq}$ contains the functions $⋂ a$ , $a ∖ b$ and $a \cap b$ . By convention $⋂ 0 = 0$ .

${CRSF}_{\subseteq}$ contains the usual pairing and projection functions for k-tuples, for $k \in N$ .

${CRSF}_{\subseteq}$ contains $σ_{a, b}$ and the projection functions $π_{1, a, b}$ and $π_{2, a, b}$ .

Proof.

We use ${a} = {a, a}$ and $a \cup b = ⋃ {a, b}$ . We define ${cond}_{=}$ as ${cond}_{\in} (a, b, c, {d})$ .

We define $\neg (g (\vec{a}) \neq 0)$ and $(f (\vec{a}) \neq 0) \lor (g (\vec{b}) \neq 0)$ respectively by ${cond}_{=} (1, 0, g (\vec{a}), 0) \neq 0$ and $f (\vec{a}) \cup g (\vec{b}) \neq 0$ .

Using ${cond}_{\in}$ , ${cond}_{=}$ and Boolean operations we can define functions by cases. Define $k (\vec{a}, b, c)$ by recursion on c as $\begin{matrix} k (\vec{a}, b, c) = \{\begin{matrix} {c} & if c \in b and φ (\vec{a}, c) \\ ⋃ {k (\vec{a}, b, d) : d \in c} & if c = b \\ 0 & otherwise . \end{matrix} \end{matrix}$ Then $k (\vec{a}, b, c) \subseteq b$ always, so k is definable by subset-bounded recursion with bound b. We put $f (\vec{a}, b) = k (\vec{a}, b, b)$ .

We can define the relation $\exists c \in b φ (\vec{a}, c)$ by $\begin{matrix} {c \in b : φ (\vec{a}, c)} \neq 0 \end{matrix}$ where the set on the left is given by separation.

We take $⋂ a = {x \in ⋃ a : \forall b \in a (x \in b)}$ , using separation. The other two are trivial.

Trivial.

We have $σ_{a, b} (x, y) = y ⊙ {z # b : z \in x}$ , where the set ${z # b : z \in x}$ can be obtained by separation, since it is a subset of $tc ([x # b])$ . For $z \in [a # b]$ we can define, for example, the projection function $π_{1, a, b}$ by $\begin{matrix} π_{1, a, b} (z) = ⋃ {x \in [a] : \exists y \in [b] σ_{a, b} (x, y) = z} \end{matrix}$ since exactly one x satisfies the condition on the right.
□
Lemma 3.6.
The rank function is in ${CRSF}_{\subseteq}^{+}$ .
Proof.
Given a set a, define $ρ (a)$ by first letting H be the transitive closure of $G (a)$ as a graph, that is, we start with $G (a)$ and add an edge $⟨ x, y ⟩$ whenever there is a path from x to y, and then letting $ρ (a)$ be the Mostowski collapse of H. Then $ρ (a)$ is an ordinal, since it is a transitive set of transitive sets. Furthermore, we can show by induction on a that $rank (ρ (a)) = rank (a)$ . We have $ρ (a) = {ρ (x) : x \in tc (a)}$ so $\begin{array}{l} rank (ρ (a)) & = sup {rank (y) + 1 : y \in ρ (a)} \\ = sup {rank (ρ (x)) + 1 : x \in tc (a)} \\ = sup {rank (x) + 1 : x \in tc (a)} \\ = rank (a) \end{array}$ It follows that $ρ (a) = rank (a)$ . This construction can be done in ${CRSF}_{\subseteq}^{+}$ by defining $ρ (a) = M (a, H)$ , where $H = {⟨ x, y ⟩ \in {[a]}^{2} : x < y}$ . □

Note that the graph H above is in general not extensional – for example, consider what happens to the nodes ${1}$ and 2 when $a = {{1}, 2}$ . This situation is similar to the appearance of a multi-valued embedding in the construction of the rank function in [4].
Lemma 3.7.
Ordinal addition and multiplication are in ${CRSF}_{\subseteq}^{+}$ .
Proof.
We know that $rank (a ⊙ b) = rank (b) + rank (a)$ and $rank (a # b) + 1 = (rank (b) + 1) (rank (a) + 1)$ , from Lemma 2.10. Hence the function $a + b = rank (b ⊙ a)$ gives us ordinal addition, and we can define ordinal multiplication by subset-bounded recursion as $\begin{matrix} a \cdot b = ⋃ {a \cdot c + a : c \in b} \cap rank (b # a) \end{matrix}$ since $a \cdot b \subseteq rank (b # a)$ for ordinals. □
Lemma 3.8.
For any ${CRSF}_{\subseteq}^{+}$ function f, we have $rank (f (\vec{a})) ⩽ p (rank (\vec{a}))$ and $| [f (\vec{a})] | ⩽ p (| [\vec{a}] |)$ for some polynomial p.
Proof.
This is a straightforward induction on the complexity of f. □
Corollary 3.9.
Ordinal exponentiation is not in ${CRSF}_{\subseteq}^{+}$ .
Corollary 3.10.
There is no ${CRSF}_{\subseteq}^{+}$ function which, on all hereditarily finite sets x, ouputs the ordinal $| x |$ .
Proof.
Let f be such a function. Take $n \in N$ and let a be its power set $P (n)$ , so $f (a)$ is the ordinal $2^{n}$ . Then $rank (a) = n + 1$ while $rank (f (a)) = 2^{n}$ . □

We conclude this section with a digression about the choice of initial functions and whether they are all necessary. It turns out that Mostowski collapse plays a more limited role in ${CRSF}_{\subseteq}^{+}$ than might be expected. We will show in Section 8 that for any function $f (\vec{a})$ in ${CRSF}_{\subseteq}^{+}$ , there is a smash-term $t (\vec{a})$ and a function $g (\vec{a})$ in ${CRSF}_{\subseteq}$ such that $f (\vec{a}) = M (t (\vec{a}), g (\vec{a}))$ . In other words, if we can compute a set in ${CRSF}_{\subseteq}^{+}$ , then we can already compute a diagram of it in ${CRSF}_{\subseteq}$ . In particular, Mostowski collapse is not needed if we are only interested in computing $0 / 1$ -valued functions.

We expect that we could do without cartesian product, since if we want to quantify over pairs in $a \times b$ we could instead quantify over elements of $[a # b]$ , using the function $σ_{a, b} (x, y)$ where we now use the ordered pair $⟨ x, y ⟩$ . This change would require some formal changes to our definitions of diagrams and Mostowski collapse, to make use of this new system.

In the full system ${CRSF}_{\subseteq}^{+}$ we do not need to include set composition as an initial function, since it is easy to construct the Mostowski graph of $a ⊙ b$ as a diagram embedded inside $a # b$ and then recover $a ⊙ b$ using Mostowski collapse.

The smash function would seem to play a central role in introducing polynomial growth rate functions. Nonetheless, there is a natural way to extend embedded Mostowski collapse which removes the need for the smash function. For $k \in N$ , define k-embedded Mostowski collapse as $\begin{matrix} M_{k} (⟨ \vec{a} ⟩, E) = {M_{k} (⟨ \vec{b} ⟩, E) : ⟨ \vec{b} ⟩ <_{k} ⟨ \vec{a} ⟩ \land ⟨ ⟨ \vec{b} ⟩, ⟨ \vec{a} ⟩ ⟩ \in E} \end{matrix}$ where $⟨ \vec{a} ⟩, ⟨ \vec{b} ⟩$ are k-tuples and $<_{k}$ is the lexicographic ordering given by <. We can use the order-isomorphism between ${[a]}^{k}$ under $<_{k}$ and $[a # \dots # a]$ (with k occurrences of a) under < to define $M_{k}$ in ${CRSF}_{\subseteq}^{+}$ . In the other direction, it is straightforward to define the smash function using $M_{2}$ , so the class ${CRSF}_{\subseteq}^{+}$ is unchanged if we remove smash and set composition and replace M with $M_{2}$ . For more on $<_{k}$ and $M_{k}$ , see Section 10.
4. Turing machines

We consider a simple model of infinite-time Turing machines [7]. The usual finite Turing machines are special cases of the definition below, obtained by considering only finite ordinals and skipping any text containing the word “limit”.

We simulate machines operating on strings of symbols from a finite alphabet of numerals $0, \dots, k - 1$ . These strings may be finite, but more generally will have ordinal length. We need to specify how to code such strings as sets, so that we can manipulate them with ${CRSF}_{\subseteq}^{+}$ functions. We do this in a straightforward way by letting a string of length $λ ⩽ ω$ be formally a function $λ \to k$ and dealing with this directly as a set-theoretic function, that is, as a set of ordered pairs.2

²
There are other ways of handling this. In particular, over the binary alphabet we could code strings of length λ simply as subsets of λ. We do not use this encoding here, partly to avoid issues of how to mark the end of a string, but we will use it beginning in Section 5.1 where we will be dealing with strings of fixed size. An alternative where we explicitly record the length λ would be to code binary strings $a_{0} a_{1} \dots$ as pairs $⟨ λ, {i < λ : a_{i} = 1} ⟩$ . This would be essentially equivalent to the coding used in the current section, since there are ${CRSF}_{\subseteq}^{+}$ functions translating in both directions between them.

Consider a Turing machine A with a single, one-way tape, m states, and k symbols. We will simulate the machine running on a tape of length $λ ⩽ ω$ for time τ, where λ and τ are ordinals (that is, λ will be either finite or ω). A configuration of the machine is a triple $⟨ W, i, s ⟩$ where the string W is the contents of the tape, i is the position of the head and s is the state.

At each step $σ + 1$ , machine A reads the symbol that was under the head in step σ, then writes a symbol, changes state and moves the head, all according to the transition function (as usual).

At limit steps σ, we set the symbol in each cell j in W to be the highest symbol that occurs cofinally often in cell j as we range over the earlier configurations. We change the state s to a distinguished limit state and move the head to $i = 0$ .

Let ${Config}_{A} (λ, I, τ)$ be the function that takes as inputs ordinals $λ ⩽ ω$ and τ, and a string I of ordinal length $⩽ λ$ , and outputs the configuration of the machine A with tape length λ after running for τ steps on input I.

Lemma 4.1.

${Config}_{A}$ is in ${CRSF}_{\subseteq}$ .

Proof.

${Config}_{A}$ can be defined by a straightforward recursion. The only technical issue is to make sure that the intermediate values in the recursion are all subsets of a set we can construct. We assume that λ and τ are ordinals and will write < rather than ∈ for membership in an ordinal.

Let $F (λ, I, τ)$ be the function that, on well-formed inputs, outputs $\begin{matrix} {τ} \times W \times {i} \times {s} = {⟨ τ, a, i, s ⟩ : a \in W} \end{matrix}$ where $⟨ W, i, s ⟩$ is the configuration of M at step τ. Then $\begin{matrix} F (λ, I, τ) \subseteq {τ} \times (λ \times k) \times λ \times m \end{matrix}$ so we can potentially define F directly by subset-bounded recursion. To do so, we must show how to compute $F (λ, I, τ)$ from $S = {F (λ, I, σ) : σ < τ}$ . Observe that for $σ < τ$ we can recover $F (λ, I, σ)$ from S as the subset of $⋃ S$ consisting of elements with first component σ. In particular we can recover the tape contents $W_{σ}$ at step σ by separation as $\begin{matrix} W_{σ} = {a \in λ \times k : \exists i < λ \exists s < m ⟨ σ, a, i, s ⟩ \in ⋃ S} \end{matrix}$ and can similarly recover the head position $i_{σ}$ and the state $s_{σ}$ .

If $τ = 0$ then we let $i = 0$ , let s be the starting state, and let W be the input string I, padded out as necessary to length λ with pairs $⟨ j, 0 ⟩$ (assuming without loss of generality that the symbol 0 stands for “blank”). If $σ : = ⋃ τ \in τ$ then τ is the successor ordinal $σ + 1$ . Using $W_{σ}$ , $i_{σ}$ , $s_{σ}$ and the transition function of M, we compute W using separation and change i and s appropriately.

Otherwise τ is a limit. We let s be the limit state and let $i = 0$ . The set of symbols occurring cofinally often in cell j is $\begin{matrix} X_{j} = {x < k : \forall σ < τ \exists σ^{'} < τ (σ < σ^{'} \land ⟨ j, x ⟩ \in W_{σ^{'}})} . \end{matrix}$ Hence $⋃ X_{j}$ is the maximum symbol that occurs cofinally often, and we can let $W = {a \in λ \times k : a = ⟨ j, ⋃ X_{j} ⟩}$ .

This shows that F is in ${CRSF}_{\subseteq}$ . The lemma follows. □

As usual, ${0, 1}^{*}$ denotes the set of finite binary strings.

Theorem 4.2.

Every polynomial time function from ${0, 1}^{*}$ to ${0, 1}^{*}$ is in ${CRSF}_{\subseteq}^{+}$ .

Proof.

Suppose f is computed by a Turing machine A which halts in time $n^{c}$ on inputs of length $n > 1$ . Given a finite string w, in ${CRSF}_{\subseteq}^{+}$ we can compute the length n of w as ${i \in ⋃ ⋃ w : \exists x < k ⟨ i, x ⟩ \in w}$ . We then compute $n^{c}$ (using Lemma 3.7) and ${Config}_{A} (n^{c}, w, n^{c})$ , and the output of f can easily be obtained from this. □

The only use of Mostowski collapse in the proof of Theorem 4.2 is to obtain $n^{c}$ from n. If we instead let $m = n # \dots # n$ (where n appears c times) then m is order-isomorphic to ${(n + 1)}^{c} - 1$ , and we can prove a version of Lemma 4.1 that avoids using Mostowski collapse, by simulating Turing machine computations of length $n^{c}$ using ∈-recursion on m rather than on $n^{c}$ . All that prevents us from carrying out the whole proof of the theorem in this way is that, under our coding of binary strings as sets, we must be able to convert the output into a sequence indexed by an ordinal. This is not a problem for very simple outputs, so we have:

Theorem 4.3.

Every polynomial time relation on ${0, 1}^{*}$ is in ${CRSF}_{\subseteq}$ .

As a converse of Theorem 4.2 we have the following.

Theorem 4.4.

Every ${CRSF}_{\subseteq}^{+}$ function from ${0, 1}^{*}$ to ${0, 1}^{*}$ is in polynomial time.

Proof.

We use the same argument as [4]. The theorem follows from the more general observation that for any ${CRSF}_{\subseteq}^{+}$ function $f (x_{1}, \dots, x_{r})$ there is a polynomial time function which, for any hereditarily finite sets $a_{1}, \dots, a_{r}$ , given graphs $G (a_{1}), \dots, G (a_{r})$ outputs $G (f (a_{1}, \dots, a_{r}))$ (up to graph isomorphism) using the standard encoding of directed graphs as strings. This is proved by induction on the complexity of f. The bound on recursion guarantees that the sizes of the graphs involved do not grow too fast. □

We now move to infinite-time machines. Following [12], a function from ${0, 1}^{ω}$ to ${0, 1}^{ω}$ is polynomial time if it is computed by an infinite-time Turing machine with three tapes (an input tape, an output tape and a working tape) which always halts after at most $ω^{d}$ steps, for some fixed exponent $d \in N$ . Theorem 4.5.

Every polynomial time function from ${0, 1}^{ω}$ to ${0, 1}^{ω}$ is in ${CRSF}_{\subseteq}$ .

Proof.

This is proved in the same way as Theorem 4.3, with minor changes to accommodate simulating three tapes rather than one. Since the output sequence is a subset of $ω \times 2$ , we can use separation to construct it from the output of ${Config}_{M}$ and do not need Mostowski collapse. □

Theorem 4.6.

Every ${CRSF}_{\subseteq}^{+}$ function from ${0, 1}^{ω}$ to ${0, 1}^{ω}$ is polynomial time.

Proof.

It is shown in [3] that every such function from ${0, 1}^{ω}$ to ${0, 1}^{ω}$ in the class SRSF is polynomial time. By results in [4] and in Section 9 below, every function in ${CRSF}_{\subseteq}^{+}$ is in SRSF. □

5. Bisimilarity and coding

This section discusses the generalized notion of binary strings, bisimulation, and how to code collections of sets.

5.1. a-Strings

Definition 5.1.
Let a be any set. An a-string is a subset of a.

We will sometimes informally identify an a-string with its characteristic function $a \to {0, 1}$ . In this sense, for finite ordinals k, the usual binary strings in ${0, 1}^{k}$ of complexity theory correspond to the k-strings. For example, the binary string $01101 \in {0, 1}^{5}$ corresponds to the 5-string ${0, 2, 3}$ (writing the most significant bit on the left).

For us, the most important use of a-strings is to encode sets via a Mostowski collapse:
Definition 5.2.
We say that a diagram $⟨ a, E ⟩$ codes the set $M (a, E)$ . If a is fixed and E is an ${[a]}^{2}$ -string, we say E codes the set $M (a, E)$ .

This way of coding sets, as a size parameter a together with an ${[a]}^{2}$ -string E, is designed to work well with subset-bounded recursion.
5.2. Bisimilarity

We will frequently need to recognize when two diagrams code the same set even in situations where the Mostowski collapse function is not available. If we are dealing with extensional, accessible pointed diagrams, then two such diagrams code the same set if and only if they are isomorphic. However our diagrams are typically neither, so we will instead use the notion of bisimilarity (see for example [1]). This is very well-behaved on well-founded graphs.

Definition 5.3.
A bisimulation between directed graphs G and H is a relation ∼ relating nodes of G to nodes of H, such that for all nodes u in G and v in H, $u \sim v$ holds if and only if both of the following hold:
For every predecessor $u^{'}$ of u in G, there is a predecessor $v^{'}$ of v in H such that $u^{'} \sim v^{'}$

For every predecessor $v^{'}$ of v in H, there is a predecessor $u^{'}$ of u in G such that $u^{'} \sim v^{'}$ .

Recall that a diagram $⟨ a, E ⟩$ represents the directed graph with nodes $[a]$ and edges ${[a]}^{2} \cap E$ . Definition 5.4.
We say that two diagrams $⟨ a, E ⟩$ and $⟨ b, F ⟩$ are bisimilar if there is a bisimulation ∼ between $⟨ a, E ⟩$ and $⟨ b, F ⟩$ such that $a \sim b$ .
Lemma 5.5.
There is at most one bisimulation between two diagrams.
Proof.
Suppose $\sim_{1}$ and $\sim_{2}$ are distinct bisimulations between diagrams $⟨ a, E ⟩$ and $⟨ b, F ⟩$ . Choose u <-minimal in $[a]$ such that there is a $v \in [b]$ for which $\sim_{1}$ and $\sim_{2}$ differ on the pair $⟨ u, v ⟩$ , and fix a <-minimal such v. Then $\sim_{1}$ and $\sim_{2}$ agree on all predecessors of u and v. Therefore, by the definition of a bisimulation, they must agree on $⟨ u, v ⟩$ , giving a contradiction. □
Lemma 5.6.
Given diagrams $⟨ a, E ⟩$ , $⟨ b, F ⟩$ , there is at least one bisimulation between them, and they are bisimilar if and only if $M (a, E) = M (b, F)$ .
Proof.
Define a relation ∼ by $u \sim v$ if and only if $M (u, E) = M (v, F)$ . It follows directly from the definitions that this is a bisimulation between $⟨ a, E ⟩$ and $⟨ b, F ⟩$ . We then apply Lemma 5.5. □
Lemma 5.7.
There is a ${CRSF}_{\subseteq}$ function $B (a, E, b, F)$ computing the bisimulation between diagrams $⟨ a, E ⟩$ and $⟨ b, F ⟩$ , by outputting the bisimulation as a set of ordered pairs.
Proof.
First observe that $B (a, E, b, F) \subseteq [a] \times [b]$ , so we can potentially define B directly by a subset-bounded recursion. We will use recursion on a. Given a set $S = {\sim_{c} : c \in a}$ , where each $\sim_{c}$ is the bisimulation between $⟨ c, E ⟩$ and $⟨ b, F ⟩$ output by $B (c, E, b, F)$ , let $\sim = ⋃ S$ . Then by the uniqueness of bisimulations, $\sim \cap ([c] \times [b]) = \sim_{c}$ for every $c \in a$ . It follows that ∼ has all the properties of a bisimulation between $⟨ a, E ⟩$ and $⟨ b, F ⟩$ except possibly at a, and we can extend ∼ to a by adding a pair $⟨ a, y ⟩$ for every $y \in [b]$ which satisfies both conditions from Definition 5.3. □

5.3. Coding collections of sets

We use a generalized notion of a 0/1 matrix to allow a single set W to encode a collection of sets. The intuition is that the pairs $⟨ c, x ⟩$ in W encode the Mostowski graph of the c-th set encoded by W.

Definition 5.8.
For sets W and c, we define the c-th row of W, denoted $W^{(c)}$ , as the set ${x : ⟨ c, x ⟩ \in W}$ .

Note that $W^{(c)} \subseteq ⋃ ⋃ W$ , so the function $W, c \mapsto W^{(c)}$ is in ${CRSF}_{\subseteq}$ by separation. The next lemma allows us to use such a matrix to code a set of sets. Lemma 5.9.
The function $f (W, a, b) = {M (a, W^{(c)}) : c \in b}$ is in ${CRSF}_{\subseteq}^{+}$ .
Proof.
Let $e = b # a$ . Our strategy is to construct from W a single embedded graph $⟨ e, E ⟩$ such that $f (W, a, b) = M (e, E)$ . We will write σ, $π_{1}$ , $π_{2}$ for the functions $σ_{b, a}$ , $π_{1, b, a}$ , $π_{2, b, a}$ . Define $\begin{matrix} E^{'} = {⟨ u, v ⟩ \in {[e]}^{2} : π_{1} (u) = π_{1} (v) \neq b \land ⟨ π_{2} (u), π_{2} (v) ⟩ \in W^{(π_{1} (u))}} . \end{matrix}$ For each $c < b$ this puts the structure of $W^{(c)} \cap {[a]}^{2}$ onto copy c of the graph of a inside the graph of e, so that $M (σ (c, a), E^{'}) = M (a, W^{(c)})$ . On the other hand $σ (b, a) = e$ is not connected to anything in $E^{'}$ , so $M (e, E^{'}) = 0$ . Let $E = E^{'} \cup {⟨ σ (c, a), e ⟩ : c \in b}$ . Then $M (e, E)$ equals ${M (σ (c, a), E^{'}) : c \in b}$ , which is the required set. □

6. Boolean circuits

This section defines computations with unbounded fan-in Boolean circuits encoded by sets. We first introduce circuits that compute functions mapping strings to strings. We then extend this to circuits computing set functions, which operate on sets encoded as diagrams or strings. The set value that is computed by the circuit will be extracted from its output using the embedded Mostowski collapse.

Definition 6.1.
A circuit is a triple $⟨ c, E, λ ⟩$ where $⟨ c, E ⟩$ is a diagram and λ is a function from $[c]$ to the set of symbols ${0, 1, , ⋀, ⋁, \neg}$ (which we identify with the numbers $0, \dots, 5$ ) such that each node labelled ¬ has exactly one E-predecessor. The nodes labelled ∗ are called input nodes. We say that the circuit has size c.

Conjuctions and disjunctions may have arbitrary fan-in. The labels 0 and 1 represent the constant values False* and True.
Definition 6.2.
Let $C = ⟨ c, E, λ ⟩$ be a circuit, and let a be its set of input nodes. Given any a-string A, a computation of C on A is a $[c]$ -string W which, informally, assigns $0 / 1$ values to the nodes of C in such a way that each input node gets the same value that it has in A, and all other nodes get values according to the usual interpretations of their symbols in a circuit. That is, for all $u \in [c]$ ,
if $λ (u) = 0$ then $u \notin W$

if $λ (u) = 1$ then $u \in W$

if $λ (u) = $ then $u \in W \leftrightarrow u \in A$

if $λ (u) = ⋀$ then $u \in W \leftrightarrow \forall v < u (⟨ v, u ⟩ \in E \to v \in W)$

if $λ (u) = ⋁$ then $u \in W \leftrightarrow \exists v < u (⟨ v, u ⟩ \in E \land v \in W)$

if $λ (u) = \neg$ then $u \in W \leftrightarrow \exists v < u (⟨ v, u ⟩ \in E \land v \notin W)$ .

In general, to guarantee that a circuit has a computation it is enough for the graph underlying the circuit to be well-founded. However we need the extra condition that the graph is embedded in c for the next lemma.
Lemma 6.3.
There is a* ${CRSF}_{\subseteq}$ function which takes a circuit C and an a-string A, as in Definition 6.2 , and outputs a computation of C on A.
Proof.
Let $f (C, A, v)$ be the function that outputs a $[v]$ -string assigning correct values to all nodes $u ⩽ v$ in the circuit. Since $f (C, A, v) \subseteq [v]$ it is possible to define f directly by subset-bounded recursion. Suppose we are given $S = {f (C, A, u) : u \in v}$ . Then $W^{'} = ⋃ S$ assigns the correct values to all nodes u of the circuit with $u < v$ , and since $⟨ c, E ⟩$ is a diagram, this includes all nodes such that $⟨ u, v ⟩ \in E$ . Hence we have enough information to extend $W^{'}$ to a $[v]$ -string W which also assigns the correct value to v, and clearly this can be done in ${CRSF}_{\subseteq}$ . □

We extend the definition to handle computations on tuples of strings. When c, $a_{1}, \dots, a_{k}$ and p are finite ordinals, the following is equivalent to the usual definition of a finite Boolean circuit.
Definition 6.4.
A circuit with input sizes $a_{1}, \dots, a_{k}$ and output size p is a tuple $⟨ c, E, λ, \vec{a}, p, μ, ν ⟩$ where $⟨ c, E, λ ⟩$ is a circuit and we are also given
A partial function $μ : [c] \to ({0} \times a_{1}) \cup \dots \cup ({k - 1} \times a_{k})$ which maps every input node to a member of (a disjoint copy of) some $a_{i}$ , and

A function $ν : p \to [c]$ which maps every element of p to some node in $[c]$ . We call the range of ν the output nodes.

Definition 6.5.
The circuit evaluation function takes inputs $C, \vec{A}$ where $C = ⟨ c, E, λ, \vec{a}, p, μ, ν ⟩$ is a circuit and $\vec{A}$ is a tuple of strings, with each $A_{i}$ an $a_{i}$ -string. It outputs the p-string $C (\vec{A})$ computed by C on inputs $\vec{A}$ .
Lemma 6.6.
The circuit evaluation function is in ${CRSF}_{\subseteq}$ .
Proof.
We construct a computation W of the circuit as in the proof of Lemma 6.3. We recover the output by separation as ${i \in p : ν (i) \in W}$ . □
Definition 6.7.
A family $C_{\vec{a}}$ of circuits parametrized by a tuple $\vec{a}$ of sets is small if there are smash-terms $s, t, u_{1}, \dots, u_{k}$ such that the size of $C_{\vec{a}}$ is $s (\vec{a})$ , and $C_{\vec{a}}$ has input sizes $u_{1} (\vec{a}), \dots, u_{k} (\vec{a})$ and output size $t (\vec{a})$ . We say that a family $C_{\vec{a}, \vec{b}}$ is small with size bounds independent of $\vec{b}$ if the parameters $\vec{b}$ do not appear in any of these smash-terms.

Consider a set function $f (x)$ which, when its inputs are sets embeddable in a, outputs a set embeddable in p. Using diagrams, we can code the inputs and output of f respectively as ${[a]}^{2}$ -strings and ${[p]}^{2}$ -strings. We can then ask whether the corresponding function from strings to strings is computed by a small circuit.
Definition 6.8.
Let $f (x_{1}, \dots, x_{k})$ be any set function and let $a_{1}, \dots, a_{k}$ be a tuple of sets. Suppose that C is a circuit with input sizes ${[a_{1}]}^{2}, \dots, {[a_{k}]}^{2}$ and output size ${[p]}^{2}$ for some p, such that for every tuple $E_{1}, \dots, E_{k}$ of strings, with each $E_{i}$ an ${[a_{i}]}^{2}$ -string, we have $\begin{matrix} M (p, C (E_{1}, \dots, E_{k})) = f (M (a_{1}, E_{1}), \dots, M (a_{k}, E_{k})) \end{matrix}$ where $C (E_{1}, \dots, E_{k})$ is the ${[p]}^{2}$ -string as defined in Lemma 6.6. Then we say that C computes f on sets embeddable in $a_{1}, \dots, a_{k}$ .

We say that f has small circuits if there is a family $C_{\vec{a}}$ of small circuits such that, for all $\vec{a}$ , $C_{\vec{a}}$ computes f on sets embeddable in $\vec{a}$ .

We next describe a class of simple formulas, which we will use both for constructing circuits and to define a notion of uniformity for circuits. Note that the terms in the language below are exactly the smash-terms.
Definition 6.9.
A $Δ_{0}^{#}$ formula is a formula in the language ${\in, 0, pairing, tc, \times, ⊙, #}$ in which all quantifiers are bounded, of the form $\exists x < t$ or $\forall x < t$ . We say that a family of sets is $Δ_{0}^{#}$ -definable (with parameters $\vec{z}$ ) if there is a $Δ_{0}^{#}$ formula φ and a smash-term t such that the sets in the family have the form ${u \in t (\vec{z}) : φ (u, \vec{z})}$ .
Definition 6.10.
A family $C_{\vec{z}}$ of circuits is $Δ_{0}^{#}$ -uniform if it is small and the sets $E \subseteq {[c]}^{2}$ , $λ \subseteq [c] \times 6$ , $μ \subseteq [c] \times (({0} \times a_{1}) \cup \dots \cup ({k - 1} \times a_{k}))$ and $ν \subseteq p \times [c]$ describing the circuit $C_{\vec{z}}$ are all $Δ_{0}^{#}$ -definable with parameters $\vec{z}$ .

Below, to save space we will write e.g. “ $a_{1}, \dots, a_{k}$ -strings $A_{1}, \dots, A_{k}$ ” instead of “an $a_{1}$ -string $A_{1}$ , an $a_{2}$ -string $A_{2}$ , …” etc.

The next lemma states that the truth-sets of certain kinds of $Δ_{0}^{#}$ formulas can be computed by $Δ_{0}^{#}$ -uniform circuits. This is a crucial tool underlying the proof in Section 7 that ${CRSF}_{\subseteq}^{+}$ has small circuits.
Lemma 6.11.
Let φ be a $Δ_{0}^{#}$ formula $\begin{matrix} φ (x_{1}, \dots, x_{ℓ}, a_{1}, \dots, a_{m}, b_{1}, \dots, b_{n}, U_{1}, \dots, U_{k}) \end{matrix}$ in which all occurrences of variables $U_{i}$ are immediately to the right of an ∈ symbol in an atomic formula of the form $t \in U_{i}$ , and in which only variables $a_{i}$ can appear in terms bounding quantifiers. It is not necessary that all the variables are present in φ. Let $t (\vec{a}), s_{1} (\vec{a}), \dots, s_{k} (\vec{a})$ be smash-terms.

There is a $Δ_{0}^{#}$ -uniform family of circuits $C_{\vec{a}, \vec{b}}$ with size bounds independent of $\vec{b}$ , with input sizes $s_{1} (\vec{a}), \dots, s_{k} (\vec{a})$ and output size $t (\vec{a})$ , such that for all $\vec{a}$ and $\vec{b}$ and all $s_{1} (\vec{a}), \dots, s_{k} (\vec{a})$ -strings $U_{1}, \dots, U_{k}$ we have $\begin{matrix} C_{\vec{a}, \vec{b}} (\vec{U}) = {⟨ \vec{x} ⟩ \in t (\vec{a}) : φ (\vec{x}, \vec{a}, \vec{b}, \vec{U})} . \end{matrix}$
Proof.
We fix m, n and k and use induction on the complexity of φ. Circuits will be given with descriptions that can easily be turned into $Δ_{0}^{#}$ formulas.

Suppose φ has the form $r_{1} (\vec{x}, \vec{a}, \vec{b}) \in r_{2} (\vec{x}, \vec{a}, \vec{b})$ for terms $r_{1}, r_{2}$ . We compute the $t (\vec{a})$ -string $\begin{matrix} {⟨ \vec{x} ⟩ \in t (\vec{a}) : r_{1} (\vec{x}, \vec{a}, \vec{b}) \in r_{2} (\vec{x}, \vec{a}, \vec{b})} \end{matrix}$ using a circuit of size $t (\vec{a})$ . Each node $u \in [t (\vec{a})]$ of the circuit is labelled 1 if $u = ⟨ \vec{x} ⟩$ for some $\vec{x}$ with $r_{1} (\vec{x}, \vec{a}, \vec{b}) \in r_{2} (\vec{x}, \vec{a}, \vec{b})$ , and is otherwise labelled 0 (there are no input nodes or nodes labelled with connectives). The set E of edges is empty. The function ν mapping elements of the output size $t (\vec{a})$ to output nodes is just the identity.

The case where φ has the form $r (\vec{x}, \vec{a}, \vec{b}) \in U_{i}$ is broadly similar. This time each node $u \in [t (\vec{a})]$ is labelled with a ∗ (that is, as an input node) if $u = ⟨ \vec{x} ⟩$ for some $\vec{x}$ with $r (\vec{x}, \vec{a}, \vec{b}) \in s_{i} (\vec{a})$ , and is otherwise labelled 0. The output is arranged as in the previous case. The function μ mapping input nodes to the disjoint union of input sizes maps $⟨ \vec{x} ⟩$ to $⟨ i - 1, r (\vec{x}, \vec{a}, \vec{b}) ⟩$ (we use $i - 1$ to match the notation in Definition 6.4), with the result that a computation W assigns 1 to $⟨ \vec{x} ⟩$ if and only if $r (\vec{x}, \vec{a}, \vec{b}) \in U_{i}$ .

Suppose φ has the form $φ_{1} \land φ_{2}$ . Let $C_{1}$ and $C_{2}$ be circuits for respectively $\begin{matrix} {⟨ \vec{x} ⟩ \in t (\vec{a}) : φ_{1} (\vec{x}, \vec{a}, \vec{b}, \vec{U})} and {⟨ \vec{x} ⟩ \in t (\vec{a}) : φ_{2} (\vec{x}, \vec{a}, \vec{b}, \vec{U})} \end{matrix}$ with sizes $c_{1} = c_{1} (\vec{a})$ and $c_{2} = c_{2} (\vec{a})$ . We define a circuit D with size $d = t (\vec{a}) ⊙ {c_{2}} ⊙ {c_{1}}$ . This means that the underlying graph of D consists of a copy of $G (c_{1})$ at the bottom, with a copy of $G (c_{2})$ above it, and a copy of $G (t (\vec{a}))$ above that, with the sink node of each component connected to the source node of the next component. We will call the components $C_{1}^{'}$ , $C_{2}^{'}$ and O. The labellings, edges and connections to inputs in $C_{1}^{'}$ are copied from $C_{1}$ , and similarly for $C_{2}^{'}$ and $C_{2}$ . So, for example, if $C_{2}$ has an edge $⟨ u, v ⟩$ then D has an edge $⟨ u ⊙ {c_{1}}, v ⊙ {c_{1}} ⟩$ . The function ν maps every element of the output size $t (\vec{a})$ to the corresponding node of O, that is, $ν : u \mapsto u ⊙ {c_{2}} ⊙ {c_{1}}$ , and these nodes in the image of ν are labelled with ⋀. The other nodes of O are labelled with 0 and are not used. Finally, in the original circuits each $u \in t (\vec{a})$ was associated with an output node $ν_{1} (u)$ in $C_{1}$ and an output node $ν_{2} (u)$ in $C_{2}$ . In D we connect each node $u ⊙ {c_{2}} ⊙ {c_{1}}$ labelled ⋀ in O to the nodes of D corresponding to $ν_{1} (u)$ and $ν_{2} (u)$ , that is, to $ν_{1} (u)$ in $C_{1}^{'}$ and $ν_{2} (u) ⊙ {c_{1}}$ in $C_{2}^{'}$ .

Suppose φ has the form $\forall x^{'} \in s (\vec{a}) ψ (x^{'}, \vec{x}, \vec{a}, \vec{b}, \vec{U})$ . Let C be a circuit for $\begin{matrix} {⟨ x^{'}, \vec{x} ⟩ \in s (\vec{a}) \times t (\vec{a}) : ψ (x^{'}, \vec{x}, \vec{a}, \vec{b}, \vec{U})} \end{matrix}$ with size $c = c (\vec{a})$ . We construct a circuit D of size $t (\vec{a}) ⊙ {c}$ , consisting of C with a copy O of $G (t (\vec{a}))$ above it, similarly to the previous case. For the output nodes of D we take all nodes $u ⊙ {c}$ in O for $u \in t (\vec{a})$ , and label them with ⋀. If such a node has the form $⟨ \vec{x} ⟩ ⊙ {c}$ , we connect it by an edge to every output node $ν_{C} (⟨ x^{'}, \vec{x} ⟩)$ in C with $x^{'} \in s (\vec{a})$ , where $ν_{C}$ is C’s function mapping elements of its output size $s (\vec{a}) \times t (\vec{a})$ to its output nodes.

Negation is handled similarly. □

We finish this section by giving three concrete examples of families of small uniform circuits, all of which we will need in the next section. The first example, union, is now an easy consequence of Lemma 6.11. The other two, circuits for computing bisimilarity and the ancestor relation, are more complicated.
Lemma 6.12.
The union function has $Δ_{0}^{#}$ -uniform circuits.
Proof.
Let $⟨ a, E ⟩$ be a diagram. Let the ${[a]}^{2}$ -string F be defined from the ${[a]}^{2}$ -string E by $\begin{matrix} ⟨ x, y ⟩ \in F \Leftrightarrow \{\begin{matrix} ⟨ x, y ⟩ \in E & if y \neq a \\ \exists z \in [a], ⟨ x, z ⟩ \in E \land ⟨ z, a ⟩ \in E & if y = a . \end{matrix} \end{matrix}$ Then $M (a, F) = ⋃ M (a, E)$ . The result follows by Lemma 6.11. □

For the next two examples we will need a technical lemma, to help construct circuits defined using smash. Lemma 6.13.
For $x \in [a]$ , $y \in [b]$ and $w \in [a # b]$ the relation $σ_{a, b} (x, y) = w$ is definable by a $Δ_{0}^{#}$ formula which uses only terms in a and b as bounds on quantifiers.
Proof.
We have $σ_{a, b} (x, y) = w$ if and only if $w = y ⊙ {z # b : z \in x}$ , which holds if and only if $\begin{matrix} \exists s \in [w], w = y ⊙ s \land s = {z # b : z \in x} . \end{matrix}$ This is $Δ_{0}^{#}$ -definable, and we can bound all quantifiers by $[a # b] \cup [a]$ . □
Lemma 6.14.
There is a family $C_{a, b}$ of $Δ_{0}^{#}$ -uniform circuits, with input sizes ${[a]}^{2}$ and ${[b]}^{2}$ and with output size $[a] \times [b]$ , which take an ${[a]}^{2}$ -string E and a ${[b]}^{2}$ -string F and output a string giving the bisimulation between diagrams $⟨ a, E ⟩$ and $⟨ b, F ⟩$ .
Proof.
We will imitate the recursion on a used to show that bisimilarity is in ${CRSF}_{\subseteq}$ in Lemma 5.7. For $u \in [a]$ we write $\sim_{u}$ for the bisimulation between $⟨ u, E ⟩$ and $⟨ b, F ⟩$ , which we treat as a $[a] \times [b]$ -string.

Let $R_{u} = ⋃ {\sim_{u^{'}} : u^{'} \in u}$ . Then for $⟨ x, y ⟩ \in [a] \times [b]$ we have $⟨ x, y ⟩ \in \sim_{u}$ if and only if either $⟨ x, y ⟩ \in R_{u}$ , or $x = u$ and the conditions from Definition 5.3 hold, that is, $\begin{array}{l} \forall x^{'} \in [a] (⟨ x^{'}, x ⟩ \in E \to \exists y^{'} \in [b] (⟨ y^{'}, y ⟩ \in F \land ⟨ x^{'}, y^{'} ⟩ \in R_{u})) \\ \land \forall y^{'} \in [b] (⟨ y^{'}, y ⟩ \in F \to \exists x^{'} \in [a] (⟨ x^{'}, x ⟩ \in E \land ⟨ x^{'}, y^{'} ⟩ \in R_{u})) . \end{array}$ Thus $\sim_{u}$ is expressed by a $Δ_{0}^{#}$ formula to which we can apply Lemma 6.11, giving $Δ_{0}^{#}$ -uniform circuits $C_{a, b, u}$ computing $\sim_{u}$ from E, F and $R_{u}$ , with size bounds independent of u. Let $t = t (a, b)$ be the size of $C_{a, b, u}$ and let $λ_{u}$ , $μ_{u}$ and $ν_{u}$ be the functions describing respectively its internal, input and output gates.

Our circuit C which computes bisimulations has size $a # t$ and functions λ, μ and ν. It is formed as follows. For each $u \in [a]$ :
C has an edge $⟨ σ_{a, t} (u, x), σ_{a, t} (u, y) ⟩$ for each edge $⟨ x, y ⟩$ in $C_{a, b, u}$ .

For each $x \in [t]$ , the internal gate $λ (σ_{a, t} (u, x))$ is the same as $λ_{u} (x)$ .

For each $x \in [t]$ , if $μ_{u} (x) = ⟨ 0, z ⟩$ for $z \in {[a]}^{2}$ (representing an input from E) or if $μ_{u} (x) = ⟨ 1, z ⟩$ for $z \in {[b]}^{2}$ (representing an input from F) then $σ_{a, t} (u, x)$ is an input node of C and $μ (σ_{a, t} (u, x)) = μ_{u} (x)$ .
In other words via the map $x \mapsto σ_{a, t} (u, x)$ the u-th copy of t inside $a # t$ , which we will call $C_{u}$ , is given the same internal structure as $C_{a, b, u}$ and accesses inputs from E and F in the same way. Then:
For each $x \in [t]$ , if $μ_{u} (x) = ⟨ 2, z ⟩$ for $z \in [a] \times [b]$ (representing an input from $R_{u}$ ) then $λ (σ_{a, t} (u, x)) = ⋁$ and for each $u^{'} \in u$ there is an edge in C connecting $σ_{a, t} (u, x)$ with the “output node” of $C_{u^{'}}$ corresponding to z, that is, the node $σ_{a, t} (u^{'}, ν_{u^{'}} (z))$ . (If $u = 0$ , this is equivalent to setting $λ (σ_{a, t} (u, x)) = 0$ .)

For each $z \in [a] \times [b]$ we set $ν (z) = σ_{a, t} (a, ν_{a} (z))$ .
By item (4) the $[a] \times [b]$ -string that the subcircuit $C_{u}$ gets as its third “input” is the union of the $[a] \times [b]$ -strings “output” by the subcircuits $C_{u^{'}}$ for $u^{'} \in u$ . Thus by induction on u the “output” of $C_{u}$ is $\sim_{u}$ . Finally item (5) reads off the “output” of the top subcircuit $C_{a}$ as the output of our circuit C. □
Lemma 6.15.
There is a family $C_{a}$ of $Δ_{0}^{#}$ -uniform circuits, with input and output size ${[a]}^{2}$ , which take as input a string E and output a string giving the relation “x is an E-ancestor of y in the diagram $⟨ a, E ⟩$ ”.
Proof.
Let us write $⊲_{u}$ for the E-ancestor relation on $⟨ u, E ⟩$ . Let $R_{u} = ⋃ {⊲_{v} : v \in u}$ . Then for $x, y \in [u]$ , we have $⟨ x, y ⟩ \in ⊲_{u}$ if and only if $\begin{matrix} x = y \lor ⟨ x, y ⟩ \in R_{u} \lor \exists z \in [a] (z < y \land ⟨ x, z ⟩ \in R_{u} \land ⟨ z, y ⟩ \in E) . \end{matrix}$ Hence by Lemma 6.11 there is a small, $Δ_{0}^{#}$ -uniform circuit $C_{a, u}$ computing $⊲_{u}$ from E and $R_{u}$ , with size $t (a)$ independent of u.

Our circuit has size $a # t (a)$ and is formed by taking $G (a)$ and replacing each node u with a copy of $C_{a, u}$ , adding edges so that $C_{a, u}$ gets as input E and the union of the outputs of $C_{a, v}$ for $v \in u$ , exactly as in Lemma 6.14. □

7. Small circuits for ${CRSF}_{\subseteq}^{+}$

Theorem 7.1.
Every ${CRSF}_{\subseteq}^{+}$ function has $Δ_{0}^{#}$ -uniform circuits.

To prove this it is enough to show that all our initial functions have such circuits, and that the class of functions with such circuits is closed under composition and subset-bounded recursion. Lemma 7.2.
The class of set functions with $Δ_{0}^{#}$ -uniform circuits is closed under composition.
Proof.
Let g be an m-ary set function computed by a circuit family $D_{\vec{x}}$ with size $d (\vec{x})$ . Let $f_{1}, \dots, f_{m}$ be n-ary set functions, with $f_{i}$ computed by a circuit family $C_{\vec{y}}^{i}$ with size $c_{i} (\vec{y})$ and output size ${[s_{i} (\vec{y})]}^{2}$ . Then the circuit to compute the composition of g and $\vec{f}$ on inputs embeddable in $\vec{y}$ has size $\begin{matrix} d (s_{1} (\vec{y}), \dots, s_{m} (\vec{y})) ⊙ {c_{m} (\vec{y})} ⊙ \dots ⊙ {c_{1} (\vec{y})} \end{matrix}$ and is formed in the obvious way, by connecting copies of $D_{s_{1} (\vec{y}), \dots, s_{m} (\vec{y})}$ and $C_{\vec{y}}^{1}, \dots, C_{\vec{y}}^{m}$ together. □

7.1. Initial functions

The projection function is trivial, and we dealt with the union function in Lemma 6.12. Pairing, conditional, set composition, set smash, transitive closure, cartesian product and embedded Mostowski collapse remain. In each case the proof uses Lemma 6.11.

Lemma 7.3.
The pairing function has $Δ_{0}^{#}$ -uniform circuits.
Proof.
Given diagrams $⟨ a, E ⟩$ and $⟨ b, F ⟩$ let $c = {b} ⊙ {a}$ , so that $G (c)$ has the structure of, first, a copy of $G (a)$ , then an edge connecting its sink to the source of a copy of $G (b)$ , then an edge connecting the sink of that to the global sink c. Let $⟨ x, y ⟩ \in G$ if and only if one of the following holds:
$⟨ x, y ⟩ \in E$

$⟨ x, y ⟩ = ⟨ x^{'} ⊙ {a}, y^{'} ⊙ {a} ⟩$ for some $⟨ x^{'}, y^{'} ⟩ \in F$

$y = c$ and either $x = a$ or $x = b ⊙ {a}$ .
By items (1) and (2), $M (a, G) = M (a, E)$ and $M (b ⊙ {a}, G) = M (b, F)$ . Hence by item (3) we have $M (c, G) = {M (a, E), M (b, F)}$ as required. The lemma now follows from Lemma 6.11. □
Lemma 7.4.
(The characteristic functions of) membership and equality have $Δ_{0}^{#}$ -uniform circuits.
Proof.
This follows from Lemma 6.14. For example, to compute membership, given diagrams $⟨ a, E ⟩$ and $⟨ b, F ⟩$ we first construct a subcircuit computing the bisimulation ∼ between $⟨ a, E ⟩$ and $⟨ b, F ⟩$ . Then $M (a, E) \in M (b, F)$ if and only if there exists $u < b$ with $⟨ u, b ⟩ \in F$ and $a \sim u$ . □
Lemma 7.5.
The ${cond}_{\in}$ function has $Δ_{0}^{#}$ -uniform circuits.
Proof.
Recall that the function ${cond}_{\in} (e, f, g, h)$ takes the value e if $g \in h$ and takes the value f otherwise. Suppose we are given diagrams $⟨ a, E ⟩$ , $⟨ b, F ⟩$ , $⟨ c, G ⟩$ and $⟨ d, H ⟩$ . We will output a diagram $⟨ b ⊙ a, I ⟩$ . Our circuit is formed from four subcircuits, which we will call W, X, Y and Z. These are combined in a similar way to Lemma 7.2.

The subcircuit W computes whether $M (c, G) \in M (d, H)$ , as in Lemma 7.4.

The subcircuit X computes a ${[b ⊙ a]}^{2}$ string $I_{E}$ with $\begin{matrix} ⟨ x, y ⟩ \in I_{E} \Leftrightarrow \{\begin{matrix} ⟨ x, y ⟩ \in E & if y \neq a \\ ⟨ x, a ⟩ \in E & if y = b ⊙ a \end{matrix} \end{matrix}$ so that $I_{E}$ has the structure of E but with the sink node moved to $b ⊙ a$ , giving $M (b ⊙ a, I_{E}) = M (a, E)$ .

The subcircuit Y computes a ${[b ⊙ a]}^{2}$ string $I_{F}$ with $\begin{matrix} ⟨ x, y ⟩ \in I_{F} \Leftrightarrow ⟨ x, y ⟩ = ⟨ x^{'} ⊙ a, y^{'} ⊙ a ⟩ for some ⟨ x^{'}, y^{'} ⟩ \in F \end{matrix}$ so that $M (b ⊙ a, I_{F}) = M (b, F)$ .

Finally, Z takes the outputs of W, X and Y, and outputs $I_{E}$ if $M (c, G) \in M (d, H)$ and $I_{F}$ otherwise. □
Lemma 7.6.
The set composition function ⊙ has $Δ_{0}^{#}$ -uniform circuits.
Proof.
Suppose we are given diagrams $⟨ a, E ⟩$ and $⟨ b, F ⟩$ . We will output a diagram $⟨ a ⊙ b, G ⟩$ , where $⟨ x, y ⟩ \in G$ if one of the following holds:
$⟨ x, y ⟩ \in F$

$⟨ x, y ⟩ = ⟨ b, y^{'} ⊙ b ⟩$ for some $⟨ x^{'}, y^{'} ⟩ \in E$ where $x^{'}$ is a source node of $⟨ a, E ⟩$

$⟨ x, y ⟩ = ⟨ x^{'} ⊙ b, y^{'} ⊙ b ⟩$ for some $⟨ x^{'}, y^{'} ⟩ \in E$ where $x^{'}$ is not a source node of $⟨ a, E ⟩$
By item (1), $M (b, G) = M (b, F)$ . Items (2) and (3) put the structure of $⟨ a, E ⟩$ onto the copy of $G (a)$ inside $G (a ⊙ b)$ , except that all source nodes of $⟨ a, E ⟩$ get mapped to b. Hence $M (a ⊙ b, G) = M (a, E) ⊙ M (b, F)$ . □
Lemma 7.7.
The set smash function # has $Δ_{0}^{#}$ -uniform circuits.
Proof.
Suppose we are given diagrams $⟨ a, E ⟩$ and $⟨ b, F ⟩$ . We will output a diagram $⟨ a # b, G ⟩$ , where $⟨ x, y ⟩ \in G$ if either of the following hold:
$⟨ x, y ⟩ = ⟨ σ_{a, b} (u, x^{'}), σ_{a, b} (u, y^{'}) ⟩$ for some $u \in [a]$ and $⟨ x^{'}, y^{'} ⟩ \in F$

$⟨ x, y ⟩ = ⟨ σ_{a, b} (u, b), σ_{a, b} (v, x) ⟩$ for some $⟨ u, v ⟩ \in E$ and some source node x of $⟨ b, F ⟩$ .
Here item (1) puts a copy of the structure of F onto each copy of $G (b)$ inside $G (a # b)$ , and item (2) connects the sources and sinks of these copies according to the edges of E. Hence $M (a # b, G) = M (a, E) # M (a, B)$ . □
Lemma 7.8.
Transitive closure has $Δ_{0}^{#}$ -uniform circuits.
Proof.
We are given a diagram $⟨ a, E ⟩$ and will output a diagram $⟨ a, F ⟩$ . We first use Lemma 6.15 to construct a subcircuit computing the E-ancestor relation on $⟨ a, E ⟩$ as an ${[a]}^{2}$ -string R. We then compute F as $E \cup {⟨ x, a ⟩ : ⟨ x, a ⟩ \in R}$ , so that $M (a, F) = tc (M (a, E))$ . □
Lemma 7.9.
Cartesian product has $Δ_{0}^{#}$ -uniform circuits.
Proof.
We are given diagrams $⟨ a, E ⟩$ and $⟨ b, F ⟩$ . We will output a diagram $⟨ c, G ⟩$ where $c = ((a \times b) # 2) ⊙ {b} ⊙ {a}$ . We begin by copying the structures of $⟨ a, E ⟩$ and $⟨ b, F ⟩$ onto the copies of $G (a)$ and $G (b)$ inside $G (c)$ , so that $M (a, G) = M (a, E)$ and $M (b ⊙ {a}, G) = M (b, F)$ .

Recall that ordered pairs are defined as $⟨ e, f ⟩ = {{e}, {e, f}}$ . At the top of $G (c)$ , the graph $G ((a \times b) # 2)$ contains a disjoint copy of $G (2)$ for each $⟨ x, y ⟩ \in a \times b$ . Let $\begin{matrix} τ : z \mapsto σ_{a \times b, 2} (⟨ x, y ⟩, z) ⊙ {b} ⊙ {a} \end{matrix}$ be the mapping from $G (2)$ to this copy of $G (2)$ . If $⟨ x, a ⟩ \in E$ and $⟨ y, b ⟩ \in F$ then we add to G the edges
$⟨ x, τ (0) ⟩$ , so that $M (τ (0), G) = {M (x, E)}$

$⟨ x, τ (1) ⟩$ and $⟨ y ⊙ {a}, τ (1) ⟩$ , so that $M (τ (1), G) = {M (x, E), M (y, F)}$

$⟨ τ (0), τ (2) ⟩$ , $⟨ τ (1), τ (2) ⟩$ and $⟨ τ (2), c ⟩$ , so that $⟨ M (x, E), M (y, F) ⟩ \in M (c, G)$ .
We do this for every $⟨ x, y ⟩ \in a \times b$ . Hence $M (c, G) = M (a, E) \times M (y, F)$ . □
Lemma 7.10.
Embedded Mostowski collapse has $Δ_{0}^{#}$ -uniform circuits.
Proof.
We are given diagrams $⟨ b, G_{a} ⟩$ and $⟨ c, G_{E} ⟩$ . We will output a diagram $⟨ b, H ⟩$ such that if we let $a = M (b, G_{a})$ and $E = M (c, G_{E})$ then $M (b, H) = M (a, E)$ .

For any set x, define $κ (x) = M (x, G_{a})$ , so that $κ (b) = a$ . We put $\begin{matrix} H = {⟨ x, y ⟩ \in {[b]}^{2} : x < y \land κ (x) < κ (y) \land ⟨ κ (x), κ (y) ⟩ \in E} . \end{matrix}$ Before showing how to compute H with a circuit, we prove that $M (b, H) = M (a, E)$ . We will show by ∈-induction on y that $M (y, H) = M (κ (y), E)$ for all $y \in [b]$ . Suppose this is true for all $x < y$ . Then $\begin{array}{l} M (y, H) & = {M (x, H) : x < y \land ⟨ x, y ⟩ \in H} \\ = {M (κ (x), E) : x < y \land κ (x) < κ (y) \land ⟨ κ (x), κ (y) ⟩ \in E} \\ = {M (z, E) : z < κ (y) \land ⟨ z, κ (y) ⟩ \in E} \\ = M (κ (y), E) . \end{array}$ Here the first and fourth equalities are the definition of M, and the second follows from the inductive hypothesis and the definition of H. One direction of the third equality follows from setting $z = κ (x)$ . For the other direction, let $z < κ (y)$ and $⟨ z, κ (y) ⟩ \in E$ . Since $z < κ (y)$ there is a finite sequence $z_{1}, \dots, z_{k}$ such that $z = z_{1} \in \dots \in z_{k} \in κ (y)$ . By the definition of κ, there is some $x_{k} < y$ such that $z_{k} = κ (x_{k})$ . Similarly we can find $x_{k - 1} < x_{k}$ such that $z_{k - 1} = κ (x_{k - 1})$ , and so on until we find $x_{1} < x_{2}$ with $z = z_{1} = κ (x_{1})$ . We put $x = x_{1}$ .

To compute H with a circuit, we first construct subcircuits computing the bisimulation $\sim_{a}$ between $⟨ b, G_{a} ⟩$ and $⟨ b, G_{a} ⟩$ ; the bisimulation $\sim_{a, E}$ between $⟨ b, G_{a} ⟩$ and $⟨ c, G_{E} ⟩$ ; the bisimulation $\sim_{E}$ between $⟨ c, G_{E} ⟩$ and $⟨ c, G_{E} ⟩$ ; and the $G_{a}$ -ancestor relation $⊲_{a}$ on $⟨ b, G_{a} ⟩$ . Then for $x, y \in [b]$ , $\begin{matrix} κ (x) < κ (y) \Leftrightarrow M (x, G_{a}) \in tc (M (y, G_{a})) \Leftrightarrow \exists u < y, x \sim_{a} u \land u ⊲_{a} y . \end{matrix}$ On the other hand, $⟨ κ (x), κ (y) ⟩ \in E$ if and only if $\begin{matrix} \exists x^{'}, y^{'} < c, M (x, G_{a}) = M (x^{'}, G_{E}) \land M (y, G_{a}) = M (y^{'}, G_{E}) \land ⟨ M (x^{'}, G_{E}), M (y^{'}, G_{E}) ⟩ \in M (c, G_{E}) \end{matrix}$ which is equivalent to $\begin{matrix} \exists x^{'}, y^{'} < c, x \sim_{a, E} x^{'} \land y \sim_{a, E} y^{'} \land “ ⟨ c, G_{E} ⟩ ⊨ ⟨ x^{'}, y^{'} ⟩ \in c ”, \end{matrix}$ where the expression in quotation marks means that we interpret $⟨ x^{'}, y^{'} ⟩ \in c$ in the universe $[c]$ with the membership relation given by $G_{E}$ and equality given by $\sim_{E}$ . This can be written as a $Δ_{0}^{#}$ formula. □

7.2. Closure under recursion

Lemma 7.14 below establishes closure under subset-bounded recursion. We will need a few gadgets for the proof.

Lemma 7.11.
The function $x, y \mapsto x \cap y$ has $Δ_{0}^{#}$ -uniform circuits. Furthermore we may assume that the circuit $C_{a, b}$ computing it on sets embeddable in $a, b$ outputs an ${[a]}^{2}$ -string E for a diagram $⟨ a, E ⟩$ .
Proof.
We are given diagrams $⟨ a, X ⟩$ and $⟨ b, Y ⟩$ . We first build a subcircuit to compute the bisimulation ∼ between them, then put $\begin{matrix} ⟨ i, j ⟩ \in E \Leftrightarrow \{\begin{matrix} ⟨ i, j ⟩ \in X & if j \neq a \\ ⟨ i, j ⟩ \in X \land \exists i^{'} \in [b], ⟨ i^{'}, b ⟩ \in Y \land i \sim i^{'} & if j = a . \end{matrix} \end{matrix}$ □
Lemma 7.12.
There is a $Δ_{0}^{#}$ -uniform family $C_{a, u}$ of circuits with size bounds independent of u which, for $u ⩽ a$ , take as input an ${[a]}^{2}$ -string X and output an ${[a]}^{2}$ -string E such that $M (a, E) = M (u, X)$ .
Proof.
If $u = a$ then we output X. Otherwise we take X, remove all edges $⟨ i, a ⟩$ , then add an edge $⟨ i, a ⟩$ for every $⟨ i, u ⟩ \in X$ , and output the result. □
Lemma 7.13.
There is a $Δ_{0}^{#}$ -uniform family $C_{a, b, u}$ of circuits with size bounds independent of u which, for $u ⩽ a$ , take as input an $[a] \times {[b]}^{2}$ -string W and an ${[a]}^{2}$ -string X, and output an ${[a # b]}^{2}$ string E such that $\begin{matrix} M (a # b, E) = {M (b, W^{(v)}) : v < u \land ⟨ v, u ⟩ \in X} . \end{matrix}$
Proof.
We repeat the construction from the proof of Lemma 5.9. We will write σ, $π_{1}$ and $π_{2}$ respectively for the functions $σ_{a, b}$ , $π_{1, a, b}$ and $π_{2, a, b}$ . Define $\begin{matrix} E^{'} = {⟨ i, j ⟩ \in {[a # b]}^{2} : π_{1} (i) = π_{1} (j) \neq a \land ⟨ π_{2} (i), π_{2} (j) ⟩ \in W^{(π_{1} (i))}} . \end{matrix}$ For each $v < a$ this puts the structure of $W^{(v)} \cap {[b]}^{2}$ onto copy v of the graph of b inside the graph of $E^{'}$ , so that $M (σ (v, b), E^{'}) = M (b, W^{(v)})$ . On the other hand $σ (b, a) = a # b$ is not connected to anything in $E^{'}$ , so $M (a # b, E^{'}) = 0$ . To rectify this, let $E = E^{'} \cup {⟨ σ (v, b), a # b ⟩ : v < u \land ⟨ v, u ⟩ \in X}$ . □

We can now prove the main result of this subsection. Lemma 7.14.
The class of functions with $Δ_{0}^{#}$ -uniform circuits is closed under subset-bounded recursion.
Proof.
Suppose that g and h are set functions with $Δ_{0}^{#}$ -uniform circuits. Let f be the function satisfying $\begin{matrix} f (x, z) = g ({f (y, z) : y \in x}, x, z) \cap h (x, z) \end{matrix}$ where for simplicity we consider only a single parameter z rather than a tuple of parameters $\vec{z}$ (this does not change anything important). We are given sets $a, c$ and must construct a circuit computing $f (x, z)$ on all sets $x, z$ embeddable in respectively $a, c$ . Consider arbitrary input strings $X, Z$ and let $x = M (a, X)$ and $z = M (c, Z)$ .

We would like to build a circuit similar to those for Lemmas 6.14 and 6.15, in which we put together many copies of the circuits for g and h to simulate computing $f (x, z)$ by recursion on x. However we are given X as a string input, and cannot use it as a parameter when constructing our circuit. Instead we will model a recursion on a.

Let ${[t]}^{2} = {[t (a, c)]}^{2}$ be the output size of the given circuit computing $h (x, z)$ on sets embeddable in $a, c$ . We will build a circuit which, as it computes, constructs for each node $u \in [a]$ a ${[t]}^{2}$ -string $F_{u}$ such that $\begin{matrix} (1) & M (t, F_{u}) = f (M (u, X), z) \end{matrix}$ and hence in particular $M (t, F_{a}) = f (x, z)$ .

Let $g^{'} (s, x, z) = g (s, x, z) \cap h (x, z)$ and let $C = C_{a, c}$ be a circuit computing $g^{'}$ on sets $s, x, z$ embedded in $a # t, a, c$ . By our assumptions and Lemma 7.11, we may assume that C is $Δ_{0}^{#}$ -uniform and furthermore that the output of C is a ${[t]}^{2}$ -string. Let $D_{u} = D_{a, u}$ be the circuit from Lemma 7.12 with the property that $\begin{matrix} M (a, D_{u} (X)) = M (u, X) \end{matrix}$ for $u ⩽ a$ . Let $E_{u} = E_{a, t, u}$ be the circuit from Lemma 7.13 with the property that, for any $[a] \times {[t]}^{2}$ -string W, $\begin{matrix} M (a # t, E_{u} (W, X)) = {M (t, W^{(v)}) : v < u, ⟨ v, u ⟩ \in X} . \end{matrix}$ Combining these, let $G_{u}$ be the circuit which takes an $[a] \times {[t]}^{2}$ -string W, an ${[a]}^{2}$ -string X and a ${[c]}^{2}$ -string Z, and outputs the ${[t]}^{2}$ -string $\begin{matrix} G_{u} (W, X, Z) = C (E_{u} (W, X), D_{u} (X), Z) . \end{matrix}$

Suppose we have found $F_{v}$ satisfying (1) for all $v < u$ . If we define $\begin{matrix} W = {⟨ v, i, j ⟩ \in [a] \times {[t]}^{2} : v < u, ⟨ i, j ⟩ \in F_{v}} \end{matrix}$ then $W^{(v)} = F_{v}$ for all $v < u$ , and if we let $F_{u} = G_{u} (W, X, Z)$ we have $\begin{array}{l} M (t, F_{u}) & = M (t, C (E_{u} (W, X), D_{u} (X), Z)) \\ = g^{'} (M (a # t, E_{u} (W, X)), M (a, D_{u} (X)), M (c, Z)) \\ = g^{'} ({M (t, F_{v}) : v < u, ⟨ v, u ⟩ \in X}, M (u, X), z) \\ = g^{'} ({f (y, z) : y \in M (u, X)}, M (u, X), z) \\ = f (M (u, X), z) . \end{array}$

We can now describe a circuit computing $F_{a}$ . Its overall shape is similar to the circuit for bisimilarity in Lemma 6.14. We start by taking a copy of $G_{u}$ for each $u \in [a]$ , so the size of our circuit is $a # q$ where q is the size of $G_{u}$ (which is independent of u). We let each $G_{u}$ take its inputs X and Z from the global inputs X and Z. Its input nodes for W correspond to triples $⟨ v, i, j ⟩ \in [a] \times {[t]}^{2}$ . For each such node, if $v ≮ u$ we relabel it with the constant 0. Otherwise we wire it to the output node of $G_{v}$ corresponding to $⟨ i, j ⟩$ . In this way each $G_{u}$ gets as input exactly the string W described above. Hence the output of the topmost subcircuit $G_{a}$ is $F_{a}$ . □

8. Consequences of small circuits

In this section we use our results about small circuits first to sharpen our characterization of ${CRSF}_{\subseteq}^{+}$ , and then to prove some lower bounds for it.

Theorem 8.1.
The ${CRSF}_{\subseteq}^{+}$ functions are exactly the set functions with $Δ_{0}^{#}$ -uniform circuits.
Proof.
One direction is given by Theorem 7.1. It remains to show that every function with $Δ_{0}^{#}$ -uniform circuits is in ${CRSF}_{\subseteq}^{+}$ . So suppose that $f (x_{1}, \dots, x_{k})$ is such a function. This means that there is such a family $C_{\vec{a}}$ of circuits with the property that, for all $a_{1}, \dots, a_{k}$ , the circuit $C_{\vec{a}}$ computes f on sets embeddable in $\vec{a}$ , and that if $C_{\vec{a}} = ⟨ c, E, λ, \vec{s}, p, μ, ν ⟩$ then c and p are given by smash-terms in $\vec{a}$ , each input size $s_{i}$ is ${[a_{i}]}^{2}$ , and E, λ, μ and ν are $Δ_{0}^{#}$ -definable from $\vec{a}$ .

To compute f on $\vec{a}$ in ${CRSF}_{\subseteq}^{+}$ we first construct the circuit $C_{\vec{a}}$ . This can be done in ${CRSF}_{\subseteq}$ , since by the uniformity conditions and the closure properties of ${CRSF}_{\subseteq}$ there are ${CRSF}_{\subseteq}$ functions computing each component of $C_{\vec{a}}$ from $\vec{a}$ , and we can construct the usual ordered 7-tuples in ${CRSF}_{\subseteq}$ . Then for each i we can trivially construct from $a_{i}$ the ${[a_{i}]}^{2}$ -string $E_{i} : = \in ↾ [a_{i}]$ , so that $M (a_{i}, E_{i}) = a_{i}$ . By Lemma 6.6, we can evaluate $C_{\vec{a}}$ on these strings with a ${CRSF}_{\subseteq}$ function; then, with a ${CRSF}_{\subseteq}^{+}$ function, we can output $M (t, C_{\vec{a}} (E_{1}, \dots, E_{k}))$ , where $p = t \times t$ is the output size of $C_{\vec{a}}$ . □

It follows from the proof above that any function in ${CRSF}_{\subseteq}^{+}$ can be computed using only a single Mostowski collapse at the end of the computation.
Theorem 8.2.
Let $f \in {CRSF}_{\subseteq}^{+}$ . Then there is $g \in {CRSF}_{\subseteq}$ and a smash-term t such that $f (\vec{a}) = M (t (\vec{a}), g (\vec{a}))$ .
Proof.
By Theorem 7.1, the function f has $Δ_{0}^{#}$ -uniform circuits. We now repeat the proof of Theorem 8.1, skipping the final step, so that g computes $C_{\vec{a}} (E_{1}, \dots, E_{k})$ . □
Corollary 8.3.
The ${CRSF}_{\subseteq}^{+}$ and ${CRSF}_{\subseteq}$ relations are the same. Furthermore for every $f \in {CRSF}_{\subseteq}^{+}$ the function $g (\vec{a}, b) : = f (\vec{a}) \cap b$ is in ${CRSF}_{\subseteq}$ .
Proof.
For the first part, observe that given a diagram $⟨ t, E ⟩$ we can easily compute in ${CRSF}_{\subseteq}$ whether $M (t, E) = 0$ . For the second part, we first compute a diagram $⟨ t, E ⟩$ with $M (t, E) = f (\vec{a})$ , and then compute the bisimulation ∼ between $⟨ t, E ⟩$ and the Mostowski graph of b. Then $f (\vec{a}) \cap b = {c \in b : \exists u < t, ⟨ u, t ⟩ \in E \land u \sim c}$ . □

We can generalize Theorem 8.2 into a useful result about computing codes for ${CRSF}_{\subseteq}^{+}$ functions in ${CRSF}_{\subseteq}$ .
Lemma 8.4.
Let $f \in {CRSF}_{\subseteq}^{+}$ . Then there is $g \in {CRSF}_{\subseteq}$ and a smash-term t such that $f (\vec{b}) = M (t (\vec{a}), g (\vec{a}, \vec{b}))$ whenever $\vec{a}$ and $\vec{b}$ are tuples of sets with $b_{i} ⩽ a_{i}$ for all i.
Proof.
As before we repeat the proof of Theorem 8.1, except, rather than choosing $E_{i}$ such that $M (a_{i}, E_{i}) = a_{i}$ we choose it so that $M (a_{i}, E_{i}) = b_{i}$ . This can be done by first constructing a ${[b_{i}]}^{2}$ -string $E_{i}^{'}$ such that $M (b_{i}, E_{i}^{'}) = b_{i}$ and then using the method of Lemma 7.12. □
Corollary 8.5.
${CRSF}_{\subseteq}^{+}$ is closed under the replacement and union schemes. That is, for any ${CRSF}_{\subseteq}^{+}$ function g, there are ${CRSF}_{\subseteq}^{+}$ functions f and u with $\begin{matrix} f (\vec{a}, c) = {g (\vec{a}, b) : b \in c} and u (\vec{a}, c) = ⋃_{b \in c} g (\vec{a}, b) . \end{matrix}$
Proof.
By Lemma 8.4 there is a smash term t and a ${CRSF}_{\subseteq}$ function h such that $h (\vec{a}, c, b) \subseteq {[t (\vec{a}, c)]}^{2}$ and $g (\vec{a}, b) = M (t (\vec{a}, c), h (\vec{a}, c, b))$ for every $b \in c$ . We can now use the method of Section 5.3 for coding collections of sets. Let $\begin{matrix} W = ⋃_{b \in c} {b} \times h (\vec{a}, c, b) . \end{matrix}$ Then $M (t (\vec{a}, c), W^{(b)}) = g (\vec{a}, b)$ for every $b \in c$ , and W is computable in ${CRSF}_{\subseteq}$ from $\vec{a}$ and c using separation, since $W \subseteq c \times {[t (\vec{a}, c)]}^{2}$ . Replacement follows by Lemma 5.9, and union follows immediately from replacement. □

The course-of-values of a function $f (x)$ on a set a (where f may possibly have other parameters) is defined in [4] as the set ${⟨ b, f (b) ⟩ : b \in tc (a)}$ . We will use a slightly different definition, in the spirit of Section 5.3, which is more convenient to use with subset-bounded recursion.
Definition 8.6.
We define $f_{↾ c} (\vec{a}, -) : = ⋃_{b \in c} {b} \times f (\vec{a}, b)$ , so that for $b \in c$ we have $f (\vec{a}, b) = f_{↾ c} {(\vec{a}, -)}^{(b)}$ .

We define the course-of-values of $f (\vec{a}, x)$ on c (with respect to the argument x) as $f_{↾ tc (c)} (\vec{a}, -)$ , and will write this as $f_{< c} (\vec{a}, -)$ .
Definition 8.7.
The function f is obtained from g by subset-bounded course-of-values recursion with bound h if $\begin{matrix} f (\vec{a}, b) = g (\vec{a}, b, f_{< b} (\vec{a}, -)) \cap h (\vec{a}, b) . \end{matrix}$
Corollary 8.8.
${CRSF}_{\subseteq}^{+}$ is closed under subset-bounded course-of-values recursion.
Proof.
Suppose $f (\vec{a}, b) = g (\vec{a}, b, f_{< b} (\vec{a}, -)) \cap h (\vec{a}, b)$ with $g, h \in {CRSF}_{\subseteq}^{+}$ . Define $F (\vec{a}, b) = f_{↾ [b]} (\vec{a}, -)$ . Then $F (\vec{a}, b) \subseteq [b] \times ⋃_{c ⩽ b} h (\vec{a}, c)$ , since each $f (\vec{a}, c) \subseteq h (\vec{a}, c)$ . By Corollary 8.5 this bound on F is in ${CRSF}_{\subseteq}^{+}$ . Hence we may potentially define F by subset-bounded recursion. This is straightforward, as given $S = {F (\vec{a}, c) : c \in b}$ we have that $⋃ S = f_{< b} (\vec{a}, -)$ , so $f (\vec{a}, b) = g (\vec{a}, b, ⋃ S)$ and $F (\vec{a}, b) = ⋃ S \cup ({b} \times f (\vec{a}, b))$ . Hence F is in ${CRSF}_{\subseteq}^{+}$ , and it follows immediately that f is as well. □

An interesting consequence of our characterization of ${CRSF}_{\subseteq}^{+}$ in terms of circuits is that it allows us to use known circuit lower bounds to prove that certain functions are not in ${CRSF}_{\subseteq}^{+}$ .
Theorem 8.9.
There is no ${CRSF}_{\subseteq}^{+}$ function f which computes the parity of $| x |$ for every hereditarily finite set x.
Proof.
Suppose f is such a function. Then by Theorem 7.1 there is a smash-term t such that for every set a there is a circuit $C_{a}$ of size $t (a)$ computing f on all sets embeddable in a. Choose a large $n \in ω$ of the form $2^{2^{k}}$ . Let $a = P (P (k))$ . Then $rank (a) = k + 2$ , $| a | = n$ and $| [a] | ⩽ 2 n$ . Therefore the underlying graph $G (t (a))$ of $C_{a}$ has depth (that is, rank) polynomial in k and size polynomial in n. But since $C_{a}$ computes the parity of all subsets of a, it is straightforward to build from it a circuit of depth polynomial in k and size polynomial in n which computes the parity of all n-bit strings, which is impossible by [8]. □

In contrast, by the simulation of polynomial time in ${CRSF}_{\subseteq}^{+}$ in Section 4 there is a ${CRSF}_{\subseteq}$ function which can compute the parity of a hereditarily finite set x, as long as x is a set of ordinals.

As a corollary of Theorem 8.9 we get a version of P ≠ NP for ${CRSF}_{\subseteq}^{+}$ . We first define a natural notion of NP for ${CRSF}_{\subseteq}^{+}$ .
Definition 8.10.
A $Σ_{1}^{\subseteq}$ - ${CRSF}_{\subseteq}^{+}$ relation is one of the form $\exists y \subseteq t (x) φ (x, y)$ , where $φ (x, y)$ is a ${CRSF}_{\subseteq}^{+}$ relation and t is a smash term.
Corollary 8.11.
The relation $φ (x)$ expressing that x can be partitioned into a collection of unordered pairs is $Σ_{1}^{\subseteq}$ - ${CRSF}_{\subseteq}^{+}$ but is not equivalent to any ${CRSF}_{\subseteq}^{+}$ relation, even on hereditarily finite sets x.

That $Σ_{1}^{\subseteq}$ - ${CRSF}_{\subseteq}^{+}$ is different from ${CRSF}_{\subseteq}^{+}$ on ${0, 1}^{ω}$ already follows from [12]. Say that a set $L \subseteq {0, 1}^{ω}$ is in NP if there is a set $M \subseteq {0, 1}^{ω}$ in P (that is, decided by a polynomial time infinite-time Turing machine) such that $x \in L \leftrightarrow \exists y \in {0, 1}^{ω} x \oplus y \in M$ , where $x \oplus y \in {0, 1}^{ω}$ alternates bits from x with bits from y. Then [12] shows that every set in P is Borel, and gives an example of a set Δ in NP which is not Borel. By Theorems 4.5 and 4.6, P coincides with ${CRSF}_{\subseteq}^{+}$ on ${0, 1}^{ω}$ . It follows that Δ is in $Σ_{1}^{\subseteq}$ - ${CRSF}_{\subseteq}^{+}$ but not in ${CRSF}_{\subseteq}^{+}$ .

As was already discussed, since the above separation is based on parity, it has no relevance for whether the ordinary versions of P and NP are distinct.
9. Embedding-bounded recursion

We will write ${CRSF}_{≼}$ for the class of $CRSF$ functions in the sense of [4]. The goal of this section is to show that ${CRSF}_{\subseteq}^{+}$ and ${CRSF}_{≼}$ are the same. We recall some definitions from [4].

Definition 9.1.
A function τ is an embedding of a into b, written $τ : a ≼ b$ , if $τ : tc (a) \to P (tc (b))$ and for all $x, y \in tc (a)$ ,
$τ (x) \neq 0$

if $x \neq y$ then $τ (x) \cap τ (y) = 0$

if $x \in y$ then for every $v \in τ (y)$ , there is some $u \in τ (x)$ with $u < v$ .

Definition 9.2.
Let $g (\vec{a}, b, x)$ , $h (\vec{a}, b)$ and $τ (x, \vec{a}, b)$ be functions. The function $f (\vec{a}, b)$ is obtained from $g (\vec{a}, b, x)$ by embedding-bounded recursion with bound $h (\vec{a}, b)$ and embedding function $τ (x, \vec{a}, b)$ if $\begin{matrix} f (\vec{a}, b) = g (\vec{a}, b, {f (\vec{a}, c) : c \in b}) \end{matrix}$ and if for all $\vec{a}, b$ we have $τ (x, \vec{a}, b) : f (\vec{a}, b) ≼ h (\vec{a}, b)$ . The last condition means that the function $x \mapsto τ (x, \vec{a}, b)$ is an embedding $f (\vec{a}, b) ≼ h (\vec{a}, b)$ .
Definition 9.3.
${CRSF}_{≼}$ is the closure of the empty set, projections, pairing, union, ${cond}_{\in}$ and set smash # functions under composition and embedding-bounded recursion.

We first show that the two natural notions of embeddability coincide.
Lemma 9.4.
The following are equivalent:
There is a set E such that $a = M (b, E)$ .

There is a function τ such that $τ : a ≼ b$ .

Proof.
First suppose that $a = M (b, E)$ . For $x < a$ define $τ (x) = {u < b : x = M (u, E)}$ . It is straightforward to show that τ has the properties of an embedding function. In particular, if $v \in τ (y)$ and $x \in y$ then $x \in M (v, E)$ so, by the definition of embedded Mostowski collapse, $x = M (u, E)$ for some $u < v$ , giving $u \in τ (x)$ as required.

For the other direction, suppose $τ : a ≼ b$ . We first extend the domain of τ from $tc (a)$ to $[a]$ by defining $τ (a) = {b}$ . It is easy to see that the three properties of an embedding function still hold. Now define E as the set of pairs $⟨ u, v ⟩ \in {[b]}^{2}$ such that $\begin{matrix} u < v \land \exists x, y \in [a], x \in y \land u \in τ (x) \land v \in τ (y) . \end{matrix}$ We will prove by ∈-induction on y that, for every $y \in [a]$ and $v \in τ (y)$ , $y = M (v, E)$ . Since $τ (a) = {b}$ it will follow that $a = M (b, E)$ .

Fix $v \in τ (y)$ . To show $M (v, E) \subseteq y$ , let $z \in M (v, E)$ . Then $z = M (u, E)$ for some $u < v$ with $⟨ u, v ⟩ \in E$ . By the definition of E and the properties of τ, there exists $x \in y$ with $u \in τ (x)$ . By the inductive hypothesis, $x = M (u, E)$ . Therefore $x = z$ , so $z \in y$ .

To show $y \subseteq M (v, E)$ , suppose $x \in y$ . Since $v \in τ (y)$ , by the properties of τ there is some $u \in τ (x)$ with $u < v$ . Then $⟨ u, v ⟩ \in E$ and also by the inductive hypothesis $x = M (u, E)$ . Therefore $x \in M (v, E)$ . □
Theorem 9.5.
${CRSF}_{\subseteq}^{+}$ is contained in ${CRSF}_{≼}$ .
Proof.
It is shown in [4] that ${CRSF}_{≼}$ contains all the initial functions of ${CRSF}_{\subseteq}$ and is closed under subset-bounded recursion. That is, all ${CRSF}_{\subseteq}$ functions are in ${CRSF}_{≼}$ . So it is enough to show that embedded Mostowki collapse is in ${CRSF}_{≼}$ . We know from [4] that ${CRSF}_{≼}$ is closed under course-of-values embedding-bounded recursion, which is a version of embedding-bounded recursion in which we are allowed us to use the sequence ${⟨ c, f (c, \vec{z}) ⟩ : c < b}$ of all earlier values of f when calculating $f (b, \vec{z})$ . We have $\begin{matrix} M (a, E) = {M (b, E) : b < a \land ⟨ b, a ⟩ \in E} . \end{matrix}$ If $S = {⟨ b, M (b, E) ⟩ : b < a}$ is the sequence of earlier values of M then $\begin{matrix} M (a, E) = {y \in ⋃ ⋃ S : \exists b < a, ⟨ b, y ⟩ \in S \land ⟨ b, a ⟩ \in E} \end{matrix}$ which is a ${CRSF}_{≼}$ function of S, E and a.

For this to be a valid instance of course-of-values embedding-bounded recursion, we also need to provide a ${CRSF}_{≼}$ function embedding $M (a, E)$ into an existing ${CRSF}_{≼}$ function of a and E. By the proof of Lemma 9.4, if $b = M (a, E)$ and we define $τ (x) = {u < a : x = M (u, E)}$ then $τ : b ≼ a$ . To compute τ by a ${CRSF}_{≼}$ function which does not use M, we first compute the bisimulation ∼ between the Mostowski graph of x and $⟨ a, E ⟩$ (by Lemma 5.7 we can do this in ${CRSF}_{\subseteq}$ , and hence in ${CRSF}_{≼}$ ) and then take $τ (x) = {u < a : x \sim u}$ . □
Theorem 9.6.
${CRSF}_{≼}$ is contained in ${CRSF}_{\subseteq}^{+}$ .
Proof.
By Theorem 21 of [4], it is enough to show that ${CRSF}_{\subseteq}^{+}$ is closed under ≼-bounded recursion where the bounding term h is a #-term. Here a #-term is a stricter version of our smash-term: it is built only from variables, the constant 1, and the function symbols ⊙ and #. So suppose that g and τ are ${CRSF}_{\subseteq}^{+}$ functions, h is a #-term and f is a function such that for all $\vec{a}, b$ $\begin{matrix} f (\vec{a}, b) = g (\vec{a}, b, {f (\vec{a}, c) : c \in b}) and τ (x, \vec{a}, b) : f (\vec{a}, b) ≼ h (\vec{a}, b) . \end{matrix}$ We must show that $f \in {CRSF}_{\subseteq}^{+}$ .

By Lemma 9.7 below we may assume that there is a function $τ^{'}$ in ${CRSF}_{\subseteq}^{+}$ such that, for all $\vec{a}, b, d$ with $b ⩽ d$ , $\begin{matrix} τ^{'} (x, \vec{a}, b, d) : f (\vec{a}, b) ≼ h (\vec{a}, d) . \end{matrix}$ We will use $τ^{'}$ rather than τ because it is convenient to have one fixed bounding set throughout the recursion. Below we write h for $h (\vec{a}, d)$ .

We will show $f \in {CRSF}_{\subseteq}^{+}$ by defining a function $F (\vec{a}, b, d)$ in ${CRSF}_{\subseteq}^{+}$ with the property that $F (\vec{a}, b, d) = {b} \times E$ for some ${[h]}^{2}$ -string E such that $M (h, E) = f (\vec{a}, b)$ whenever $b ⩽ d$ (the ${b}$ is there to help us carry out a kind of course-of-values recursion). We will construct F using ⊆-bounded recursion on b – note that $F (\vec{a}, b, d) \subseteq {b} \times {[h]}^{2}$ . We then obtain $f (\vec{a}, b)$ as $M (h (\vec{a}, b), F {(\vec{a}, b, b)}^{(b)})$ .

Consider the point in the recursion where we reach a set $b ⩽ d$ . We are given the set $s = {F (\vec{a}, c, d) : c \in b}$ . Let $W = ⋃ s$ . By Lemma 5.9 we can compute $s^{'} = {M (h, W^{(c)}) : c \in b}$ . By the properties of F, each $W^{(c)}$ is a set E with $M (h, E) = f (\vec{a}, c)$ . Therefore $s^{'} = {f (\vec{a}, c) : c \in b}$ .

We can now compute $f (\vec{a}, b)$ as $g (\vec{a}, b, s^{'})$ . Since we have a ${CRSF}_{\subseteq}^{+}$ embedding $τ^{'} : f (\vec{a}, b) ≼ h$ , we can use the construction in the proof of Lemma 9.4 to build a set $E \subseteq {[h]}^{2}$ such that $f (\vec{a}, b) = M (h, E)$ . We put $F (\vec{a}, b, d) = {b} \times E$ . □

For the previous theorem we need to reprove, for ${CRSF}_{\subseteq}^{+}$ functions, some technical results from [4] which capture the idea that #-terms behave like monotone functions with respect to embeddings. Lemma 9.7.
Let $f, g, h, i$ be ${CRSF}_{\subseteq}^{+}$ functions with arguments $\vec{a}, b$ , which we treat as parameters. Let $τ_{1}, τ_{2}$ be ${CRSF}_{\subseteq}^{+}$ functions with arguments $x, \vec{a}, b$ .
There is a ${CRSF}_{\subseteq}^{+}$ function τ such that if $τ_{1} : f ≼ g$ and $τ_{2} : g ≼ h$ , then $τ : f ≼ h$ .

There are ${CRSF}_{\subseteq}^{+}$ functions τ and $τ^{'}$ such that if $τ_{1} : f ≼ g$ and $τ_{2} : h ≼ i$ , then $τ : f ⊙ h ≼ g ⊙ i$ and $τ^{'} : f # h ≼ g # i$ .

If g is a #-term then there is a ${CRSF}_{\subseteq}^{+}$ function τ with arguments $x, \vec{a}, b, c$ such that whenever $τ_{1} (x, \vec{a}, b) : f (\vec{a}, b) ≼ g (\vec{a}, b)$ and $b ⩽ c$ then $τ (x, \vec{a}, b, c) : f (\vec{a}, b) ≼ g (\vec{a}, c)$ .

Proof.
For item (1), let $τ (x) = {z \in [h] : \exists y \in τ_{1} (x), z \in τ_{2} (y)}$ . The proof that this is an embedding function is just as in Lemma 18 of [4].

For item (2), extend $τ_{1}$ and $τ_{2}$ so that $τ_{1} (f) = {g}$ and $τ_{2} (h) = {i}$ . Let $\begin{array}{l} τ (x) = \{\begin{matrix} τ_{2} (x) & if x \in tc (h) \\ {y ⊙ i : y \in τ_{1} (x ⊙^{- 1} h)} & otherwise \end{matrix} \\ τ^{'} (x) = {σ_{g, i} (y^{'}, z^{'}) : y^{'} \in τ_{1} (π_{1, f, h} (x)) \land z^{'} \in τ_{2} (π_{2, f, h} (x))}, \end{array}$ where $x ⊙^{- 1} h$ is the (unique) z such that $x = z ⊙ h$ , or is 0 if no such z exists. Then $τ (x) \subseteq tc (g ⊙ i)$ and $τ^{'} (x) \subseteq tc (g # i)$ so both functions can be computed in ${CRSF}_{\subseteq}^{+}$ using separation. The proofs that these work are as in Lemma 19 of [4].

For item (3) it is enough, using item (1), to find a function $τ^{'}$ such that $τ^{'} (x, \vec{a}, b, c) : g (\vec{a}, b) ≼ g (\vec{a}, c)$ whenever $b ⩽ c$ . This is done by induction on the complexity of the #-term g, using items (1) and (2). □

10. Rudimentary functions

The class $Rud$ of rudimentary functions was introduced in [9], as the smallest class which contains projections, pairing and set subtraction $x ∖ y$ and is closed under composition and the union operation $f (\vec{a}, c) : = ⋃_{b \in c} g (\vec{a}, b)$ . We will use some properties of $Rud$ shown in [9], namely that it contains ×, is closed under separation, and that the $Rud$ relations are closed under Boolean operations and $Δ_{0}$ quantification.

Lemma 10.1.

Every $Rud$ function is in ${CRSF}_{\subseteq}^{+}$ .

Proof.

The only possible issue is closure under union, but this is taken care of by Corollary 8.5. □

Definition 10.2.

Let $RS$ be the class of functions obtained from $Rud$ by adding transitive closure as a basic function, and closing under subset-bounded recursion.

We will show that $RS$ and ${CRSF}_{\subseteq}^{+}$ have essentially the same complexity. A straightforward induction shows that no function in $RS$ increases the rank of its arguments by more than a constant, so $RS$ does not contain ⊙ or # and the two classes cannot exactly coincide. But by Theorem 10.8 below, for any ${CRSF}_{\subseteq}^{+}$ function f we can compute in $RS$ a string coding the value of f via a version of embedded Mostowski collapse. In particular it follows that the relations in $RS$ and ${CRSF}_{\subseteq}^{+}$ are the same.

The key idea is that constructions in ${CRSF}_{\subseteq}^{+}$ typically use recursion over smash-terms ordered by <, and we can simulate this in $RS$ using recursion over cartesian products ordered lexicographically by <.

Definition 10.3.

For $k \in N$ and k-tuples $\vec{a}, \vec{b}$ we write $⟨ \vec{a} ⟩ <_{k} ⟨ \vec{b} ⟩$ for the usual lexicographic ordering induced by the ordering < on components. For any set u we write $<_{k}^{u} ⟨ \vec{a} ⟩$ for the set ${⟨ \vec{b} ⟩ \in tc (u) : ⟨ \vec{b} ⟩ <_{k} ⟨ \vec{a} ⟩}$ , where $⟨ \vec{b} ⟩$ ranges over k-tuples. We write $⟨ \vec{b} ⟩ <_{k}^{u} ⟨ \vec{a} ⟩$ instead of $⟨ \vec{b} ⟩ \in <_{k}^{u} ⟨ \vec{a} ⟩$ .

When doing course-of-values recursion we use the notation $\begin{matrix} f_{<_{k}^{u} ⟨ \vec{b} ⟩} (\vec{p}, -) : = ⋃_{⟨ \vec{c} ⟩ <_{k}^{u} ⟨ \vec{b} ⟩} {⟨ \vec{c} ⟩} \times f (\vec{p}, \vec{c}) . \end{matrix}$ where the dash − indicates the last k arguments of f.

We introduce the bound u because the collection of all tuples $⟨ \vec{b} ⟩$ such that $⟨ \vec{b} ⟩ <_{k} ⟨ \vec{a} ⟩$ is typically not a set. Note that $<_{k}$ is well-founded on k-tuples, in the sense that for any formula φ in the language of set theory, if $φ (\vec{p}, \vec{a})$ holds for some k-tuple $⟨ \vec{a} ⟩$ then there is some $<_{k}$ minimal k-tuple $⟨ \vec{b} ⟩$ such that $φ (\vec{p}, \vec{b})$ holds.

We will use the following strengthening of course-of-values recursion to simulate ${CRSF}_{\subseteq}^{+}$ in $RS$ .

Definition 10.4.

For $k \in N$ , the function f is obtained from g by subset-bounded k-lexicographic recursion with bound h if $\begin{matrix} f (\vec{p}, u, \vec{a}) = g (\vec{p}, u, \vec{a}, f_{<_{k}^{u} ⟨ \vec{a} ⟩} (\vec{p}, u, -)) \cap h (\vec{p}, u, \vec{a}) . \end{matrix}$ We call u the domain of the recursion.

Theorem 10.5.

For each $k \in N$ , the class $RS$ is closed under subset-bounded k-lexicographic recursion.

Proof.

We use induction on k. The case $k = 1$ is just the usual course-of-values recursion as discussed in Section 8. The proof of Corollary 8.8, that this is available in ${CRSF}_{\subseteq}^{+}$ , relies on the subset-bounded recursion and union schemes and exactly the same proof goes through for $RS$ .

Suppose $k > 1$ . For clarity we will suppress the parameters $\vec{p}$ . We will assume that $g (u, \vec{a}, S) \subseteq h (u, \vec{a})$ always, by replacing g with $g \cap h$ if necessary, and we will write ${\vec{a}}_{2}$ and ${\vec{b}}_{2}$ instead of $a_{2}, \dots, a_{k}$ and $b_{2}, \dots, b_{k}$ . We have $\begin{matrix} f (u, \vec{a}) = g (u, \vec{a}, f_{<_{k}^{u} ⟨ \vec{a} ⟩} (u, -)) \end{matrix}$ with $g, h \in RS$ . Let $f^{'}$ be defined by the $(k - 1)$ -lexicographic recursion $\begin{matrix} f^{'} (u, \vec{a}, S) : = g (u, \vec{a}, S \cup R (u, a_{1}, f_{<_{k - 1}^{u} ⟨ {\vec{a}}_{2} ⟩}^{'} (u, a_{1}, -, S))) \end{matrix}$ where R is the function $\begin{matrix} R (u, a_{1}, Z) : = {⟨ ⟨ a_{1}, {\vec{b}}_{2} ⟩, y ⟩ : ⟨ ⟨ {\vec{b}}_{2} ⟩, y ⟩ \in Z and ⟨ a_{1}, {\vec{b}}_{2} ⟩ \in tc (u)} \end{matrix}$ whose purpose is to prepend elements of a course-of-values Z over $<_{k - 1}^{u} ⟨ {\vec{a}}_{2} ⟩$ with $a_{1}$ , and remove any which could not then be elements of a course-of-values over $<_{k}^{u} ⟨ \vec{a} ⟩$ . By the inductive hypothesis $f^{'} \in RS$ . Define a function F by $\begin{matrix} F (u, a_{1}) = f_{<_{k}^{u} ⟨ a_{1}, \vec{0} ⟩} (u, -) \end{matrix}$ where $\vec{0}$ stands for the $(k - 1)$ -tuple of empty sets.

We claim that for all $\vec{a}$ and u, $\begin{matrix} f^{'} (u, \vec{a}, F (u, a_{1})) = f (u, \vec{a}) . \end{matrix}$ To see this, fix u and $a_{1}$ and use $<_{k - 1}$ -induction on ${\vec{a}}_{2}$ . For the inductive step, suppose that for all $⟨ {\vec{b}}_{2} ⟩ <_{k - 1} ⟨ {\vec{a}}_{2} ⟩$ we have $\begin{matrix} f^{'} (u, a_{1}, {\vec{b}}_{2}, F (u, a_{1})) = f (u, a_{1}, {\vec{b}}_{2}) . \end{matrix}$ By definition $\begin{matrix} (2) & f^{'} (u, a_{1}, {\vec{a}}_{2}, F (u, a_{1})) = g (u, a_{1}, {\vec{a}}_{2}, Z) \end{matrix}$ where $\begin{array}{l} Z & = F (u, a_{1}) \cup R (u, a_{1}, f_{<_{k - 1}^{u} ⟨ {\vec{a}}_{2} ⟩}^{'} (u, a_{1}, -, F (u, a_{1}))) \\ = f_{<_{k}^{u} ⟨ a_{1}, \vec{0} ⟩} (u, -) \cup R (u, a_{1}, ⋃_{⟨ {\vec{b}}_{2} ⟩ <_{k - 1}^{u} ⟨ {\vec{a}}_{2} ⟩} {⟨ {\vec{b}}_{2} ⟩} \times f^{'} (u, a_{1}, {\vec{b}}_{2}, F (u, a_{1}))) \\ = f_{<_{k}^{u} ⟨ a_{1}, \vec{0} ⟩} (u, -) \cup ⋃_{\begin{array}{c} ⟨ {\vec{b}}_{2} ⟩ <_{k - 1}^{u} ⟨ {\vec{a}}_{2} ⟩ \\ ⟨ a_{1}, {\vec{b}}_{2} ⟩ \in tc (u) \end{array}} {⟨ a_{1}, {\vec{b}}_{2} ⟩} \times f^{'} (u, a_{1}, {\vec{b}}_{2}, F (u, a_{1})) \\ = f_{<_{k}^{u} ⟨ a_{1}, \vec{0} ⟩} (u, -) \cup ⋃_{\begin{array}{c} ⟨ {\vec{b}}_{2} ⟩ <_{k - 1}^{u} ⟨ {\vec{a}}_{2} ⟩ \\ ⟨ a_{1}, {\vec{b}}_{2} ⟩ \in tc (u) \end{array}} {⟨ a_{1}, {\vec{b}}_{2} ⟩} \times f (u, a_{1}, {\vec{b}}_{2}) \end{array}$ by the inductive hypothesis. From the definition, $\begin{array}{l} <_{k}^{u} ⟨ \vec{a} ⟩ & = {⟨ b_{1}, {\vec{b}}_{2} ⟩ \in tc (u) : (b_{1} < a_{1}) \lor (b_{1} = a_{1} \land ⟨ {\vec{b}}_{2} ⟩ <_{k - 1} ⟨ {\vec{a}}_{2} ⟩)} \\ = <_{k}^{u} ⟨ a_{1}, \vec{0} ⟩ \cup {⟨ a_{1}, {\vec{b}}_{2} ⟩ \in tc (u) : ⟨ {\vec{b}}_{2} ⟩ <_{k - 1}^{u} ⟨ {\vec{a}}_{2} ⟩} \end{array}$ where we are using that $⟨ a_{1}, {\vec{b}}_{2} ⟩ \in tc (u)$ implies $⟨ {\vec{b}}_{2} ⟩ \in tc (u)$ . It follows that $Z = f_{<_{k}^{u} ⟨ \vec{a} ⟩} (u, -)$ . Therefore the right hand side of (2) is exactly the recursive definition of $f (u, \vec{a})$ , giving us the inductive step.

To finish the proof it is enough to show that F is in $RS$ . We have $\begin{matrix} F (u, a_{1}) = f_{<_{k}^{u} ⟨ a_{1}, \vec{0} ⟩} (u, -) = ⋃_{\begin{array}{c} ⟨ \vec{b} ⟩ \in tc (u) \\ b_{1} < a_{1} \end{array}} {⟨ \vec{b} ⟩} \times f (u, \vec{b}) = ⋃_{\begin{array}{c} ⟨ \vec{b} ⟩ \in tc (u) \\ b_{1} < a_{1} \end{array}} {⟨ \vec{b} ⟩} \times f^{'} (u, \vec{b}, F (u, b_{1})) \end{matrix}$ hence F is definable by course-of-values recursion on $a_{1}$ , using $f^{'}$ . Furthermore since $f \subseteq h$ we have $F (u, a_{1}) \subseteq tc (u) \times ⋃_{⟨ \vec{b} ⟩ <_{k}^{u} ⟨ a_{1}, \vec{0} ⟩} h (u, \vec{b})$ , and this bound is in $RS$ . Hence F is in $RS$ . □

We now generalize the notion of diagram from Definition 2.1.

Definition 10.6.

For $k \in N$ , a k-diagram is a pair $⟨ ⟨ \vec{a} ⟩, E ⟩$ where $⟨ \vec{a} ⟩$ is a k-tuple, and a pair $⟨ ⟨ \vec{x} ⟩, ⟨ \vec{y} ⟩ ⟩$ of k-tuples is in E only if $⟨ \vec{x} ⟩ <_{k} ⟨ \vec{y} ⟩$ . The domain of a k-diagram is defined as $\begin{matrix} dom (⟨ ⟨ \vec{a} ⟩, E ⟩) = {⟨ \vec{a} ⟩} \cup {⟨ \vec{x} ⟩ : there is some pair ⟨ ⟨ \vec{x} ⟩, ⟨ \vec{y} ⟩ ⟩ \in E} . \end{matrix}$

A k-diagram represents the graph with nodes $dom (⟨ ⟨ \vec{a} ⟩, E ⟩)$ and edges given by E.

Definition 10.7.

For $k \in N$ , the k-embedded Mostowski collapse $M_{k}$ is defined by the lexicographic recursion $\begin{matrix} M_{k} (⟨ \vec{a} ⟩, E) = {M_{k} (⟨ \vec{b} ⟩, E) : ⟨ ⟨ \vec{b} ⟩, ⟨ \vec{a} ⟩ ⟩ \in E and ⟨ \vec{b} ⟩ <_{k} ⟨ \vec{a} ⟩} . \end{matrix}$

For convenience we will often treat $M_{k}$ as a one-argument function, writing $M_{k} (Δ)$ to mean $M_{k} (⟨ \vec{a} ⟩, E)$ for a k-diagram $Δ = ⟨ ⟨ \vec{a} ⟩, E ⟩$ . We consider a k-diagram Δ as a code for the set $M_{k} (Δ)$ . Working with codes rather than directly with sets allows us to simulate computations involving sets of higher rank than we could produce in $RS$ . Note that $M_{k}$ itself is not in $RS$ , at least for $k ⩾ 2$ , and that if we add $M_{2}$ to $RS$ it becomes possible to construct # and thus every function in ${CRSF}_{\subseteq}^{+}$ .

We state our main result.

Theorem 10.8.

If $f \in {CRSF}_{\subseteq}^{+}$ then there is a function $F \in RS$ and $k \in N$ such that $F (\vec{a})$ is a k-diagram and $f (\vec{a}) = M_{k} (F (\vec{a}))$ . It follows that the ${CRSF}_{\subseteq}^{+}$ and $RS$ relations are the same, and furthermore that for $f \in {CRSF}_{\subseteq}^{+}$ the function $g (\vec{a}, b) : = f (\vec{a}) \cap b$ is in $RS$ .

This will follow from Theorem 10.10 below, together with the observation that $RS$ contains the function $a \mapsto ⟨ a, \in ↾ {[a]}^{2} ⟩$ which maps a to a 1-diagram coding a. For the last sentence we repeat the proof of Corollary 8.3, using Lemma 10.11 to compute bisimulations in $RS$ .

Definition 10.9.

We say that a function $f (x_{1}, \dots, x_{m})$ is $RS$ -definable on diagrams if for all $k_{1}, \dots, k_{m} \in N$ there is an $RS$ function $F_{\vec{k}} (x_{1}, \dots, x_{m})$ and $ℓ \in N$ such that, for all $Δ_{1}, \dots, Δ_{m}$ where each $Δ_{i}$ is a $k_{i}$ -diagram, $F_{\vec{k}} (Δ_{1}, \dots, Δ_{m})$ is an ℓ-diagram and $\begin{matrix} M_{ℓ} (F_{\vec{k}} (Δ_{1}, \dots, Δ_{m})) = f (M_{k_{1}} (Δ_{1}), \dots, M_{k_{m}} (Δ_{m})) . \end{matrix}$ A relation $r (x_{1}, \dots, x_{m})$ is $RS$ -definable on diagrams if for all $k_{1}, \dots, k_{m} \in N$ there is an $RS$ relation $R_{\vec{k}} (x_{1}, \dots, x_{m})$ such that for all $k_{i}$ -diagrams $Δ_{i}$ $\begin{matrix} R_{\vec{k}} (Δ_{1}, \dots, Δ_{m}) \Leftrightarrow r (M_{k_{1}} (Δ_{1}), \dots, M_{k_{m}} (Δ_{m})) . \end{matrix}$

We show that $RS$ can simulate ${CRSF}_{\subseteq}^{+}$ functions in this sense.

Theorem 10.10.

Every ${CRSF}_{\subseteq}^{+}$ function is $RS$ -definable on diagrams.

The proof of this takes up the rest of this section. The constructions used are similar to those in Section 7.

Lemma 10.11.

For $k, ℓ \in N$ , there is a function $B_{k, ℓ} (⟨ \vec{a} ⟩, E, ⟨ \vec{b} ⟩, F)$ in $RS$ which computes the bisimulation between the k-diagram $⟨ ⟨ \vec{a} ⟩, E ⟩$ and the ℓ-diagram $⟨ ⟨ \vec{b} ⟩, F ⟩$ .

Proof.

First observe that the desired bisimulation is a subset of $dom (⟨ \vec{a} ⟩, E) \times dom (⟨ \vec{b} ⟩, F)$ . We will define $B_{k, ℓ}$ by k-lexicographic recursion on $⟨ \vec{a} ⟩$ with domain E. Suppose we are given $S = {(B_{k, ℓ})}_{↾ <_{k}^{E} ⟨ \vec{a} ⟩} (-, E, ⟨ \vec{b} ⟩, F)$ , that is, the course-of-values of $B_{k, ℓ}$ below $⟨ \vec{a} ⟩$ . Expanding the definition, $\begin{matrix} S = ⋃_{\begin{array}{c} ⟨ \vec{c} ⟩ <_{k} ⟨ \vec{a} ⟩ \\ ⟨ \vec{c} ⟩ \in tc (E) \end{array}} {⟨ \vec{c} ⟩} \times B_{k, ℓ} (⟨ \vec{c} ⟩, E, ⟨ \vec{b} ⟩, F) . \end{matrix}$ Let $⟨ \vec{c} ⟩$ be any E-predecessor of $⟨ \vec{a} ⟩$ . Then $⟨ \vec{c} ⟩ <_{k} ⟨ \vec{a} ⟩$ and $⟨ \vec{c} ⟩ \in tc (E)$ . Hence we can extract from S the bisimulation between $⟨ ⟨ \vec{c} ⟩, E ⟩$ and $⟨ ⟨ \vec{b} ⟩, F ⟩$ using an $RS$ function, as $\begin{matrix} B_{k, ℓ} (⟨ \vec{c} ⟩, E, ⟨ \vec{b} ⟩, F) = {z \in ⋃ ⋃ S : ⟨ ⟨ \vec{c} ⟩, z ⟩ \in S} . \end{matrix}$ We then carry on as in the proof of Lemma 5.7. □

Corollary 10.12.

The relations = and ∈ are $RS$ -definable on diagrams.

Lemma 10.13.

The constant 0 and the functions pairing, ${cond}_{\in} \times$ , ⊙ and # are $RS$ -definable on diagrams.

Proof.

A 1-diagram for 0 is simply $⟨ 0, 0 ⟩$ . For the other functions, suppose we are given a k-diagram $Γ = ⟨ ⟨ \vec{a} ⟩, E ⟩$ and an ℓ-diagram $Δ = ⟨ ⟨ \vec{b} ⟩, F ⟩$ .

For the pairing function we take $m = 1 + k + ℓ$ and construct an m-diagram, whose nodes we will write in the form $⟨ i, \vec{x}, \vec{y} ⟩$ where i is a 1-tuple, $\vec{x}$ is a k-tuple and $\vec{y}$ is an ℓ-tuple. We define an edge relation G, using infix notation for G, by

$⟨ 0, \vec{x}, \vec{0} ⟩ G ⟨ 0, {\vec{x}}^{'}, \vec{0} ⟩$ if and only if $⟨ \vec{x} ⟩ E ⟨ {\vec{x}}^{'} ⟩$

$⟨ 1, \vec{0}, \vec{y} ⟩ G ⟨ 1, \vec{0}, {\vec{y}}^{'} ⟩$ if and only if $⟨ \vec{y} ⟩ F ⟨ {\vec{y}}^{'} ⟩$

$⟨ 0, \vec{a}, \vec{0} ⟩ G ⟨ 2, \vec{0}, \vec{0} ⟩$

$⟨ 1, \vec{0}, \vec{b} ⟩ G ⟨ 2, \vec{0}, \vec{0} ⟩$ .

Note that G respects the ordering

<_{m}

. By (1) and (2),

M_{m} (⟨ 0, \vec{a}, \vec{0} ⟩, G) = M_{k} (Γ)

and

M_{m} (⟨ 1, \vec{0}, \vec{b} ⟩, G) = M_{k} (Δ)

. Thus by (3) and (4),

M_{m} (⟨ 2, \vec{0}, \vec{0} ⟩, G) = {M_{k} (Γ), M_{ℓ} (Δ)}

. The set composition and

{cond}_{\in}

functions are similar (see Lemmas 7.5 and 7.6).

For the smash function # we take $m = k + ℓ$ . Using similar notation for tuples as the previous case, we define an edge relation G on m-tuples by

$⟨ \vec{x}, \vec{y} ⟩ G ⟨ \vec{x}, {\vec{y}}^{'} ⟩$ if and only if $⟨ \vec{x} ⟩ \in dom (Γ)$ and $⟨ \vec{y} ⟩ F ⟨ {\vec{y}}^{'} ⟩$

$⟨ \vec{x}, \vec{b} ⟩ G ⟨ {\vec{x}}^{'}, \vec{y} ⟩$ if and only if $⟨ \vec{x} ⟩ E ⟨ {\vec{x}}^{'} ⟩$ and $⟨ \vec{y} ⟩$ is a source node of F.

We output

⟨ ⟨ \vec{a}, \vec{b} ⟩, G ⟩

For the cartesian product we take $m = 3 + k + ℓ$ . We define an edge relation G by first, for each pair $p \in dom (Γ) \times dom (Δ)$ , putting

$⟨ 0, p, 0, \vec{x}, \vec{0} ⟩ G ⟨ 0, p, 0, {\vec{x}}^{'}, \vec{0} ⟩$ if and only if $⟨ \vec{x} ⟩ E ⟨ {\vec{x}}^{'} ⟩$

$⟨ 0, p, 1, \vec{0}, \vec{y} ⟩ G ⟨ 0, p, 1, \vec{0}, {\vec{y}}^{'} ⟩$ if and only if $⟨ \vec{y} ⟩ F ⟨ {\vec{y}}^{'} ⟩$ .

For each such p, if p has the form

⟨ ⟨ \vec{x} ⟩, ⟨ \vec{y} ⟩ ⟩

where

⟨ \vec{x} ⟩ E ⟨ \vec{a} ⟩

and

⟨ \vec{y} ⟩ F ⟨ \vec{b} ⟩

, meaning that

e_{⟨ \vec{x} ⟩} : = M_{k} (⟨ \vec{x} ⟩, E) \in M_{k} (Γ)

and

f_{⟨ \vec{y} ⟩} : = M_{ℓ} (⟨ \vec{y} ⟩, F) \in M_{ℓ} (Δ)

, then we add six more edges:

$⟨ 0, p, 0, \vec{x}, \vec{0} ⟩ G ⟨ 0, p, 2, \vec{0}, \vec{0} ⟩$

$⟨ 0, p, 0, \vec{x}, \vec{0} ⟩ G ⟨ 0, p, 3, \vec{0}, \vec{0} ⟩$ and $⟨ 0, p, 1, \vec{0}, \vec{y} ⟩ G ⟨ 0, p, 3, \vec{0}, \vec{0} ⟩$

$⟨ 0, p, 2, \vec{0}, \vec{0} ⟩ G ⟨ 0, p, 4, \vec{0}, \vec{0} ⟩$ and $⟨ 0, p, 3, \vec{0}, \vec{0} ⟩ G ⟨ 0, p, 4, \vec{0}, \vec{0} ⟩$

$⟨ 0, p, 4, \vec{0}, \vec{0} ⟩ G ⟨ 1, 0, 0, \vec{0}, \vec{0} ⟩$ .

From (1) and (3), we have

M_{m} (⟨ 0, p, 2, \vec{0}, \vec{0} ⟩, G) = {e_{⟨ \vec{x} ⟩}}

. From (1), (2) and (4), we have

M_{m} (⟨ 0, p, 3, \vec{0}, \vec{0} ⟩, G) = {e_{⟨ \vec{x} ⟩}, f_{⟨ \vec{y} ⟩}}

. From (5),

M_{m} (⟨ 0, p, 4, \vec{0}, \vec{0} ⟩, G) = ⟨ e_{⟨ \vec{x} ⟩}, f_{⟨ \vec{y} ⟩} ⟩

. We output

⟨ ⟨ 1, 0, 0, \vec{0}, \vec{0} ⟩, G ⟩

, which thus by (6) codes the whole set

M_{k} (Γ) \times M_{ℓ} (Δ)

. □

Below we will use small Greek letters to denote tuples of sets. The arity will be clear from the context.

Lemma 10.14.

The transitive closure function is $RS$ -definable on diagrams.

Proof.

Given a k-diagram $Δ = ⟨ α, E ⟩$ , we first claim that there is an $RS$ function computing the ancestor relation on the nodes of Δ.

To see this, for $β ⩽_{k} α$ let $R_{β}$ be the ancestor relation on the graph whose nodes are the set $⩽_{k}^{dom (Δ)} β$ and whose edges are those induced on this set by E. Then $R_{β} \subseteq dom (Δ) \times dom (Δ)$ and can be computed by subset-bounded k-lexicographic recursion, where the form of the recursion is similar to the proof of Lemma 10.11, and we compute $R_{β}$ from earlier values $R_{γ}$ with $⟨ γ, β ⟩ \in E$ as in Lemma 6.15.

We output $⟨ α, E \cup G ⟩$ where G consists of every pair $⟨ β, α ⟩$ such that β is an E-ancestor of α. □

Lemma 10.15.

Embedded Mostowski collapse is $RS$ -definable on diagrams.

Proof.

We are given a k-diagram $⟨ α, G_{a} ⟩$ and an ℓ-diagram $⟨ β, G_{E} ⟩$ . We will construct a set H such that $\begin{matrix} M_{k} (⟨ α, H ⟩) = M (a, E) \end{matrix}$ where $a = M_{k} (⟨ α, G_{a} ⟩)$ and $E = M_{ℓ} (⟨ β, G_{E} ⟩)$ . As in Lemma 7.10, we define $κ (ρ) = M_{k} (⟨ ρ, G_{a} ⟩)$ for k-tuples ρ. We put $\begin{matrix} H = {⟨ ρ, σ ⟩ \in dom (⟨ α, G_{a} ⟩) \times dom (⟨ α, G_{a} ⟩) : ρ <_{k} σ \land κ (ρ) < κ (σ) \land ⟨ κ (ρ), κ (σ) ⟩ \in E} . \end{matrix}$ The proof that this works is the same as for Lemma 7.10.

To construct H in $RS$ , we first observe that $κ (ρ) < κ (σ)$ if and only if $M_{k} (⟨ ρ, G_{a} ⟩) \in tc (M_{k} (⟨ σ, G_{a} ⟩))$ . Since membership and transitive closure are $RS$ -definable on diagrams, this relation is as well. To decide whether $⟨ κ (ρ), κ (σ) ⟩ \in E$ , we first construct a subcircuit computing the bisimulation ∼ between $⟨ α, G_{a} ⟩$ and $⟨ β, G_{E} ⟩$ . Then $⟨ M_{k} (⟨ ρ, G_{a} ⟩), M_{k} (⟨ σ, G_{a} ⟩) ⟩$ is in E if and only if there exist ℓ-tuples $ρ^{'}, σ^{'}$ in $dom (⟨ β, G_{E} ⟩)$ such that $\begin{matrix} ρ \sim ρ^{'} \land σ \sim σ^{'} \land ⟨ M_{ℓ} (⟨ ρ^{'}, G_{E} ⟩), M_{ℓ} (⟨ σ^{'}, G_{E} ⟩) ⟩ \in M_{ℓ} (⟨ β, G_{E} ⟩) \end{matrix}$ and this condition is decidable in $RS$ , since membership and the pairing function relation are $RS$ -definable on diagrams. □

Lemma 10.16.

For $k \in N$ there is an $RS$ function ${Collect}_{k}$ such that, for any set S of k-diagrams, ${Collect}_{k} (S)$ is a $(k + 1)$ -diagram with $\begin{matrix} M_{k + 1} ({Collect}_{k} (S)) = {M_{k} (Δ) : Δ \in S} . \end{matrix}$

Proof.

We write a k-diagram Δ as $⟨ ⟨ {\vec{a}}_{Δ} ⟩, E_{Δ} ⟩$ , and can recover the k-tuple ${\vec{a}}_{Δ}$ and the set $E_{Δ}$ from Δ using $RS$ functions. Define $\begin{matrix} F = ⋃_{Δ \in S} {⟨ ⟨ Δ, \vec{x} ⟩, ⟨ Δ, {\vec{x}}^{'} ⟩ ⟩ : ⟨ ⟨ \vec{x} ⟩, ⟨ {\vec{x}}^{'} ⟩ ⟩ \in E_{Δ}} . \end{matrix}$ That is, for each pair in $E_{Δ}$ we prepend Δ to both k-tuples in the pair, turning them into $(k + 1)$ -tuples, and then take the union over all $Δ \in S$ . The result is that $M_{k + 1} (⟨ ⟨ Δ, {\vec{a}}_{Δ} ⟩, F ⟩) = M_{k} (Δ)$ for each $Δ \in S$ . Then we define $\begin{matrix} G = F \cup {⟨ ⟨ Δ, {\vec{a}}_{Δ} ⟩, ⟨ S, \vec{0} ⟩ ⟩ : Δ \in S} \end{matrix}$ where $\vec{0}$ is a k-tuple of empty sets. Note that the extra edges respect the lexicographic ordering. Finally we output $⟨ ⟨ S, \vec{0} ⟩, G ⟩$ . □

Lemma 10.17.

Suppose g and h are $RS$ -definable on diagrams. Then the function f defined by subset-bounded recursion from g with bound h is $RS$ -definable on diagrams.

Proof.

For simplicity of presentation we will only consider a recursion without parameters – this changes nothing important. So we have $\begin{matrix} f (x) = g ({f (y) : y \in x}, x) \cap h (x) . \end{matrix}$ Suppose that our input x is given as a k-diagram. By assumption there are $ℓ, m \in N$ and a function $H \in RS$ simulating h, which takes as input a k-diagram and outputs an ℓ-diagram, and a function $G \in RS$ simulating g, which takes as input an $(ℓ + 1)$ -diagram (for the previous values) and a k-diagram (for x) and outputs an m-diagram.

Let us name the parts of a diagram, so that $Δ = ⟨ sink (Δ), Edges (Δ) ⟩$ . We claim that there is an $RS$ function $G^{'}$ such that for all k-diagrams Δ and $(ℓ + 1)$ -diagrams Γ, we have that $G^{'} (Γ, Δ) \subseteq Edges (H (Δ))$ and $\begin{matrix} (3) & M_{ℓ} (⟨ sink (H (Δ)), G^{'} (Γ, Δ) ⟩) = g (M_{ℓ + 1} (Γ), M_{k} (Δ)) \cap h (M_{k} (Δ)) . \end{matrix}$ To compute $G^{'}$ , we first compute $G (Γ, Δ)$ , $H (Δ)$ and the bisimulation ∼ between them. To deal with the intersection, we then take the set $Edges (H (Δ))$ and delete from it every edge $⟨ ⟨ \vec{v} ⟩, sink (H (Δ)) ⟩$ for which there is no $⟨ \vec{w} ⟩ \sim ⟨ \vec{v} ⟩$ with the edge $⟨ ⟨ \vec{w} ⟩, sink (G (Γ, Δ)) ⟩$ in $Edges (G (Γ, Δ))$ . We output the result.

We can now define a function simulating f by recursively applying $G^{'}$ . Below, $α, β, γ$ stand for k-tuples. Suppose our input is $⟨ α, E ⟩$ . Define a function $F (β, E)$ , by k-lexicographic recursion on β with domain E as $\begin{matrix} F (β, E) = G^{'} ({Collect}_{ℓ} (S_{β}), ⟨ β, E ⟩) where S_{β} = {⟨ s (γ), F (γ, E) ⟩ : γ <_{k}^{E} β, ⟨ γ, β ⟩ \in E} \end{matrix}$ and we introduce the notation $s (γ)$ for $sink (H (⟨ γ, E ⟩))$ . Recall that the course-of-values of $F (-, E)$ below β on domain E is $\begin{matrix} F_{<_{k}^{E} β} (-, E) : = ⋃_{γ <_{k}^{E} β} {γ} \times F (γ, E), \end{matrix}$ from which we can construct $S_{β}$ in $RS$ . Furthermore this is a subset-bounded recursion, since by the definition of $G^{'}$ we have that $F (β, E) \subseteq Edges (H (⟨ β, E ⟩))$ . Hence F is in $RS$ .

We claim that $M_{ℓ} (⟨ s (β), F (β, E) ⟩) = f (M_{k} (⟨ β, E ⟩))$ . It follows that we can define f on diagrams by setting β to be α. We will use k-lexicographic induction on β. Letting $Δ = ⟨ β, E ⟩$ and $b = M_{k} (Δ)$ , we have $\begin{array}{l} M_{ℓ} (⟨ s (β), F (β, E) ⟩) & = M_{ℓ} (⟨ sink (H (Δ)), G^{'} ({Collect}_{ℓ} (S_{β}), Δ) ⟩) \\ = g (M_{l + 1} ({Collect}_{ℓ} (S_{β})), b) \cap h (b) \\ = g ({M_{ℓ} (⟨ s (γ), F (γ, E) ⟩) : γ <_{k}^{E} β, ⟨ γ, β ⟩ \in E}, b) \cap h (b) \\ = g ({f (M_{k} (⟨ γ, E ⟩)) : γ <_{k}^{E} β, ⟨ γ, β ⟩ \in E}, b) \cap h (b) \\ = g ({f (c) : c \in b}, b) \cap h (b) \\ = f (b) \end{array}$ using, in order, the definition of F, equation (3), the definition of ${Collect}_{ℓ}$ , the inductive hypothesis, and the recursive definitions of $M_{k}$ and f. □

Footnotes

Acknowledgements

Sam Buss is supported in part by NSF grants DMS-1101228 and CCR-1213151, by the Simons Foundation, award 306202, and by the Skolkovo Institute for Science and Technology. Sy-David Friedman is supported by the Austrian Science Fund (FWF) under project number P24654. Moritz Müller is supported by the Austrian Science Fund (FWF) under project number P28699. Neil Thapen is supported in part by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013)/ERC grant agreement 339691. The Institute of Mathematics of the Czech Academy of Sciences is supported by RVO:67985840.

References

Aczel, Non-Well-Founded Sets, CSLI Lecture Notes, Vol. 14, Center for the Study of Language and Information, Stanford, 1988.

Arai, Predicatively computable functions on sets, Archive for Mathematical Logic 54 (2015), 471–485. doi:10.1007/s00153-015-0422-2.

Beckmann,

S.R.

Buss and

S.-D.

Friedman, Safe recursive set functions, Journal of Symbolic Logic 80 (2015), 730–762. doi:10.1017/jsl.2015.26.

Beckmann,

S.R.

Buss,

S.-D.

Friedman,

Müller and

Thapen, Cobham recursive set functions, Annals of Pure and Applied Logic 167 (2016), 335–369. doi:10.1016/j.apal.2015.12.005.

Beckmann,

S.R.

Buss,

S.-D.

Friedman,

Müller and

Thapen, Cobham recursive set functions and weak set theories, in: Sets and Computations, Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore, World Scientific, 2017, pp. 55–116. doi:10.1142/9789813223523_0005.

Cobham, The intrinsic computational difficulty of functions, in: Logic, Methodology and Philosophy of Science, Proceedings of the Second International Congress, Held in Jerusalem, 1964,

Bar-Hillel, ed., North-Holland, Amsterdam, 1965, pp. 24–30.

J.D.

Hamkins and

Lewis, Infinite time Turing machines, Journal of Symbolic Logic 65 (2000), 567–604. doi:10.2307/2586556.

Håstad, Almost optimal lower bounds for small depth circuits, in: Proceedings of the 18-th Annual ACM Symposium on Theory of Computing, 1986, pp. 6–20.

R.B.

Jensen, The fine structure of the constructible hierarchy, Annals of Mathematical Logic 4 (1972), 229–308, Errata, ibid 4 (1972) 443.

10.

G.E.

Sacks, Higher Recursion Theory, Springer-Verlag, Berlin, 1990.

11.

V.Y.

Sazonov, On bounded set theory, in: Logic and Scientific Methods,

M.L.

Dalla Chiara ,

Doets ,

Mundici ,

van Benthem , eds, Synthese Library, Vol. 259, Kluwer Academic, 1997, pp. 85–103. doi:10.1007/978-94-017-0487-8_5.

12.

Schindler,

P \neq N P

for infinite time Turing machines, Monatshefte für Mathematik 139 (2003), 335–340. doi:10.1007/s00605-002-0545-5.

Feasible set functions have small circuits

Abstract

Keywords

1. Introduction

2. Preliminaries

2.1. Notational conventions

2.2. Embedded Mostowski collapse

1 Aczel [1] defines an accessible pointed graph as one with a distinguished node from which every other node is reachable. Note that our paths run in the opposite direction.

5.1. a-Strings

Footnotes

Acknowledgements

References

¹
Aczel [1] defines an accessible pointed graph as one with a distinguished node from which every other node is reachable. Note that our paths run in the opposite direction.