Effectivity and reducibility with ordinal Turing machines

Abstract

This article expands our work in (LNCS 9709 (2016), 225–233). By its reliance on Turing computability, the classical theory of effectivity, along with effective reducibility and Weihrauch reducibility, is only applicable to objects that are either countable or can be encoded by countable objects. We propose a notion of effectivity based on Koepke’s Ordinal Turing Machines (OTMs) that applies to arbitrary set-theoretical $Π_{2}$ -statements, along with according variants of effective reducibility and Weihrauch reducibility. As a sample application, we compare various choice principles with respect to effectivity.

Keywords

Effective reducibility ordinal computability

1. Introduction

In mathematics, it has always been of interest to what extent theorems claiming the existence of certain objects are ‘effective’ in the sense that a procedure—an algorithm—can be found that produces an object of the desired kind. In the case of a $Π_{2}$ -statements, which, roughly, are claims that, for every x from a certain range of objects, there is a y from another such range such that x and y relate in a certain (simple) way, effectivity would then mean that some appropriate y can be obtained effectively from a given x. In the finite realm, such questions are studied by the theory of Weihrauch reducibility, see e.g. [3].

With the notion of Turing computability serving as a formalization of the notion of a ‘procedure’, such questions can be turned into mathematical questions that potentially have provable answers; recursive analysis is an example of an area that deals with such questions (see e.g. [16]).

A large amount of standard theorems, however, turn out to be ‘ineffective’ in this sense. For these theorems, it is still possible to compare their remoteness from effectivity by asking whether one $Π_{2}$ -statement, say ϕ, becomes effective once an effectivization for the other, say ψ, is given as an oracle. This yields the notion of effective reducibility. Insisting that only one instance of ψ may be requested when processing an instance of ϕ, one obtains the stronger notion of Weihrauch reducibility. All of these concepts have given rise to thriving areas of mathematics.

However, the reliance on Turing computability has the effect that the areas of mathematics thus surveyed are limited to countable objects or objects that, like separable spaces, can be encoded by countable objects. On the other hand, there seems to be an intuition of effectiveness even for general set theory; see e.g. [19].

So far, the literature on effectivity notions for the uncountable is rather sparse; we mention on the one hand Hodges [19], which is the first such approach known to us, and further [17], in particular the contribution by Shore [26]. While this leads to effectiveness notions suitable for the uncountable, suitable analogues of effective reducibility and Weihrauch reducibility remain unconsidered, save for a remark in [26].

The first paper dealing with effective (Weihrauch) reducibility in the uncountable realm was [6], where such notions were defined and some basic methods for their study were presented and applied. The guiding idea of [6] was to retain the usual definitions as far as possible while replacing Turing machines with Koepke’s Ordinal Turing Machines (OTMs) (see e.g. [22]), that have a working tape of proper class length, the cells of which are indexed by ordinals, and additionally work along an ordinal ‘time axis’. A related piece of work is Galeotti and Nobrega [15], where a notion of Weihrauch reducibility based on OTMs was applied to various problems on generalized real numbers.

In this paper, we will expand the work started in [6] by (i) extending the realm of methods for obtaining results, (ii) considerably extending the number of applications by investigating how various set-theoretical choice principles compare in the sense of ordinal Weihrauch reducibility, (iii) considering connections between reducibility and provability and (iv) extending the notions of reducibility from [6] to arbitrary set-theoretical statements.

Many of the results explained here will also appear in the forthcoming [7], and we want to express our gratitude both to the editors of Computability and the de Gruyter publishing company for the kind permission to use parts of this article in [7] and vice versa. Finally, this paper extends [6] in the sense that the contents of Section 2 and parts of the contents of Sections 3 and 4 can be found there. In most cases, we again present the result, but refer to [6] for proofs.

2. Setting the stage

In this section, we will briefly recall the underlying model of computation, namely Koepke’s Ordinal Turing Machines (OTMs) and then work towards appropriate notions of effectivity and reducibility for functions and problems on arbitrary sets.

2.1. Ordinal Turing machines

Ordinal Turing Machines (OTMs) were introduced by Koepke in [22] as a “symmetric” variant of the Infinite Time Turing Machines of Hamkins and Kidder that were introduced in [18]. The same concept was obtained almost at the same time independently by Dawson and is contained in his thesis [11].

Programs for OTMs are just regular Turing programs, where we imagine the inner states to be indexed by natural numbers. Also, like classical Turing machines, OTMs have a finite number of tapes, split into cells, each of which can contain one element of the alphabet ${0, 1}$ ; moreover, as usual, there is a read-write-head for each tape that moves along the cells, reads out the symbol on the current cell and can replace it when instructed to do so. However, both the “hardware” and the working time of OTMs are considerably expanded: The tape of an OTM has proper class length On, with one cell for each ordinal, and programs are carried out along an ordinal “time axis”. At successor times, an OTM behaves like a classical Turing machine, with the additional rule that, if the head is commanded to go to the left while currently occupying a cell indexed by a limit ordinal, it is reset to the start of the tape, i.e. the cell indexed 0. At limit times, for each cell c, the content of c is the inferior limit of the sequence of earlier contents of c, and likewise, the index of the active program line and the head position are obtained as the inferior limits of the sequence of earlier values. For an explication of OTMs in formal detail, we refer the reader to [22]. In this paper, we will only consider parameter-free OTMs, i.e. we always start with an empty working tape.

In our framework, OTMs work with four tapes, one input tape $T_{in}$ , one working tape T, one output tape $T_{out}$ and one “miracle” tape $T_{m}$ that will be explained below. Occasionally, we will also use a fifth tape, the “oracle tape” $T_{o}$ , for storing extra information. An input for an OTM is always a set or class X of ordinals, which is given to the OTM by writing a 1 on the ιth cell of $T_{in}$ if and only if $ι \in X$ , and otherwise a 0.1

¹
Sometimes, when X is a set, it will be important to know where it ‘stops’, i.e. to know some upper bound for X, e.g. to be able to “exhaustively search” through X. This can clearly be arranged in a number of ways (e.g. by having two input tapes, one for inputs and one for bounds), but in order to simplify our presentation, we will not discuss this point any further.

Thus, OTMs can compute on sets or classes of ordinals. In order to make OTMs compute on sets, we need to fix some encoding of sets by sets of ordinals, which we do as follows: For a transitive set x, pick some bijection

f : α \to x

between x and some ordinal, and then let

c_{f} (x) : = {p (ι, ζ) : ι, ζ \in α \land f (ι) \in f (ζ)}

. Then

c_{f} (x)

is an “α-code for x via f”; when c is an α-code for x via f for some α and f, we say that c “codes” x. Now, for arbitrary sets x, a code for x is a code for

{x} \cup tc (x)

, where

tc (x)

denotes the transitive closure of x.

Thus, OTMs can be used to compute on arbitrary sets, and we can say that a (class) function $F : V^{n} \to V$ (where V is the set-theoretical universe) is OTM-computable if and only if there is an OTM-program P such that, for each $(x_{1}, \dots, x_{n}) \in V^{n}$ and each set c of ordinals that codes $(x_{1}, \dots, x_{n})$ , P will, when run with c on the input tape and all other tapes empty, eventually halt with some d on the output tape such that d codes $F (x_{1}, \dots, x_{n})$ . Note that we allow the specific code written to the output tape to depend on the code chosen for the input. If $X \subseteq V$ is such that, for any OTM-computable $F : V \to V$ and any $x \in X$ , we have $F (x) \in X$ , then we call X ‘closed under OTM-computability’ or ‘OTM-closed’. Similarly, a class $X \subseteq On$ is OTM-decidable if and only if there is an OTM-program that, on input c coding x, halts with output 1 if and only if $x \in X$ and otherwise halts with output 0.

We recall a few results about OTMs that will be relevant below. Theorem 1.

[Seyfferth, Schlicht, [ 25 ]] A set x is coded by an OTM-computable set if and only if $x \in L_{σ}$ , where σ is minimal such that $L_{σ} ≺_{Σ_{1}} L$ .

[Koepke, [ 22 ]] There is a (non-halting) OTM-program $P_{L}$ that “enumerates L”, i.e. that successively writes codes for all constructible sets (and no others) to the output tape.

[Koepke, [ 22 ]] There is an OTM-program $P_{truth}$ such that, for any $Δ_{0}$ -statement ϕ and all sets $x_{1}, \dots, x_{n}$ , $P_{truth} (⌊ ϕ ⌋, c (x_{1}), \dots, c (x_{n}))$ halts with the truth value of $ϕ (x_{1}, \dots, x_{n})$ on the output tape. Here, $⌊ ϕ ⌋$ is the Gödel number of ϕ and $c (x_{1}), \dots, c (x_{n})$ are codes for the sets $x_{1}, \dots, x_{n}$ .

2.2. Effectivity of

Π_{2}

-statements

It has become customary to associate the term “effective” with “recursive” in mathematical contexts. However, as e.g. Hodges has pointed out in [19], there is apparently an intuition about a notion of effectiveness that goes beyond Turing computability, according to which e.g. forming quotient fields of integral domains is effective, while obtaining maximal ideals of rings is not (cf. Hodges, [19], p. 1). Hodges proposes a variant of the primitive recursive set functions of Jensen and Karp [21] as a formalization of this notion. Partly motivated by our argument in [5] that there are good reasons to accept OTMs as a formal counterpart to the intuitive notion of “higher effectivity”, we base our approach on OTMs instead.2

²
Though not formally equivalent, the two approaches agree with respect to the problems considered by Hodges.

Another reason is that the OTM-approach seems more suited to considering reducibility between problems, which is not considered by Hodges. A slight change in perspective is that the emphasis in Hodges’ paper is on “construction problems”, while ours is on statements. However, for the transition from “problems” to “statements”, it suffices to note that

Π_{2}

-statements are naturally associated with “problems”:

Let ϕ be a $Π_{2}$ -sentence in the language of set theory, say ϕ is $\forall x \exists y ψ (x, y)$ , where ψ is $Δ_{0}$ . We say that ϕ is “witnessed” by the proper class function $F : V \to V$ if and only if $ψ (x, F (x))$ holds for all $x \in V$ . In this case, we also call F a “canonification” of ϕ.

More generally, when $R \subseteq V \times V$ is a binary relation on sets, we say that F is a canonification of R if and only if, for every $x \in V$ , we have $R (x, F (x))$ .

Definition 2.

A binary relation $R \subseteq V \times V$ is ‘OTM-effective’ if and only if there is an OTM-computable canonification F for R. Fixing the notation $R_{ψ} : = {(x, y) : ψ (x, y)}$ for a $Δ_{0}$ -formula ψ, we say that the $Π_{2}$ -statement $ϕ \equiv \forall x \exists ψ (x, y)$ with $ψ \in Δ_{0}$ is OTM-effective if and only if $R_{ψ}$ has an OTM-computable canonification F; in this case, we also say that F is a canonification for ϕ.

We say that an OTM-program P is “functional” if and only if P computes a class function $F : V \to V$ . When P is functional, we denote the function computed by it by $F_{P}$ .

In fact, this definition of effectivity can be generalized to arbitrary sentences in the language of set theory by (roughly) replacing Turing machines with OTMs in Kleene’s realizability interpretation intuitionistic logic. The above definition then becomes a special case of this more general approach and one can show that the axioms of KP are OTM-effective, while the “impredicative” ZFC-axioms, like the power set axiom or separation for formulas with arbitrary use of unbounded quantifiers, are not. We will briefly touch on this topic in Section 6 below and further refer the interested reader to [7,8] and the detailed study [9] for more information. We fix some further terminology. For $F : V \to V$ , $X \subseteq V$ , we say that X is F-closed if and only if $F (x) \in X$ for all $x \in X$ .

For $R \subseteq V^{2}$ , X is R-closed if and only if it is F-closed for some canonification F of R. Moreover, for $R \subseteq V^{2}$ , $X \subseteq V$ , we let $R [X] : = {y : \exists x \in X (x, y) \in R}$ and $R^{- 1} [X] : = {x : \exists y \in X (x, y) \in R}$ .

Clearly, every OTM-effective $Π_{2}$ -statement ϕ holds in V. If we also require ϕ to be “provably OTM-effective”, i.e. that the existence of the desired program is provable in ZFC, then ϕ will be provable in ZFC. We will see below that not every $Π_{2}$ -consequence of ZFC must be OTM-effective. However, if the universe is small, this is indeed the case: Proposition 3.

If $V = L$ , then every $Π_{2}$ -consequence of ZFC is effective.

Proof.

Let $ϕ \equiv \forall x \exists y ψ (x, y)$ be a $Π_{2}$ -consequence of ZFC, where ψ is $Δ_{0}$ . Given a code c for a set x on the input tape, run $P_{L}$ from Theorem 1. Whenever $P_{L}$ outputs a code $c^{'}$ for a set y, use $P_{truth}$ to check whether $ψ (x, y)$ holds. If not, continue with $P_{L}$ . Otherwise, output $c^{'}$ and halt. Clearly, this will compute a canonification of ϕ. □

2.3. Reducibility

Though studying the effectivity, or otherwise, of various mathematical statements is certainly an extensive and worthwhile task, we will mostly be concerned with a more general notion, namely the “reducibility” of one statement or problem to another. In order to formalize this, we need to be able to use class functions $F : V \to V$ as “oracles”. We will write $P^{F}$ to indicate that the OTM-program P is run in the oracle F. This is where the “miracle tape” $T_{m}$ comes in. We reserve a special inner state s as our “miracle command”. Now, whenever the state s is assumed during a run of $P^{F}$ , the following takes place: The content of $T_{m}$ is read out; if it does not code a set, nothing further happens and the program execution is continued. Otherwise, if it codes the set x, then the content of $T_{m}$ is replaced with a code for $F (x)$ and then the execution of the program is continued. Thus, whenever the state s is assumed, a code for the F-image of the set coded by the content of the miracle tape appears on the miracle tape.

We recall some standard notation. As usual $Q \circ R$ will denote the composition of the (possibly proper class) relations or functions Q and R. By slight abuse of notation, we will also write $F \circ P$ or $P \circ Q$ for functional OTM-programs P, Q and a (class) function F to denote the (class) function obtained by composing F with $F_{P}$ or $F_{P}$ with $F_{Q}$ . When F and G are (class) functions or functional OTM-programs, $(F, G)$ denotes the “parallelization” of F and G, i.e. the function mapping a set x to the ordered pair $(F (x), G (x))$ .

Now we can define our reducibility relations:

Definition 4.
Let $R, R^{'} \subseteq V^{2}$ . We say that R is “OTM-reducible” to $R^{'}$ if and only if the following holds: There is an OTM-program P such that, for every canonification F of $R^{'}$ , $P^{F}$ computes a canonification of R. In this case, we write $R ⩽_{OTM} R^{'}$ .

In this setting, arbitrarily many instances of $R^{'}$ may be used in computing a canonification of R. We may also demand that each instance of R is reduced to a single instance of $R^{'}$ . This yields the following reducibility notion, adapted from the classical notion of Weihrauch reducibility (see e.g. [2]) which is the one we will be primarily interested in in this article:
Definition 5.
Let $R, R^{'} \subseteq V^{2}$ . We say that R is “ordinal Weihrauch reducible” to $R^{'}$ if and only if there are functional OTM-programs P and Q such that, for every canonification $F^{'}$ of $R^{'}$ , $F_{P} \circ (F^{'}, id) \circ F_{Q}$ is a canonification of R (where $id : V \to V$ denotes the identity function).

In this case, we write $R ⩽_{oW} R^{'}$ and say that $[P, Q]$ witnesses the ordinal Weihrauch reducibility of R to $R^{'}$ .3
³
In [6], the notation was $⩽_{gW}$ for ‘generalized Weihrauch reducibility’. D. Dzhafarov pointed out in his review of [6] that this name is already taken and suggested ‘ordinal Weihrauch reducible’ instead, a suggestion which we thankfully follow here.

The corresponding concepts and notations for $Π_{2}$ -statements are defined in the obvious way.

If the above holds with $F_{P} \circ F^{'} \circ F_{Q}$ being a canonification of R (i.e. with the identity function deleted in the middle term), we say that R is ‘strongly ordinal Weihrauch reducible’ to $R^{'}$ and write $R ⩽_{soW} R^{'}$ .

For each of these reducibility relations, we write $R \equiv_{i} R^{'}$ with the respective index i to express that $R ⩽_{i} R^{'}$ and $R^{'} ⩽_{i} R$ .

If $ϕ (x, y)$ is an ∈-formula, we write $R_{ϕ}$ for the construction problem ${(x, y) \in V^{2} : ϕ (x, y)}$ and call $R_{ϕ}$ the associated construction problem for ϕ. If $ϕ \equiv \forall x \exists y ϕ^{'} (x, y)$ and $ψ \equiv \forall x \exists y ψ^{'} (x, y)$ are $Π_{2}$ -statements, we write $ϕ ⩽_{i} ψ$ to indicate that $R_{ϕ^{'}} ⩽_{i} R_{ψ^{'}}$ . If θ is another $Π_{2}$ -formula, we write $ϕ ⩽_{i} ψ \circ θ$ for $R_{ϕ} ⩽_{i} R_{ψ} \circ R_{θ}$ .

Thus, in ordinal Weihrauch reducibility, the “preprocessed input” set $F_{Q} (x)$ is retained and passed on to $F_{P}$ for further processing, while in strong Weihrauch reducibility, it is “forgotten”. We note the obvious fact that strong ordinal Weihrauch reducibility implies ordinal Weihrauch reducibility, which in turn implies OTM-reducibility. We will see below that the second implication cannot be reversed. For the first one, this is easy to see: For example, every OTM-effective function $F : V \to V$ is $⩽_{oW}$ -reducible to any relation $R \subseteq V \times V$ , while, for instance, when $id$ and 0 denotes the identitity and the constant zero function on V, respectively, then $id ≰_{sOW} 0$ , as the image of $F \circ 0 \circ G$ will be $\subseteq {0}$ for any choice of F and G, while the image of $id$ is clearly class-sized. This idea is well-known from the classical setting; see Proposition 12 below for a general version. Though $⩽_{oW}$ seems to be the more natural reducibility relation, most reducibility results we will prove below will in fact be strong reducibilities, a phenomenon also well-known from the classical setting. (Our nonreducibility results, however, will mostly apply to $⩽_{oW}$ .)

Furthermore, we note that all three reducibility relations are reflexive and transitive and the corresponding ≡-relations are thus equivalence relations.

We have stated the definitions of effectivity and reducibility in terms of proper classes. While this has the advantage of expressing the intuition behind these concepts most straightforwardly and is also in agreement with the approach taken in [6], it has some less attractive technical consequences in the proofs; for example, in the considerations about versions of the axiom of choice, we assume global choice in the background theory. This could be avoided4
⁴
We thank our anonymous referee for pointing this out to us.

by defining canonifications and reductions not on the whole set-theoretical universe, but rather on set-sized restrictions thereof, such as the levels $V_{α}$ . The proofs below would then go through in ZF. However, for the sake both of simplicity and keeping the concepts intuitive, we phrase our results in terms of classes. Remark 6.
To avoid misunderstandings, a note may be in order about the relation of ordinal Weihrauch reducibility to Weihrauch reducibility in the classical setting. In the classical theory of Weihrauch reducibility, it is not required that the reduction is coding-independent, i.e. yields same result on a code of a set x, no matter which code is chosen. In fact, demanding coding-independence in the classical setting would have rather detrimental effects, see e.g. [4]. We thank A. Pauly for pointing this out to us.

3. Basic methods

In this section, we will recall the methods for proving non-reducibility that we adapted in [6] from the methods used by Hodges in [19] for proofs of non-effectivity and add some more possibilities adapted from the classical theory of Weihrauch degrees, see [2].

Our first method for proving nonreducibility is adapted from Hodges’ “cardinality method”, see Lemma 3.2 of [19]. First, let us fix some terminology (cf. Hodges, [19]): For $α \in On$ , we say that a class function $F : V \to V$ ‘raises cardinalities above α’ if and only if there is some set x with $| tc (x) | ⩾ α$ such that $| F (x) | > | tc (x) |$ . For $R \subseteq V^{2}$ , we say that R raises cardinalities above α if and only if every canonification of R raises cardinalities above α.

Lemma 7 (Cf. [19], Lemma 3.2).

Let $R, R^{'} \subseteq V^{2}$ , and let α be an infinite ordinal. Suppose that R raises cardinalities above α and $R ⩽_{OTM} R^{'}$ . Then $R^{'}$ raises cardinalities above α. Thus, a relation that raises cardinalities above α is not OTM-reducible—and hence also not ordinal Weihrauch reducible—to one that does not.

In particular, if R raises cardinalities above ω, then R is not effective.

Proof.
See [6], Lemma 1. The main ingredient is the well-known observation that OTM-computations cannot output sets of larger cardinalities than their input when the latter is infinite. □

We note some sample applications:
Corollary 8 (Cf. [6], Lemma 2).

None of the following relations is effective:

The relation between an ordinal and its cardinal successor.

The relation between an ordinal and its cardinal successor in L. 5

⁵
This requires relativizing the above to L.

The relation between a set and its (constructible) power set.

The relation between a linear ordering and its completions.

For the separation of $Π_{2}$ -statements, however, the cardinality method is useless, as binary $Π_{2}$ -relations never raise cardinalities for any infinite α by an easy collapsing argument.

Our second method is adapted from Hodges’ “Forcing Method”, see Hodges [19], Lemma 3.7. The idea is that, when $M \subseteq V$ is OTM-closed and $R^{'}$ -closed, then $R ⩽_{oW} R^{'}$ implies that it is also R-closed. Thus, to show that $R ≰_{oW} R^{'}$ , it suffices to find some OTM-closed set or class M with some $x \in M$ such there is no $y \in M$ with $(x, y) \in R$ .

If X satisfies the well-ordering principle and thus contains codes for all of its elements, then in order to guarantee OTM-closure, it suffices that M is a union of transitive KP-models that contain all ordinals (or is even only of sufficient ordinal height).

Below, we will be particularly interested in separating various versions of the axiom of choice. Thus, M will in general not satisfy the well-ordering principle. The problem is that, in this case, OTM-closure is not obvious: As M will not contain encodings for all of its elements, it will also not contain the corresponding computations and is thus not guaranteed to contain the set coded by the output. The idea then is that, for $x \in M$ , there should be two mutually generic filters $G_{0}$ , $G_{1}$ for some forcing that makes x well-ordered. $M [G_{0}]$ and $M [G_{1}]$ will contain codes for x and also all halting OTM-computations on these codes, along with their outputs and the sets they code. For an OTM-program P that computes a class function $F_{P} : V \to V$ , we will thus have $F (x) \in M [G_{0}] \cap M [G_{1}]$ , and if M is a model of sufficiently much set theory to guarantee that $M [G_{0}] \cap M [G_{1}] = M$ , it follows that $F (x) \in M$ , as desired.

Thus, it is necessary to guarantee the existence of the required filters. This requires some extra assumption beyond ZFC. Indeed, as noted above (see Proposition 3), some largeness assumption is necessary, for under $V = L$ , all $Π_{2}$ -consequences of ZFC are (trivially) ordinal Weihrauch reducible to each other. To prove the results below, one needs to ensure the existence of certain generic filters, which follows from the (rather harmless) extra assumption that some sufficiently large L-cardinal is countable in V.6

⁶

This will in particular follow when we assume that $0^{♯}$ exists, as it implies that every forcing with a parameter-free definition in L is countable and thus has a generic filter, see e.g. p. 59 of Friedman [14], thereby covering all cases we are interested in below.

For a set x, we denote by $P_{x}$ the set ${f : ω \to {x} \cup tc (x) | f finite}$ , partially ordered by ⊆, which forces x to be well-ordered in order type ω. Theorem 9 (Cf. [6], Thm. 8).

Let $R, R^{'} \subseteq V^{2}$ , and let M be an increasing union of transitive, class-sized KP-models such that $M \cap On = On$ . Suppose that there are a canonification $F^{'}$ of $R^{'}$ and a set x such that M is $F^{'}$ -closed, but does not contain a y with $(x, y) \in R$ . Moreover, suppose that there are two filters $G_{0}$ and $G_{1}$ that are mutually $P_{x}$ -generic over M. Then $R ≰_{oW} R^{'}$ .

Proof.
See [6]. We sketch the proof for the convenience of the reader: The condition on $G_{0}$ and $G_{1}$ implies that x has codes in $M [G_{0}]$ and $M [G_{1}]$ ; also, the forcing will preserve enough of KP so that all halting OTM-computations starting on these codes will be contained in both extensions. So both extensions will contain the coded set, which will thus lie in the intersection. Thus $(F_{P} \circ (F^{'}, id) \circ F_{Q}) (x)$ will be contained in M for all functional OTM-programs P and Q, while by assumption, no y with $(x, y) \in R$ is contained in M. Hence, there are no P and Q that witness the ordinal Weihrauch reducibility of R to $R^{'}$ , as desired. □
Remark.
The condition that M contains all ordinals is unnecessarily strong: It is only needed to ensure that the generic extensions are “long” enough so that all OTM-computations that do in fact halt halt there. Further, the condition “increasing union of transitive, class-sized KP-models” can be further weakened e.g. to M being a model of Mathias’ provident set theory (see [24]). So far we have not found applications for these variants.

3.1. Further methods

We mention a few other ways for proving nonreducibility. In general, many of the methods used in the classical theory of Weihrauch reducibility depend so little on the specific model of computation that they immediately carry over to our context; we give two examples of this observation, namely Propositions 10 and 12. The intuition between the following two propositions is that, when R is ordinal Weihrauch reducible to $R^{'}$ and there are subclasses X and Y of V that are closed under OTM-computability such that, for all $x \in X$ , there is $y \in Y$ with $(x, y) \in R^{'}$ , then the same holds for R; more informally, when ‘simple’ instances of $R^{'}$ have ‘simple solutions’, then the same holds for R.

Proposition 10 (For the classical version, cf. Brattka et al., [2], Proposition 12.1).

When A is a set or a class of ordinals, a set x is called OTM-computable in A if and only if there is an OTM-program P such that, when P is run with A on the oracle tape, it halts with a code for x on the output tape.

Now let A and B be classes of ordinals, and let $R, R^{'} \subseteq V^{2}$ . Suppose that, whenever x is OTM-computable in A, then there is some y that is OTM-computable in B such that $(x, y) \in R^{'}$ and that $R ⩽_{oW} R^{'}$ . Then it also holds that, whenever x is OTM-computable in A, then there is some y that is OTM-computable in B such that $(x, y) \in R$ .

In particular, when there is a canonification of $R^{'}$ that sends each OTM-computable set to an OTM-computable set and $R ⩽_{oW} R^{'}$ , then there is such a canonification for R as well.

Proof.
The proof is the same as that for the classical version in [2]: Assume that the assumptions of the proposition are satisfied, let $[P, Q]$ witness the reducibility of R to $R^{'}$ , and let x be OTM-computable in A. Let $\hat{x}$ be the set coded by the output of Q when run on a code for x as its input. Then $\hat{x}$ is also OTM-computable in A. Thus, by assumption, there is a set $\hat{y}$ that is OTM-computable in B such that $(\hat{x}, \hat{y}) \in R^{'}$ . Similarly, if y is the set coded by the output of P when run on a code for $\hat{y}$ as its input, then y is OTM-computable in B, as y is. As $[P, Q]$ witnesses the ordinal Weihrauch reducibility of R to $R^{'}$ , we have $(x, y) \in R$ . Thus y is as desired. □

For $c \subseteq On$ , $σ^{c}$ denotes the supremum of the halting times of OTMs that start with c on the oracle tape. For a set x, we let $σ^{x} : = min {σ^{c} : c codes x}$ .
Proposition 11.
Let $R, R^{'} \subseteq V^{2}$ such that $R ⩽_{oW} R^{'}$ , and let $X \subseteq V$ be OTM-closed and $α \in On$ . Suppose that, for every $x \in X$ , there is y such that $(x, y) \in R^{'}$ and $σ^{y} < α$ . Then it also holds that, for every $x \in X$ , there is $y \in Y$ such that $(x, y) \in R$ and $σ^{y} < α$ .

In particular, if any OTM-computable instance x of $R^{'}$ has a solution y with $σ^{y} < α$ , then the same is true of R.
Proof.
Let $[P, Q]$ witness the reduction of R to $R^{'}$ and let $x \in X$ be an instance of R. Let $x^{'}$ be the set coded by the output $c^{'}$ of $Q (c)$ when c codes x. Then $σ^{c^{'}} ⩽ σ^{c} < α$ by transitivity of computations. By assumption on $R^{'}$ , there is $y^{'}$ with a code $d^{'}$ such that $(x^{'}, y^{'}) \in R^{'}$ and $σ^{d} < α$ . If d is the output of P run on the input $d^{'}$ , then $σ^{d} < α$ as above. Consequently, if y is the set coded by d, then $σ^{y} < α$ and $(x, y) \in R$ , so y is as desired. □

Another smooth generalization of a classically important observation to our setting is the following: Proposition 12 (For the classical version, cf. Brattka et al., [2], Section 13).

Let $R, R^{'} \subseteq V^{2}$ , $R ⩽_{soW} R^{'}$ , $X \subseteq V$ OTM-closed. Suppose that R is ‘slim on X’, i.e. for every $z \in R [X]$ , there is some $x \in X$ such that z is unique with $(x, z) \in R$ . Then $| R [X] | ⩽ | R^{'} [X] |$ .

Proof.
The proof of Proposition 13.1 in [2] carries over almost verbatim. □

4. An application: Choice principles

We will now apply the methods obtained above to a comparison between various set-theoretical choice principles with respect to ordinal (Weihrauch) reducibility. Unfortunately, if the $Π_{2}$ -statement ϕ is false in V, then every $Π_{2}$ -statement ψ reduces to ϕ: As there are no canonifications of ϕ, the statement that every such canonification can effectively be turned into one of ψ is vacuous.7

⁷
We thank our anonymous referee for pointing this out.

To avoid this, we will assume in this section that the set-theoretical universe possesses a definable well-ordering and thus satisfies global choice, i.e there is a class function

F : V \to V

such that, for all nonempty x, we have

F (x) \in x

Specifically, we will deal with the following statements, further variants of which will be introduced below; all of these statements are $Π_{2}$ and thus naturally associated with a “construction problem”.

“Every non-empty set contains an element” (PP, “picking principle”)

“Every non-empty finite set contains an element” ( ${PP}_{fin}$ )

“Every 2-element set contains an element” ( ${PP}_{2}$ )

“Every non-empty set has a non-empty finite subset” (MPP, “multiple picking principle”)

“For every family X of pairwise disjoint, non-empty sets, there is a set x that has finite non-empty intersection with any element of X” (MuC, principle of multiple choice)

“Every family of pairwise disjoint, non-empty sets has a system of representatives” (AC, axiom of choice)

“Every family of non-empty sets has a choice function” ( ${AC}^{'}$ )

“Every vector space has a basis” (VC)

“Every set can be well-ordered” (WO, well-ordering principle)

“Every partially ordered set has a maximal chain” (HMP, Hausdorff’s maximality principle)

“Every partially ordered set in which every chain has an upper bound contains a maximal element” (ZL, Zorn’s Lemma)

We begin with some obvious observations:

Proposition 13.

${PP}_{2} ⩽_{soW} {PP}_{fin} ⩽_{soW} PP \equiv_{soW} ZL ⩽_{soW} AC$ .

$MuC ⩽_{soW} AC \equiv_{soW} {AC}^{'}$ .

When ϕ is any of the above principles, then $ϕ ⩽_{soW} WO$ .

$MuC ⩽_{soW} VC$

Proof.

(i) The first three reducibilities work via $[P, P]$ , where P computes the identity function. For $PP ⩽_{soW} ZL$ , given a non-empty set x to pick from, pass over $(x, id)$ to ZL, i.e. the partial ordering on x where all elements are maximal; then any canonification of ZL will pick out an element of x. For the other direction, given a partially ordered set $(x, ⩽)$ satisfying the condition of ZL, ZL implies that it will contain some maximal element. Given $(x, ⩽)$ , it is easy to compute the set $M \subseteq x$ of maximal elements. Applying PP to M then yields a maximal element of x. For reducing PP (or ZL) to AC, hand over ${x}$ to a canonification of AC when an instance x of PP is given as the input.

(ii) $MuC ⩽_{soW} AC$ is trivial. $AC \equiv_{soW} {AC}^{'}$ works via the obvious OTM-effectivization of the equivalence proof over ZF, see e.g. Devlin [12], Section 2.7.

(iii) Again, the usual proofs of implication over ZF effectivize on OTMs. For the picking principles, one well-orders the set x and then picks the minimal element. For VC, given a well-ordered vector space V, it is easy to see that the subset of V consisting of those elements that are not linearly generated by those preceding it in the well-ordering forms a basis of V (see e.g. Shore, [26]) and thus OTM-computable from such a well-ordering.

(iv) This works by an easy effectivization of the proof in Blass [1]. □

Remark.

The reduction of ZL to PP is somewhat unsatisfying. We hence propose to consider HMP instead, which is the combinatorial “core” behind ZL.

When arbitrarily many instances of a problem can be used, the hierarchy collapses:

Proposition 14.

We have $PP \equiv_{OTM} WO$ . Thus, all of the above principles except ${PP}_{2}$ and ${PP}_{fin}$ are $⩽_{OTM}$ -equivalent to WO.

Proof.

Again, the usual proof effectivizes. Let P be an OTM-program that works as follows: Given a (code of a) set x, iteratively use PP to pick elements from the remaining set and exclude them from the set; eventually, every element of x has been picked, and the order in which they were picked is a well-ordering of x. □

Though PP may seem too obvious to be called a “principle”, note that this is not so in terms of effectivity: There is no general prescription for picking an element from an arbitrary set! Indeed, not even the simplest version is effective:8

⁸

Recall that we are working under set-theoretical extra assumptions that guarantee the existence of the required generic filters below (which in particular follow from, but are much weaker than, $0^{♯}$ ).

Proposition 15.

${PP}_{2}$ is not effective.

Proof.

Suppose otherwise, and let P be an OTM-program that computes a canonification F of ${PP}_{2}$ . By Jech [20], Section 5.4, there is a symmetric extension M of L in which ZF holds while ${AC}_{2}$ , the axiom of choice for countable sequences of pairs, fails. Let $s : = ({a_{i}, b_{i}} : i \in ω) \in M$ be such a sequence without a choice function in M. The model M is a symmetric submodel of a generic extension $L [G]$ of L, where G satisfies the countable chain condition; thus, the cardinals in $L [G]$ are the same as the cardinals in L. The $a_{i}$ and $b_{i}$ are sets of real numbers and thus contained in $L_{ω_{2}^{L}} [G]$ , so we have $tc (s) \in L_{ω_{3}^{L}} [G]$ . Thus, the forcing $P$ for adding a bijection between $tc (s)$ and ω is contained in $L_{ω_{4}^{L}} [G]$ and its power set $P (P)$ is contained in $L_{ω_{5}^{L}} [G]$ .

By our set-theoretical assumptions, $L_{ω_{5}^{L}} [G]$ , and hence

$P (P)$ , is countable; thus there are two mutually generic filters over M that make $tc (s)$ well-ordered. Then both generic extensions, say N and $N^{'}$ , will contain codes for each ${a_{i}, b_{i}}$ , so P can be applied to each such pair in both models, and thus, $F | s$ is definable over N and $N^{'}$ . Thus $F [s]$ will be a choice function for s contained both in N and $N^{'}$ by replacement, and so $F [s] \in N \cap N^{'} = M$ , a contradiction. □

A similar idea allows us to separate versions of the picking principle:

Theorem 16.

$PP ≰_{oW} {PP}_{fin}$ . Thus ${PP}_{fin} <_{oW} PP$ . In particular, ${PP}_{n} <_{oW} PP$ for all $n \in ω$ .

Proof.

We write ${AC}_{fin}$ for the axiom of choice for finite sets. Also, let us write ‘LO’ for the statement that every set can be linearly ordered. It is well-known that LO implies ${AC}_{fin}$ (given a set X of finite sets, pick a linear ordering $⩽^{o}$ of $⋃ X$ and then pick the minimal $⩽^{o}$ -minimal element of each element of X).

Now suppose otherwise, and let $[P, Q]$ witness the reduction of PP to ${PP}_{fin}$ . By Theorem 5.21 of [20], there is a transitive set model of ZF+LO (and thus of $ZF + {AC}_{fin}$ which contains a set without a choice function. Under the assumption that sufficiently large L-cardinals are countable (in particular, when one assumes $0^{♯}$ ), the same construction works over the ground model L (as the required filters exist) and yields a transitive class model M with the same properties. Moreover, M can be taken to be a submodel of a cardinal-preserving generic extension $L [G]$ . In fact, X can be taken to be $P^{M} (ω) ∖ {\emptyset}$ .

Let $X \in M$ be a set without a choice function in M. By the above, we can assume that $X \in L_{ω_{5}^{L}} [G]$ . For each code $c_{x}$ of an element $x \in X$ , let $\tilde{x}$ be the set coded by the output of the computation $Q (c_{x})$ .

By our set-theoretical extra assumptions, the forcing for making $tc (X)$ well-ordered is countable in V and thus has two mutually generic filters $G_{0}$ , $G_{1}$ over M. Thus, all elements of X have codes both in $M [G_{0}]$ and $M [G_{1}]$ , and therefore, the corresponding Q-computations exist in $M [G_{0}]$ and $M [G_{2}]$ . Thus, for each $x \in X$ , we have $\tilde{x} \in M [G_{0}] \cap M [G_{1}]$ and, by replacement in $M [G_{0}]$ and $M [G_{1}]$ , in fact $\tilde{X} : = {\tilde{x} : x \in X} \in M [G_{0}] \cap M [G_{1}] = M$ . Now, since a canonification of ${PP}_{fin}$ is applicable to $\tilde{x}$ for each $x \in X$ , $\tilde{X}$ is a set of finite sets. By ${AC}_{fin}$ in M, $\tilde{X}$ has a choice function $f \in M$ . By global choice, let $F \supseteq f$ be a canonification of ${PP}_{fin}$ that extends f. Thus, $F_{P} \circ F \circ F_{Q}$ is a canonification of PP.

Let $Y : = F [\tilde{X}] = f [\tilde{X}] \in M$ . By the same argument as above, the collection Z of sets coded by the outputs of P when applied to an element of Y is contained in two mutually generic extensions of M that make $tc (Y)$ well-ordered and thus we have $Z \in M$ .

But now, by the assumptions on P, Q and F, Z is a choice function for X contained in M, a contradiction. □

Remark.

The same approach works to turn many independence results over ZF between versions of AC into non-reducibility results between versions of PP. Thus, for example, the results given in Section 7.4 of Jech [20] imply in the same way that ${PP}_{2}$ and ${PP}_{3}$ are $⩽_{OTM}$ -incomparable, that $MPP <_{oW} PP$ etc. Moreover, it in fact suffices to construct such (transitive, class-sized) models of KP (and possibly less), which is enough to guarantee the existence of the relevant computations.

On the other hand, by an obvious OTM-effectivization of the proof of the implication ${AC}_{2} \to {AC}_{4}$ over ZF in [20], Example 7.12, we also get:

Proposition 17.

${PP}_{4} ⩽_{OTM} {PP}_{2}$

Question.

Is ${PP}_{4} ⩽_{oW} {PP}_{2}$ ? In general, let us write ${PP}_{k, n}$ for the problem of picking k elements from a set with n elements. Then how do the ${PP}_{k, n}$ relate with respect to $⩽_{oW}$ and $⩽_{soW}$ ?

Proposition 18.

$PP <_{oW} AC$ .

$PP <_{oW} HMP$

$MPP <_{oW} MuC$ .

Proof.

Clearly, PP reduces to AC, since, given a non-empty set x, an element of x is obtained by applying AC to ${x}$ . So $PP ⩽_{oW} AC$

We now want to show that the reduction is strict, i.e. that $AC ≰_{oW} PP$ . To this end, suppose that F is a canonification of PP. Now let M be a transitive proper class such that $M ⊧ ZF + \neg AC$ . Being transitive, M contains $F (x)$ for every non-empty $x \in M$ .

Now M is closed under F, which is a canonification of PP, but contains some x contradicting AC. By Lemma 9, $PP ≰_{oW} AC$ .

The arguments for (ii) and (iii) are completely analogous. □

On the other hand, given that PP is a provability-wise trivial principle, the following proposition about its computational power may come as a surprise. However, this becomes quite reasonable once one notices that a canonification of PP is in fact a global choice function.

Proposition 19.

Suppose that ϕ is a set-theoretical $Π_{2}$ -statement such that $ZF ⊢ ϕ$ . Then $ϕ ⩽_{oW} PP$ . In other words, PP is “ $Π_{2}$ -universal for ZF”.

Proof.

Let a be an arbitrary set and write ϕ in the form $\forall x \exists y ψ$ with ψ a $Δ_{0}$ -formula. Let us write $\bar{x} : = tc (a \cup {a})$ .

We show how to compute a (code for a) set Y such that $ψ (a, y)$ holds for all $y \in Y$ . This is achieved by the OTM-program P that, given a code for a, enumerates $L [tc (\bar{a})]$ until the first $L [\bar{a}]$ -level $L_{β} [\bar{a}]$ is found that contains some y such that $ψ (a, y)$ . Whether or not $ψ (a, y)$ holds is easily OTM-decidable, since ψ is $Δ_{0}$ .

Then the output is $Y : = {y \in L_{β} (\bar{a}) : ψ (a, y)}$ . As $L [\bar{a}]$ is a model of ZF, such a level must eventually be found, so the program always terminates with a non-empty output Y that has the desired properties.

Now applying PP to Y yields some b such that $ψ (a, b)$ . Thus, we have reduced ϕ to PP. □

We have an analogous statement to Proposition 19 for ZFC and WO in place of ZF and PP: Namely, WO is, with respect to set-theoretical $Π_{2}$ -statements provable in ZFC, maximal for oW-reducibility:

Theorem 20.

Let ϕ be a $Π_{2}$ -statement in the language of set theory such that $ZFC ⊢ ϕ$ . Then $ϕ ⩽_{oW} WO$ .

Proof.

Let $ϕ = \forall x \exists y ψ (x, y)$ , where ψ is $Δ_{0}$ . We describe two programs P and Q such that $[Q, P]$ witnesses the oW-reducibility of ϕ to WO. Let F be an arbitrary canonification of WO. P works as follows: Given a code c for a set x, compute a code $c^{'}$ for tc(x), the transitive closure of x. Then $F (c^{'})$ will be a code $c^{″}$ for a well-ordering of tc(x). Let ⪯ be that well-ordering. Now Q works as follows: Given $Y : = (tc (x), ⪯)$ , a well-ordered set, $L [Y]$ will be a model of ZFC, so $L [Y] ⊧ \exists z ψ (x, z)$ by assumption. Now Q enumerates $L [Y]$ until some $L_{α} [Y]$ is found that contains such a z and returns the $<_{L [Y]}$ -smallest such z.

Clearly then, $F_{Q} \circ F \circ F_{P}$ is a canonification of ϕ. □

Finally, we note two further separation results (under our set-theoretical extra assumptions granting the existence of the necessary generic filters):

Theorem 21 (Cf. [6], Thm. 10).

$AC <_{oW} WO$

Proof.
As we already know $AC ⩽_{soW} WO$ , it suffices to show that $WO ≰_{oW} AC$ . This is shown in [[6], Thm. 10]. The idea of the proof is that Zarach’s construction of a model of ${ZF}^{-} + AC + \neg WO$ in [27] can (under the set-theoretical assumptions necessary to guarantee the existence of the required generic filters, which follows, e.g., from $0^{♯}$ ) be carried out over L and yields a transitive class model M of the same theory and contains a counterexample to WO that can be well-ordered by forcing over M in two mutually generic ways, so that the assumptions of Lemma 9 are satisfied. □

The preceding result is plausible, as the proof of $AC \to WO$ over ZF applies AC to the power set of the set to be well-ordered, and power sets are not computable by Corollary 8. The following is thus to be expected. As usual, for $R, R^{'} \subseteq V^{2}$ , we write $R \circ R^{'}$ for ${(a, b) : \exists c ((a, c) \in R \land (c, b) \in R^{'})}$ ; moreover, we write “Pot” for the relation ${(x, P (x) ∖ {\emptyset}) : x \in V}$ . Finally, we recall that ${AC}^{'}$ is associated with the relation that holds between families of non-empty sets choice functions for these families.
Proposition 22.
$WO <_{oW} Pot \circ {AC}^{'}$ .
Proof.
$⩽_{oW}$ follows by the obvious effectivization of the proof of the implication ${AC}^{'} \to WO$ over ZF. Since a choice function on the power set of a set x has the same cardinality as that power set, strictness follows from Lemma 7. □

Note that we saw above that $WO \equiv_{OTM} PP$ . Thus, we have seen that ordinal Weihrauch reducibility is strictly stronger than OTM-reducibility.

Figure 1 summarizes the situation; $<_{oW}$ is indicated by arrows, $⩽_{oW}$ by dotted arrows and $\equiv_{OTM}$ by a dashed arrow. All indicated oW-reducibilities (whether strict or not) are strong.

Figure 1.
Reducibility relations between various choice principles.
Question.
We do not know the answers to the following questions:
Is $AC <_{oW} HMP$ (or even $AC ⩽_{oW} HMP$ )?

Is $HMP <_{oW} WO$ ?

Is $MuC <_{oW} AC$ ?

5. Effectivity and provability

A question that has recently received attention in the classical theory of Weihrauch reducibility is whether the reducibility of a statement ϕ to another statement ψ corresponds to the provability of the implication $ψ \to ϕ$ in some logical calculus; partial answers to this have been obtained in Kuyper [23]. We expect a similar analysis to work in the transfinite setting. As a first observation, we show below that reducibility of a set-theoretical $Π_{2}$ -sentence ψ to $ϕ \land PP$ for another such $Π_{2}$ -sentence ϕ in the sense of $⩽_{OTM}$ (where arbitrarily many applications of a canonification are allowed) is implied by the provability of $ϕ \to ψ$ in KP. (PP is necessary here to pick a particular witness after a non-empty set of witnesses has been determined at the end of the construction.) The result is certainly not optimal, so that one cannot expect the converse to hold; and in fact we have $WO ⩽_{OTM} PP$ , while the implication $PP \to WO$ is not even provable in ZF, let alone in KP.

Lemma 23.
Let $ϕ (x, y)$ be $Δ_{0}$ , and let a be a set. If there is b such that $ϕ (a, b)$ holds in V, then there is $b^{'}$ such that $ϕ (a, b^{'})$ holds in V and such that $| tc (b^{'}) |^{L [tc (a, b^{'})]} ⩽ | tc (a) | ℵ_{0}$ .
Proof.
Form the elementary hull of ${tc (a)}$ in level $L_{α} [tc (a, b^{'})]$ that contains b and use condensation. □
Definition 24.
Let ϕ be $Π_{2}$ . A canonification of ϕ is called ‘reasonable’ if and only if $| tc (F (a)) | ⩽ | tc (a) | ℵ_{0}$ for every set a.
Corollary 25.
Suppose that F is a canonification of the $Π_{2}$ -statement ϕ. Then a reasonable canonification G of ϕ is OTM-computable from F.
Proof.
Effectivize the proof of Lemma 23. That is, suppose a is given; to simplify the argumentation, we will assume that a is transitive, which we can assume without loss of generality by replacing a with $tc (a)$ if necessary. Use the miracle command to obtain $F (a)$ . Then $L [a, tc ({F (a)})]$ 9
⁹
We write $L [a, b]$ for $L [(a, b)]$ .

will contain some b with $ψ (a, b)$ (namely $F (a)$ ), and, by Lemma 22, it will contain such a b of the required cardinality. It thus suffices to enumerate $L [a, tc ({F (a)})]$ using the relativized version of $P_{L}$ and output the element that is minimal in the sense of the canonical well-ordering of $L [a, tc (F (a))]$ . □
Theorem 26.
Let $ϕ, ψ \in Π_{2}$ , and suppose that $KP ⊧ ϕ \to ψ$ . Then $ψ ⩽ ϕ \land PP$ .
Proof.
Let ϕ be $\forall x \exists y ϕ^{'} (x, y)$ and let ψ be $\forall x \exists y ψ^{'} (x, y)$ , where $ϕ^{'}$ and $ψ^{'}$ are $Δ_{0}$ . Moreover, let F be a canonification for ϕ and let a be an instance for ψ. By Corollary 25, we may assume without loss of generality that F is reasonable.

In order to compute, relative to F, a (code for a) set b such that $ψ^{'} (a, b)$ , we proceed as follows:

Given a, compute $(L_{α} [a] : α \in On)$ up to the first $α_{0}$ such that $L_{α_{0}} [a] ⊧ KP$ . Let $M_{0} : = L_{α_{0}} [a]$ .

In general, let $α_{ι + 1}$ be minimal such that $L_{α_{ι + 1}} [F [M_{α_{ι}}]] ⊧ KP$ and let $M_{ι + 1} : = L_{α_{ι + 1}} [F [M_{α_{ι}}]]$ . For δ a limit ordinal, let $M_{δ} : = ⋃_{ι < δ} M_{ι}$ . Claim.
There is a limit ordinal β such that $M_{β} ⊧ KP + ϕ$ .

To see this, first note that all $M_{β}$ are transitive and increasing unions of admissible sets. Clearly, $M_{δ} ⊧ ϕ$ whenever δ is a limit ordinal, as such sets are closed under F. Also, all axioms of KP expect $Δ_{1}$ -collection and -separation will clearly hold in such an $M_{δ}$ . It thus suffices to show that there is a limit ordinal δ such that $Δ_{1}$ -collection and $Δ_{1}$ -separation holds in $M_{δ}$ .

Let κ be the smallest regular uncountable cardinal $> | a |$ . We claim that $M_{κ}$ is as desired. Since F is reasonable, it follows inductively that $| u | < κ$ for all $u \in M_{κ}$ . To see that $Σ_{1}$ -collection holds in $M_{κ}$ , let $u, \vec{p} \in M_{κ}$ , and let H be a $Σ_{1}$ -function over $M_{κ}$ such that H is defined on u. We claim that there is $γ < κ$ such that H is defined on u in $M_{γ}$ (i.e. $M_{γ}$ contains the necessary witnesses); this suffices, as $M_{γ + 1} ⊧ KP$ will satisfy $Σ_{1}$ -collection and thus contain the desired superset of $H [u]$ , which will still work in $M_{κ}$ by upwards absoluteness of $Σ_{1}$ -formulas. Now, if this failed, then the set of ξ such that a new value of H for some element of u is defined in $M_{ξ}$ would be cofinal in κ and have cardinality $< | u |$ , which, by our initial observation, contradicts the regularity of κ. Thus $Σ_{1}$ -collection holds in $M_{κ}$ . The same argument shows that $M_{κ}$ satisfies $Σ_{1}$ -separation, and a fortiori $Δ_{1}$ -separation. This concludes the proof of the claim.

Now, to compute a b as desired, compute the sequence $(M_{ι} : ι \in On)$ until a limit ordinal γ is found for which $M_{γ}$ is admissible; that such a γ exists follows from the claim, and thus it will eventually be found. As $M_{γ} ⊧ KP + ϕ$ and $KP ⊧ ϕ \to ψ$ , we have $M_{γ} ⊧ ψ$ . As $a \in M_{γ}$ , there is $b \in M_{γ}$ such that $M_{γ} ⊧ ψ^{'} (a, b)$ , and thus, by absoluteness of $Δ_{0}$ , $ψ^{'} (a, b)$ will hold in V. But now, the set B of all such b from $M_{γ}$ can easily be determined by searching through $M_{γ}$ . By one application of PP to B, we finally obtain the required witness. □
Question.
Are there logical calculi C and axiomatic systems T such that reducibility of ψ to ϕ in the sense of $⩽_{OTM}$ corresponds precisely to the provability of the implication $ϕ \to ψ$ from T in C? What about $⩽_{oW}$ or $⩽_{soW}$ ? It seems particularly tempting to look for connections to constructive set theory here. Some first results in this direction can be found in [8], which is extended in [9].

We conclude by observing that the correspondence between provability and reducibility has its limits, at least as long as the underlying calculus is classical.

Let us say that an ∈-theory T effectivizes a binary relation $C$ if every model M of T has, for every $x \in M$ , some $y \in M$ such that $(x, y) \in C$ .
Proposition 27.
Let T be an OTM-computable ∈-theory with transitive models in L. Then there is an ∈-definable binary relation $C$ that is effective, but for which $\forall x \exists y (x, y) \in C$ is not provable in T.

Moreover, if the existence of transitive models of T is consistent with ZFC, then so is the existence of such a $C$ .
Proof.
Consider the relation that holds between each set x and each transitive model of T in L. Then $C$ has an effective canonification: The program P that enumerates L until the first transitive model of T is found and then outputs that model is of the desired kind. But T, being consistent, cannot prove that there are such models. □

Consequently, for classical logic, the answer to our above question is negative. Given that connections between reducibility and provability have been based on intuitionistic or linear logic in the classical case, this is hardly surprising.
6. Beyond $Π_{2}$

The setting introduced above is restricted to $Π_{2}$ -formulas. However, there are at least two ways to generalize canonifications, and thus reducibility notions, beyond this point, which we want to sketch briefly in this section. For technical convenience, let us assume from now on that all formulas are given in prenex normal form and let us consider the $Π_{n}$ -statement $ϕ \equiv \forall x_{1} \exists y_{1} \forall x_{2} \exists y_{2} ... \forall x_{n} \exists y n ψ (x_{1}, y_{1}, x_{2}, y_{2}, \dots, x_{n}, y_{n})$ , where ψ is $Δ_{0}$ . A straightforward generalization of the notion of a canonification given above Definition 2 would be to say that a canonification of ϕ is a function $F : V \to V$ such that, for all $a \in V$ , we have $\forall x_{2} \exists y_{2} ... \forall x_{n} \exists y_{n} ψ (a, F (a), x_{2}, y_{2}, \dots, x_{n}, y_{n})$ . Let us call this a “superficial” canonification, or s-canonification, of ϕ. A more radical approach would be to demand the canonification to “penetrate” the whole quantifier nesting; so we define a “thorough” canonification, or t-canonification, to be an n-tuple $(F_{1}, \dots, F_{n})$ of functions with $F_{i} : V^{i} \to V$ such that, for all $i \in {1, 2, \dots, n}$ and all $a_{1}, \dots, a_{i - 1} \in V$ , we have $\forall x_{i} \exists y_{i} ... \forall x_{n} \exists y_{n} ψ (a_{1}, F_{1} (a_{1}), a_{2}, F_{2} (a_{1}, a_{2}), \dots, a_{i - 1}, F_{i - 1} (a_{1}, \dots, a_{i - 1}), x_{i}, y_{i}, \dots, x_{n}, y_{n})$ .

In the spirit of Definitions 4 and 5 above, we can then introduce reducibility relations between $Π_{n}$ -statements for arbitrary n. For s-canonifications, the definitions carry over verbatim. For t-canonifications, let $ϕ \in Π_{m}$ , $ϕ^{'} \in Π_{n}$ .

We say that ϕ is ${OTM}^{t}$ -reducible to $ϕ^{'}$ and write $ϕ ⩽_{OTM}^{t} ϕ^{'}$ if and only if there is an OTM-program P using n “miracle” tapes $T_{1}, \dots, T_{n}$ and m output tapes $T_{1}^{'}, \dots, T_{m}^{'}$ , such that, whenever $(F_{1}, \dots, F_{n})$ is a canonification of $ϕ^{'}$ and carrying out the “miracle” command on $T_{i}$ replaces the i-tuple coded by the current content of $T_{i}$ by a code of its image under $F_{i}$ , then P computes the components of a canonification of ϕ on its output tapes.

We say that ϕ is ordinal ${Weihrauch}^{t}$ -reducible to $ϕ^{'}$ and write $ϕ ⩽_{oW}^{t} ϕ^{'}$ if and only if there are there are functional OTM-programs P and Q with $F_{Q} : V^{m} \to V^{n}$ and $F_{P} : V^{n + 1} \to V^{m}$ such that, for all $\vec{a} = (a_{1}, \dots, a_{m}) \in V$ and all canonication $(F_{1}, \dots, F_{n})$ of $ϕ^{'}$ , if $F_{Q} (a_{1}, \dots, a_{m}) = (b_{1}, \dots, b_{n})$ and $(c_{1}, \dots, c_{m}) = F_{P} (\vec{a}, F_{1} (b_{1}), F_{2} (b_{1}, b_{2}), \dots, F_{n} (b_{1}, \dots, b_{n}))$ , then the function tuple $(F_{1}, \dots, F_{m})$ such that $F_{i}$ maps $(a_{1}, \dots, a_{i})$ to $(c_{1}, \dots, c_{i})$ for $1 ⩽ i ⩽ m$ is a canonification of ϕ.

In order to be able to consider cases like the ZFC axioms, we can slightly further extend this to axiom schemes and say that ${ϕ_{i} : i \in ω}$ is ordinal Weihrauch reducible to ${ψ_{j} : j \in ω}$ if and only if we have a program P that, for any $i \in ω$ , computes a $j \in ω$ and further reduces $ϕ_{i}$ to $ψ_{j}$ .

By an easy adaptation of the proof, one obtains a variant of Lemma 7, which can be used to show that the power set axiom is not reducible to any other ZFC-axiom, while an obvious effectivization of the well-known proof of the implication shows that the separation scheme is reducible to the replacement scheme in this sense.

The ideas sketched in this section are closely related to the concept of realizability for OTMs, which are discussed in [7] and studied in detail in work with Galeotti and Passmann [9].

7. Conclusion and further work

We have introduced notions of effectivity, reducibility and ‘case-wise’ reducibility applicable to mathematical objects of arbitrary cardinality. The approach to effectivity is supported by the remarkable conceptual stability of ordinal computability (see e.g. [13] or [5]) and moreover, while not equivalent to e.g. the approach by Hodges, agrees with it concerning the results obtained so far. With regard to reducibility, we have seen how set-theoretical techniques can be used to distinguish between various versions of set-theoretical principles usually regarded as equivalent.

Clearly, there is a host of questions asking which statements are effectively reducible or (s)oW-reducible to which others. This may be viewed as a cardinality-independent version of reverse mathematics (as e.g. considered in [26]) and the theory of the Weihrauch lattice. In particular, we did not consider important choice principles like the Boolean Prime Ideal theorem, the principle that any set can be linearly ordered, Tukey’s lemma, Tychonov’s theorem etc. Apart from that, it may be interesting to consider variants of these notions with parameter-free computability replaced by other models of transfinite computation, like Infinite Time Turing Machines ([18]) or OTMs with ordinal parameters. Another worthwhile topic would be to replace (relativized) computability with (relativized) recognizability (see e.g. [10]).

Although Hodges did not introduce reducibility notions in his [19], the notion of effectivity proposed there, based on primitive-recursive set functions, can easily be supplemented with such concepts following the example of Definitions 4 and 5. A potential advantage is that primitive recursive set functions apply immediately to sets with no need for coding, and thus the technical issues that in our approach need to be dealt with using forcing no longer present themselves. Moreover, it will be interesting to see whether reducibility and nonreducibility results like those obtained in the present paper are ‘stable’ in the sense that they hold for various formalizations of reducibility in the transfinite.

Another topic from the classical setting that might lead to interesting results in the uncountable realm is that of ‘decomposability’ of statements or relations; like, e.g., in [2], we can say that the $Π_{2}$ -statement ϕ is ‘oW-decomposable’ if and only if there are $Π_{2}$ -statements $ψ, ψ^{'} <_{oW} ϕ$ such that ϕ is a $⩽_{oW}$ -least upper bound for ψ and $ψ^{'}$ in the $⩽_{oW}$ -ordering. As a special case, we say that a $Π_{2}$ -statement ϕ is ‘partitionable’ if and only if there are disjoint OTM-decidable classes $X, Y \subseteq V$ such that $X \cup Y = V$ and such that both $R_{0} : = {(x, y) : (x \in X \land (x, y) \in R_{ϕ}) \lor (x \notin X \land y = \emptyset)}$ and $R_{1} : = {(y, z) : (y \in Y \land (y, z) \in R_{ϕ}) \lor (y \notin Y \land z = \emptyset)}$ are strictly oW-reducible to $R_{ϕ}$ .

A crucial step in studying partitionability of statements would be the verification of the following conjecture, which is currently open:10

¹⁰

See, however, the discussion on MathOverflow at https://mathoverflow.net/questions/314053/delta1-2-and-degrees-of-constructibility-textbfon-sets.

Conjecture.

Let $F : V \to {0, 1}$ be OTM-computable. Then one of $F^{- 1} [0]$ and $F^{- 1} [1]$ contains sets of every degree of constructibility.

Relative to this conjecture, it is rather easy to obtain the following from the fact that the well-ordering principle holds in any $L [X]$ when X is a well-ordered transitive set:

Conjecture.

WO is not partitionable.

Finally, various notions from classical computability theory could be incorporated into our framework: For example, one should be able to make sense of the concept of a ‘random construction’ and ask whether there are interesting non-effective constructions that are reducible to them. We will also consider candidates for a sensible notion of a ‘jump operator’ for construction problems, a notion that led to a number of fascinating results about Weihrauch reducibility ([2]).

Footnotes

Acknowledgements

First of all, we want to express our gratitude to the organizers of the Dagstuhl workshop “Measuring the Complexity of Computational Content: From Combinatorial Problems to Analysis” for providing an inspiring incentive to continue our work on this topic and writing this paper.

We thank the anonymous referees of our CiE 2016 paper [] on which this paper is based for their help in improving the presentation. Moreover, we thank the anonymous referee of the current paper and A. Pauly for several valuable corrections, comments and suggestions.

Finally, we thank De Gruyter for the permission to use some of the material appearing in chapter 8 of the forthcoming [] in this article.

References

Blass, Existence of bases implies the axiom of choice, in: Axiomatic Set Theory,

S.S.J.E.

Baumgartner and

D.A.

Martin, eds, American Mathematical Society, 1984, pp. 31–33. doi:10.1090/conm/031/763890.

Brattka,

Gherardi and

Marcone, The Bolzano–Weierstraß theorem is the Jump of weak König’s lemma, Annals of Pure and Applied Logic 163 (2012), 623–655. doi:10.1016/j.apal.2011.10.006.

Brattka,

Gherardi and

Pauly, Weihrauch Complexity in Computable Analysis (2017).

Brattka,

Roux and

Pauly, Connected choice and the Brouwer fixed point theorem, Journal of Mathematical Logic 19 (2012).

Carl, Towards a Church-Turing-Thesis for Infinitary Computations, 2013.

Carl, Generalized effective reducibility, in: LNCS, Vol. 9709, 2016, pp. 225–233. ISBN 978-3-319-40188-1.

Carl, Ordinal Computability: An Introduction to Infinitary Machines, 2019. ISBN 9783110496154.

Carl, A Note on OTM-Realizability and Constructive Set Theories, 2019.

Carl,

Galeotti and

Passmann, Realisability for Infinitary Intuitionistic Set Theory, 2020.

10.

Carl,

Schlicht and

Welch, Recognizable sets and Woodin cardinals: Computation beyond the constructible universe, Annals of Pure and Applied Logic 169 (2015).

11.

Dawson, Ordinal Time Turing Computation, PhD thesis, University of Bristol, 2009.

12.

Devlin, Fundamentals of Contemporary Set Theory, 1st edn, Springer, New York, 1994.

13.

Fischbach, The Church-Turing-Thesis for Ordinal Computable Functions, Master’s thesis, Rheinische Friedrich-Wilhelms Universität Bonn, Bonn, 2010.

14.

Friedman, Fine Structure and Class Forcing, 2000. ISBN 9783110809114.

15.

Galeotti and

Nobrega, in: Towards Computable Analysis on the Generalised Real Line, LNCS, 2017, pp. 246–257.

16.

Goodstein, Recursive Analysis, 2010. ISBN 9780720422122.

17.

Greenberg,

Hamkins,

Hirschfeldt and

Miller, Effective Mathematics of the Uncountable, 2013, ISBN 9781107014510.

18.

Hamkins and

Lewis, Infinite time Turing machines, Journal of Symbolic Logic 65 (1998).

19.

Hodges, On the effectivity of some field constructions, in: Proceedings of the London Mathematical Society – Proc London Math Soc, Vol. 32, 1976, pp. 133–162. doi:10.1112/plms/s3-32.1.133.

20.

Jech, The Axiom of Choice, 1973. ISBN 9780720422757.

21.

Jensen and

Karp, Primitive recursive set functions, in: Proc. of Symposia in Pure Mathematics, Vol. 13, 1971. ISBN 9780821802458. doi:10.1090/pspum/013.1/0281602.

22.

Koepke, Turing computations on ordinals, Bulletin of Symbolic Logic 11 (2005). doi:10.2178/bsl/1122038993.

23.

Kuyper, On Weihrauch reducibility and intuitionistic reverse mathematics, The Journal of Symbolic Logic 82 (2015). doi:10.1017/jsl.2016.61.

24.

Mathias, Provident sets and rudimentary set forcing, Fundamenta Mathematicae 230 (2015), 99–148. doi:10.4064/fm230-2-1.

25.

Schlicht and

Seyfferth, Tree representations via ordinal machines, Computability 1 (2012). doi:10.3233/COM-2012-002.

26.

Shore, Reverse Mathematics, Countable and Uncountable: A Computational Approach, 2020.

27.

Zarach, Unions of ZF–Models which are themselves ZF–Models, in: Studies in Logic and the Foundations of Mathematics, Vol. 108, 1982. ISBN 9780444864659. doi:10.1016/S0049-237X(09)70519-1.

Effectivity and reducibility with ordinal Turing machines

Abstract

Keywords

1. Introduction

2. Setting the stage

2.1. Ordinal Turing machines

2 Though not formally equivalent, the two approaches agree with respect to the problems considered by Hodges.

Lemma 7 (Cf. [19], Lemma 3.2).

Proof. See [6], Lemma 1. The main ingredient is the well-known observation that OTM-computations cannot output sets of larger cardinalities than their input when the latter is infinite. □ We note some sample applications: Corollary 8 (Cf. [6], Lemma 2).

5 This requires relativizing the above to L.

Proposition 10 (For the classical version, cf. Brattka et al., [2], Proposition 12.1).

Proof. The proof of Proposition 13.1 in [2] carries over almost verbatim. □ 4. An application: Choice principles

7 We thank our anonymous referee for pointing this out.

7. Conclusion and further work

Footnotes

Acknowledgements

References

²
Though not formally equivalent, the two approaches agree with respect to the problems considered by Hodges.

Proof.
See [6], Lemma 1. The main ingredient is the well-known observation that OTM-computations cannot output sets of larger cardinalities than their input when the latter is infinite. □

We note some sample applications:
Corollary 8 (Cf. [6], Lemma 2).

⁵
This requires relativizing the above to L.

Proof.
The proof of Proposition 13.1 in [2] carries over almost verbatim. □

4. An application: Choice principles

⁷
We thank our anonymous referee for pointing this out.