Reverse mathematics, countable and uncountable: a computational approach

Richard A. Shore^{∗} Department of Mathematics Cornell University Ithaca NY 14853

December 20, 2010

Abstract

Reverse mathematics analyzes the complexity of mathematical statements in terms of the strength of axiomatic systems needed to prove them. Its setting is countable mathematics and subsystems of second order arithmetic. We present a similar analysis based on (recursion theoretic) computational complexity instead. In the countable case, this view is implicit in many of results in the area. By making it explicit and precise, we provide an alternate approach to this type of analysis for countable mathematics. It may be more intelligible to some mathematicians in that it replaces logic and proof systems with relative computability. In the uncountable case, second order arithmetic and its proof theory is insufficient for the desired analysis. Our computational approach, however, supplies a ready made paradigm for similar analyses. It can be implemented with any appropriate notion of computation on uncountable sets.

1 Introduction

The enterprise of calibrating the strength of theorems of classical mathematics in terms of the (set existence) axioms needed to prove them, was begun by Harvey Friedman in the 1970’s (as in [6] and [7]). It is now called Reverse Mathematics as, to prove that some set of axioms is actually necessary to establish a given theorem, one reverses the standard paradigm by proving that the axioms follow from the theorem (in some weak base theory). The original motivations for the subject were foundational and philosophical. It has become a remarkably fruitful and successful endeavor supplying a framework for both the philosophical questions about existence assumptions and foundational or mathematical ones about construction techniques needed to actually produce the objects that the theorems assert exist. The basic text here is [20] to which we refer the reader for background and all unexplained notions.

∗Partially supported by NSF Grants DMS-0554855, DMS-0852811 and John Templeton Foundation Grant 13408.

The proof theoretical setting for this subject has been second order arithmetic. All systems incorporate some fixed list of elementary axioms for first order arithmetic. (These are the axioms for ordered semirings.) They also have a simple induction axiom: (0 ∈ X & ∀n(n ∈ X → n + 1 ∈ X) → ∀n(n ∈ X)). The systems considered are then defined by their comprehension axioms starting with RCA_{0} which adds comprehension for Δ_{1}^{0} formulas (and induction for Σ_{1}^{0} formulas) to the basic axioms. They then progress through more complicated existence assumptions. In principle, one can go on through, for example, both arithmetic formulas and then comprehension for Π_{n}^{1} formulas for each n. In practice, there are almost no results that extend beyond Π_{1}^{1} comprehension. (See [15] for an example at the level of Π_{2}^{1} and [16] for ones for Π_{n}^{1} for all n ≥ 3.)

In this setting, the mathematics that can naturally be analyzed is that of countable structures both combinatorial and algebraic. Topological and analytic structures can be considered if they have some sort of countable basis, e.g. the reals or any separable metric space, and one can code objects of interest such as continuous functions or Borel sets as countable sets. Such codings can at times seem awkward or unnatural (at least to nonlogicians or even novices in the field). Moreover, the whole approach is tied to second order arithmetic and so cannot in any reasonable way talk about combinatorics, algebra, topology or analysis on structures of arbitrary cardinality.

We present an alternative approach based on classical computability that is implicit in many of the results in the area in the countable case and widely taken for granted. From the viewpoint of traditional logic (model theory or proof theory), it can be seen as restricting attention to the standard models. (A model of second order arithmetic consists of a model M = (M, +, ×, <, 0, 1) of our basic version of first order arithmetic and a collection S of subsets of M that serves as the domain of quantification for the second order variables in our language. We say that (M, S) is standard if M = ℕ.) In the countable case, it has the expository advantage of requiring no logical/syntactic or proof theoretic machinery while still providing a classification of the theorems of mathematics in terms of computational complexity that is quite close to the proof theoretic ones traditionally used.

Moreover, in most cases our approach serves to answer the classification questions for results and techniques raised in discussion of classical mathematics. To give an example from combinatorics, we point to the analyses of various theorems of matching theory from Hall’s to the König Duality theorem (KDT) in [9] and [2]. These basically computational analyses provide an answer to the question raised in [12] (pp. 6, 8) where it is noted that many related theorems of matching theory from Frobenius to König seem to be in some sense equivalent (each is a “special case” of the next in a circular fashion) but nonetheless one thinks that KDT is “the deeper result”. The analyses cited in the countable case show that the other “equivalent” results are computationally (and reverse mathematically) equivalent to compactness of Cantor space (WKL_{0}) or closure under jump (ACA_{0}) while KDT is equivalent (by [19] as well) to closure under “hyperarithmetic in” or ATR_{0}. Thus KDT is demonstrably the most complicated of this array of theorems.

Similarly, the combinatorist sees that the proofs of KDT, even in the countable case, do not follow the usual pattern of being deduced from the finite case by some form of compactness (and so WKL or full König’s Lemma (KL) which is equivalent to ACA_{0}). The proofs use transfinite recursion and instances of the axiom of choice. Indeed, these concerns on the part of Aharoni (who proved KDT for graphs of arbitrary cardinality [1]) lead to the analysis in [2] which showed that, in the countable case, compactness (in the form of WKL or KL do not suffice and transfinite recursion in the form of hyperarithmetic procedures or ATR_{0} are actually necessary. In the uncountable case our approach provides a method of tackling the mathematical, foundational and philosophical questions of how to calibrate the strength of the theorems and constructions of mathematics posed by the original subject. In particular, issues about the construction techniques needed to prove theorems such as KDT for uncountable graphs can be addressed.

2 Computable entailment and equivalence

The theorems analyzed in reverse mathematics are typically Π_{2}^{1} assertions, for every structure of some sort there is a function or relation with some desired property. In this setting, it is easy to think about the analysis as one that calibrates the complexity of constructing the desired function or relation given the initial structure. But, of course, more complicated statements are also analyzed.

As is well known, the standard systems of reverse mathematics, RCA_{0}, WKL_{0}, ACA_{0}, ATR_{0} and Π_{1}^{1}-CA_{0}, each correspond to some construction or recursion theoretic principle. The first is effective mathematics, i.e. closure under relative computability so that (in the Π_{2}^{1} case) the desired function or relation is computable in the given structure. The others correspond to “every infinite binary tree has an infinite path” (or the low basis theorem [10] that every such recursive tree has an infinite path P such that P′ ≡_{T} 0′); König’s Lemma (KL) every finitely branching infinite tree has an infinite path or closure under the Turing jump; definition by transfinite recursion or closure under “hyperarithmetic in”; and a version of a comprehension/choice principle that chooses the well orderings from a set of linear orderings or closure under the hyperjump. This correspondence is precise on the standard models, i.e. a standard model (ℕ, S) is a model of RCA_{0} if and only if S is closed under Turing reducibility and join. Given that it is a model of RCA_{0}, it is also a model of WKL_{0}, ACA_{0}, ATR_{0} or Π_{1}^{1}-CA_{0} if and only if every infinite binary tree coded in S has a path in S or S closed under Turing jump, “hyperarithmetic in” or the hyperjump, respectively.

Quite often analyses in reverse mathematics actually proceed by recursion (computability) theoretic methods. In the positive direction for a Π_{2}^{1} assertion, one shows that the desired function or relation is computable in the given structure or computable from some type of jump operator (Turing, or iterations into the transfinite all the way to the hyperjump) applied to it. Such proofs generally provide ones in the analogous axiom system of Reverse Mathematics (at times with more induction needed than the usual minimum of Σ_{1}^{0}). In the other direction, one often demonstrates that one principle or Π_{2}^{1} mathematical assertion Φ does not follow from another Ψ (including, for example, one of the basic systems beyond RCA_{0}) by providing an ideal in the Turing degrees (i.e. a collection of sets closed under Turing reducibility and join and perhaps the jump operator relevant to the discussion) such that Ψ holds in (the standard model of second order arithmetic corresponding to the sets in) the ideal but Φ does not. This, of course, proves that Ψ does not imply Φ over RCA_{0} (or over the system (ACA_{0}; ATR_{0} or Π_{1}^{1}-CA_{0}) corresponding to the jump closure condition). It actually provides a stronger independence results that, for example, applies to the base systems with full induction and more.

We propose a direct formulation of this complexity measure based on the difficulty of computing the desired output (function or relation) from the input (structure) as in the typical case of Π_{2}^{1} theorems. Making this view explicit formalizes the intuition that “being harder to prove” means “harder to compute”. It also provides a different expository route into the subject suitable for a mathematical or computer science audience that intuitively understands computability but may find formal proof systems foreign or less appealing. More interestingly, for the practitioners already familiar with this approach, it provides an opportunity to deal with uncountable structures and higher order statements that are out of the reach of standard proof theoretic methods. The route here is to use one (or more) of the studied definitions of computability on uncountable structures.

Definition 2.1. If C is a closed class of sets, i.e. closed under Turing reducibility and join, we say that C computably satisfies Ψ (a sentence of second order arithmetic) if Ψ is true in the standard model of arithmetic whose second order part consists of the sets in C. We say that Ψ computably entails Φ, Ψ ⊨_{c} Φ, If every closed C satisfying Ψ also satisfies Φ. We say that Ψ and Φ are computably equivalent, Ψ ≡_{c} Φ, if each computably entails the other.

One can now express the equivalence of some Ψ with, e.g. ACA_{0}, ATR_{0} or Π_{1}^{1}-CA in this way. One can also describe entailment or equivalence over one of these systems by either adding them on to the sentences Ψ and Φ or by requiring that the classes C be closed under the appropriate operators and reductions (Turing jump, hyperarithmetic in and hyperjump, respectively). More interestingly, one can directly express the relationships between two mathematical statements without going through any formal proof systems.

Turning now to uncountable structures, one can simply interpret computability as some version of generalized computability and then immediately have notions appropriate to uncountable settings. For example, if one is interested in algebraic or combinatorial structures where the usual mathematical setting assumes that an uncountable structure is given with its cardinality, i.e. the underlying set for the structure (vector space, field, graph, etc.) may as well be taken to be a cardinal κ, then a plausible notion of computation is given by α-recursion theory. This seems particularly appropriate when one is willing to also assume that V = L to avoid many purely set theoretic issues that do not usually affect theorems of classical mathematics. (To be fair, one must also then restrain oneself from using noncomputable combinatorial principles special to L, at least without first providing some appropriate complexity analysis for these principles.) In this setting, one carries out basic computations (including an infinitary sup operation) for α (or in our situation κ) many steps assuming some closure properties such as admissibility on α. (Note that every infinite cardinal is admissible.)

For settings such as analysis where the basic underlying set is the reals ℝ or the complex numbers ℂ, it seems less natural to assume that one has a well-ordering of the structure and one wants a different model of computation. Natural possibilities include Kleene recursion in higher types, E-recursion (of Normann and Moschovakis) and Blum-Shub-Smale computability. (See for example [17] or [4] for α-recursion theory; [17], [14] or [5] for the various versions of recursion in higher types or E-recursion and [3] for the Blum-Shub-Smale model.)

The general program that we are suggesting consists of the following:

Problem 2.2. Develop a computability theoretic type of reverse mathematical analyses of mathematical theorems on uncountable structures using whichever generalized notion of computability seems appropriate to the subject being analyzed.

Note that the formulation of the basic yardsticks for this analysis will not, in general be the same as for the countable case. An obvious example is Weak König’s Lemma. For uncountable cardinals κ, the assertion that every binary tree of height κ (or even just quite simple ones) has a size κ branch is equivalent to κ being weakly compact. Thus such a principle is not even a candidate yardstick for most cardinals. On the other hand, there are natural candidates for analogs of ACA_{0} once one has the right notion for the jump operator or enough closure to make sense of closing under first order definability (as over L_{κ}). We now consider a few standard examples from reverse mathematics in the setting of α-recursion theory for arbitrary cardinals κ inside L.

3 WKL and ACA in α-recursion theory

For our α-recursion theoretic analysis of the computational strength of mathematical theorems and constructions for uncountable structures, we assume that V = L and that ours structures are ones on some uncountable cardinal κ. Thus our models are of the form (L_{κ}, S, ∈ ) where S is a collection of subsets of L_{κ} (or equivalently of κ). We take our notion of relative computability to be “α-recursive in”, i.e. in our definition of κcomputable entailment and equivalence, we assume that our classes S of subsets of L_{κ} are κ-closed, i.e. closed under an effective join on pairs of sets and, if A ∈ S and B ≤_{κ} A then B ∈ S.

Note that an essential feature of ≤_{κ} is that both input and output information consists of κ-finite sets (i.e. ones in L_{κ}). More precisely, B ≤_{κ} A if there is a κ-r.e. (i.e. Σ_{1} over L_{κ}) set W_{γ} such that for all κ-finite sets M and N, M ⊆ B ⇔ ∃K, L(⟨M, 1, K, L⟩ ∈ W_{γ} & K ⊆ A & L ⊆ Ā) and N ⊆ B̄ ⇔ ∃K, L(⟨N, 0, K, L⟩ ∈ W_{γ} & K ⊆ A & L ⊆ Ā) where K and L also range over κ-finite sets. This notion stands in contrast to weak κrecursiveness, B ≤_{wκ} A, in which correct decisions are only required for questions about individual membership in B. Our assumption that V = L eliminates worries about nonregularity, i.e. if A ⊆ κ and γ < κ then A ↾ γ is κ-finite and so all initial segments of our oracles are available as information for our calculations. On the other hand, it does not eliminate the distinction between weak and ordinary κ-recursiveness when κ is a singular cardinal. In this case, the weak notion is not, in general, transitive. This distinction is a common source of difficulties in α-recursion theory. In our considerations, it first comes to light when we consider the relationship between closure under the jump operator and Σ_{1} (or, equivalently, first order) definability. (We refer to [17] or [4] for basic definitions and information about α-recursion theory.) Without going into the competing considerations for defining the jump (see [18] and [17] VII.4.8) we adopt the definition of the κ-jump in [18] and [17] as a universal κ-r.e. set in the following form: A′ = {⟨γ, δ⟩ |(∃K, L, i ∈ {0, 1})(⟨{δ}, i, K, L⟩ ∈ W_{γ} & K ⊆ A & L ⊆ Ā)}. Of course, A′ is Σ_{1} in A (over L_{κ}) and so closure under “Σ_{1} in” implies closure under the jump. In the other direction, however, while it is easy to see that if B is Σ_{1} in A (over L_{κ}) then B ≤_{wκ} A′ (by regularity) in general it need not be the case that B ≤_{κ} A′. Nonetheless, as in the countable case, closure under jump does imply closure under first order definability over L_{κ} by the following Lemma.

Lemma 3.1. If X ≤_{wκ} Y then X ≤_{κ} Y′.

Proof. As X ≤_{wκ} Y we have a γ such that, for every δ, δ ∈ X ⇔ ∃K, L(⟨{δ}, 1, K, L⟩ ∈ W_{γ} & K ⊆ Y & L ⊆ Ȳ) and δ ∉ X ⇔ ∃K, L(⟨{δ}, 0, K, L⟩ ∈ W_{γ} & K ⊆ Y & L ⊆ Ȳ). So for κ-finite M and N we have M ⊆ X ⇔ ¬[∃δ ∈ M∃K, L(⟨{δ}, 0, K, L⟩ ∈ W_{γ} & K ⊆ Y & L ⊆ Ȳ)] ⇔ h(M) ∉ Y′ for some κ-recursive function h and N ⊆ X̄ ⇔ ¬[∃δ ∈ N∃K, L(⟨{δ}, 1, K, L⟩ ∈ W_{γ} & K ⊆ Y & L ⊆ Ȳ)] ⇔ g(M) ∉ Y′) for some κ-recursive function g. Thus X ≤_{κ} Y′ as required.

Corollary 3.2. A κ-closed set S is closed under κ-jump if and only if it is closed under “Σ_{1} in” if and only if it is closed under first order definability over L_{κ}.

Next we turn to a classic example from both effective and reverse mathematics of a standard theorem equivalent to closure under the jump or first order definability: the existence of bases for vector spaces. As is often the case, choosing the correct classical construction to generalize is crucial. We adapt an argument from [13].

Theorem 3.3. The existence of bases for all vector spaces of size κ over fields of size κ is κ-computably equivalent to closure under κ-jump or under first order comprehension (over L_{κ}).

Proof. For the classical direction, assume we are given a vector space V = {v_{γ}|γ < κ} over a field K = {a_{γ}|γ < κ} with the usual operations of addition and scalar multiplication. It suffices to define a basis for V that is Π_{1} in the given structure. Let D = {v_{γ}|∃n ∈ ω∃ ⟨γ_{i}|i ≤ n⟩ ∃ ⟨δ_{i}|i ≤ n⟩ [(∀i ≤ n(δ_{i} < γ) & v_{γ} = ∑_{i≤n} α_{γ_{i}}v_{δ_{i}}]}. D is clearly Σ_{1} over L_{κ} in the vector space structure V. We claim that B = V − D is a basis for V. B is an independent set by definition (and the exchange principle for vector spaces). On the other hand, it follows by induction on γ < κ that each v_{γ} is either itself a member of B or a linear combination of finitely many v_{δ} for δ < γ and so (by induction) of v_{β} ∈ B with β < γ.

For the reversal, we consider any κ-closed class S of subsets of κ such that any vector space coded by a set in S has a basis in S. We have to prove that if X ∈ S then X′ ∈ S. We begin with the field K generated by κ many variables over the rationals and the vector space V generated over K by independent elements z_{γ} for γ < κ. Thus V is the set of finite linear combinations of z_{γ} with coefficients in K. We list V as v_{δ} so that the set of z_{γ} appearing in the linear combination that is v_{δ} is contained in {z_{γ}|γ ≤ δ}. In particular, we take z_{0} = v_{0}. We write (v)_{β} for the coefficient of z_{β} in v ∈ V.

We now define a κ-recursive sequence λ_{β} of elements of K by recursion. At stage β we check for each γ, δ < β if we can find a k and a finite sequence k_{j} from K and one γ_{j} and γ from β such that v_{δ} = ∑ k_{j}(z_{0} + λ_{β_{j}}z_{γ_{j}}) + k(z_{0} + λz_{γ}) for some λ ∈ K with γ ≠ γ_{i} ≠ γ_{j} ≠ 0 for each i ≠ j. Note that by our numbering scheme the only possible γ, γ_{j} are less than δ and so, by the independence of the z_{γ}, this is a κ-recursive check. In fact, we claim that for each possible δ, γ, ⟨γ_{j}⟩ there can be at most one choice of k, k_{j}, λ:

First, if v_{δ} = ∑ k_{j}(z_{0} + λ_{β_{j}}z_{γ_{j}}) + k(z_{0} + λz_{γ}) then k_{j}λ_{β_{j}} = (v_{δ})_{γ_{j}} and so k_{j} is uniquely determined. Next, k + ∑ k_{j} = (v_{δ})_{0} and so k is also uniquely determined. Finally, kλ = (v_{δ})_{γ} and so λ is uniquely determined as well.

Thus there are fewer than κ many possible values of such λ over all γ, δ < β and so we may κ-recursively choose λ_{β} > β to be different from all of them.

We now consider any set W_{e}^{X} which is κ-r.e. in X and so W_{e}^{X} = {γ|∃K, L(⟨{γ}, 1, K, L⟩ ∈ W_{e} & K ⊆ X & L ⊆ X̄)}. We consider a subspace V̂ of V generated by the set B̂ of elements z_{0} + λ_{β}z_{γ} where γ is enumerated in W_{e}^{X} at stage β, γ ∈ W_{e,at β}^{X}, i.e. ∃K, L ∈ L_{β}(⟨γ}, 1, K, L⟩ ∈ W_{γ} via a witness in L_{β} with K ⊆ X & L ⊆ X̄ but there are no such K, L and witness in L_{δ} for δ < β (and so, in particular, γ < β).

Claim: B̂, V̂ ≤_{κ} X.

Proof of Claim: As for B̂, it is clear that checking membership for any element of the form z_{0} +λ_{β}z_{γ} only requires information about L_{β} and X ↾ β (a κ-finite set by regularity) and the κ-recursive sequence λ_{β} and so B̂ ≤_{κ} X.

As for V̂, we claim that v_{δ} ∈ V̂ ⇔ v_{δ} is in the span of B̂ ↾ δ + 1 as by the definition of the sequence λ_{β}, it can never be put in by later elements. Thus given the κ-finite information B̂ ↾ μ + 1 about B̂ we can check κ-recursively for all δ ≤ μ if v_{δ} = k_{0}z_{0} + ∑ k_{j}z_{γ_{j}} is in the span of B̂ ↾ μ+1 by verifying that the z_{γ_{j}} are among those appearing in B̂ ↾ μ + 1 and, if so, that assuming they appear there as z_{0} + λ_{β_{j}}z_{γ_{j}} that the coefficients are as required, i.e. there are k̂_{j} such that k̂_{j}λ_{β_{j}} = k_{j} and k_{0} = ∑ k̂_{j}. Thus V̂ ≤_{κ} X as required. □

We now define the quotient vector space V/V̂ as the set of least elements of the appropriate equivalence classes: v_{δ} ∈ V/V̂ ⇔ ∀μ < δ[(v_{μ} − v_{δ}) ∉ V̂] so, in particular, z_{0} ∈ V/V̂. We define the natural operations on V/V̂ as those inherited from V by taking the least element of the appropriate equivalence class. So, for example, if v_{γ}, v_{δ} ∈ V/V̂ then v_{γ} + v_{δ} is v_{μ} where μ is least such that (v_{μ} − (v_{δ} + v_{γ})) ∈ V̂. Thus V/V̂ ≤_{κ} X and so is coded in S. Our closure assumption now gives us a basis B ∈ S for V/V̂. Without loss of generality, we may assume that z_{0} ∈ B (otherwise, put z_{0} in and perform the standard exchange procedure replacing one of the elements needed to generate it).

We next claim that W_{e}^{X} ≤_{wκ} B = {b_{μ}|μ < κ}: To see if γ ∈ W_{e}^{X} find λ_{i} and μ_{i} for i ≤ n such that ∑ λ_{i}b_{μ_{i}} ≡V̂ z_{γ}, i.e. the least elements from which they differ by something in V̂ are the same. (There must be such as the b_{μ} form a basis for V/V̂.) Now if n = 1 and b_{μ_{0}} = z_{0} there is a λ such that z_{0} + λz_{γ} ∈ V̂ and so γ ∈ W_{e}^{X}. On the other hand, if z_{γ} ≢V̂ z_{0}, γ ∉ W_{e}^{X} for if it were then there would be a β such that z_{0} +λ_{β}z_{γ} ∈ V̂.

Now what we really want is that W_{e}^{X} ≤_{κ} B as then the proper choice of e would have X′ ≤_{κ} B as desired. However, we do not in general know where in B we may need to look to find the components of a representative for every v_{δ} in some κ-finite M. They could be unbounded if κ is singular. However, the proof of Lemma 3.1 shows that there are κ-recursive functions h and g such that for κ-finite M and N, M ⊆ W_{e}^{X} ⇔ h(M) ∉ B′ and N ⊆ \overline{W_{e}^{X}} ⇔ g(N) ∉ B′. If we now repeat our entire argument with B in place of X and B′ in place of W_{e}^{X} we produce a new vector space such that for any basis C, B′ ≤_{wκ} C. Combining these reductions, we see that W_{e}^{X} ≤_{κ} C for any such basis and so, as X′ is κ-r.e. in X and S has the assumed closure properties, X′ ∈ S as required.

We now turn to determining the appropriate analog for WKL in this setting. As explained at the end of §2, assuming that every binary branching tree of height κ has a branch of length κ is much too strong. The appropriate tree formulation seems to be the following:

Definition 3.4. A binary tree T on a cardinal κ (i.e. a subset of 2^{<κ} closed downward under initial segments) is of finite character if T is continuous at limit levels, i.e. for any γ ∈ 2^{<κ} of length a limit ordinal λ, if γ ↾ δ ∈ T for every δ < λ then γ ∈ T and for every σ ∈ T, if there is a γ > |σ| such that σ has no successors on T at level γ then there is a τ ⊆ σ of length a successor ordinal and a γ̂ such that τ has no successors on T of length γ̂.

Definition 3.5. The finite character tree property for a cardinal κ, FCTP_{κ}, says that every binary tree T on κ of finite character has a path of length κ.

We now prove the κ-computable equivalence of FCTP_{κ} with a couple of theorems from logic that, in the countable case, are equivalent to WKL_{0}.

Theorem 3.6. The following are computably equivalent in the sense of κ-recursion theory for each cardinal κ:

1. FCTP_{κ}.

2. The compactness theorem for first order logic for languages (even propositional ones) and theories of size κ.

3. Σ_{1}-Separation: for every X and pair of disjoint Σ_{1}^{X} over L_{κ} sets A and B there is a separating set C, i.e. A ⊆ C and B ∩ C = ∅.

Proof. We prove enough computable entailments among the three conditions to guarantee computable equivalence.

(1) ⊨_{c} (2): Given a theory T of size κ in a language L of size κ we add Henkin constants c_{φ} to the language and κ-recursively build a Henkin tree H of sets of sentences T_{σ} consistent with T for σ ∈ H ⊆ 2^{<κ} as usual. At a level corresponding to a sentence φ we split and add on either φ or ¬φ. If φ = ∃xψ(x) then when we add on φ we also add on ψ(c_{φ}). At limit levels we take unions. We also check at each node if T_{σ} is inconsistent with T via a proof using axioms from T_{σ} and T ∩ L_{|σ|}. If so we stop the construction of the tree above σ.

We claim that the tree so constructed is of finite character. Continuity at limit levels is immediate by construction and the finitary nature of proofs. If σ ∈ H with |σ| = λ a limit ordinal has no successors at level γ > |σ| then we claim that T_{σ} ∪ (T ∩ L_{γ}) is inconsistent. If not, then the classical construction of the Henkin tree (in L) would give some path of length γ extending σ that is consistent with T. This path is a constructible subset of γ and so in L_{κ} contrary to our assumption. Thus there are finitely many sentences in T_{σ} ∪ (T ∩ L_{γ}) which are inconsistent. All of them from T_{σ} appear first at some successor level element τ ⊆ σ of H and so τ has no successors at level γ in H as required.

Thus by FCTP_{κ}, H has a path P of length κ. One can now κ-recursively build a model of T ∪ {T_{σ}|σ ∈ P } as usual.

(2) ⊨_{c} (3): Given X ∈ S, A and B as in the statement of Σ_{1}-Separation, we define a theory T in the language of propositional logic of size κ. The language consists of the propositional letters p_{γ} for γ < κ. If β is enumerated in A at stage γ we put p_{2γ} → p_{2β+1} and ¬p_{2γ} → p_{2β+1} into T. If β is enumerated in B at stage γ we put p_{2γ} → ¬p_{2β+1} and ¬p_{2γ} → ¬p_{2β+1} into T. It is clear that T ≤_{κ} X as we can get T ↾ γ from κ-finite information about A and B essentially determined by X ↾ γ. As T is consistent by the disjointness of A and B, by (2) we have a model M of T in S. We can now define the required separator C ≤_{κ} M by β ∈ C ⇔ M ⊨ p_{2β+1}.

(3) ⊨_{c} (1): Let T ∈ S be a binary tree on κ of finite character. We define Σ_{1}^{T} sets A and B as usual: A = {σ|∃γ(σˆ 0 has no successors on T at level γ but σˆ 1 has successors on T at every level β < γ} and B = {σ|∃γ(σˆ 1 has no successors on T at level γ but σˆ 0 has successors on T at level γ}. It is clear that A and B are Σ_{1}^{T} and disjoint. Thus we have a separator C ∈ S by (3). We can now κ-recursively in C define a path P in T of length κ as required: We begin with ∅ ∈ P and then, recursively, say that if σ ∈ P then σˆ 1 ∈ P if σ ∈ C and σˆ 0 ∈ P if σ ∉ C. At limit levels, we take the union σ of the path so far. We argue by induction up to κ that T is unbounded above every σ ∈ P and so P has length κ. At successor levels this is immediate by the definitions of A, B and C and the inductive hypothesis. At limit levels λ, note first that as T is of finite character, the union σ of the path defined so far is at least a node on T. If σ does not have successors at every level of T then as T is of finite character there would be a proper initial segment δ of σ that does not have unboundedly many successors in T as well contradicting our inductive hypothesis.

We close this section with a sample theorem of classical mathematics that is κcomputably equivalent to FCTP_{κ} (and so to the κ versions of Σ_{1}-Separation and first order compactness).

Theorem 3.7. The theorem that every commutative ring of size κ has a prime ideal is κ-computably equivalent to FCTP_{κ}.

Proof. For the classical direction, suppose we have a ring R = {a_{i}|i < κ} (with a_{0} the 0 of R and a_{1} the 1 of R) coded in S. For the purposes of illustration, we offer two proofs. One shows how in this setting we can appeal to classical, nonconstrucive arguments to get a computably simple solution. The other is more traditionally constructive as one would see in a typical reverse mathematical argument.

For our first proof, we define a binary tree T ≤_{κ} R such that any path P of length κ is (the characteristic function of) a prime ideal I in R. We begin by putting ∅, ⟨1⟩ and ⟨1, 0⟩ into T and no other strings of length at most 2. We then put every other binary string σ on κ into T unless there are i_{1}, …, i_{n}, j_{1}, …, j_{n}, k_{1}, …, k_{m} < |σ| such that σ(j_{l}) = 1 for l ≤ n, σ(k_{l}) = 0 for l ≤ m but ∑_{l≤n} a_{i_{l}}a_{j_{l}} = ∏_{l≤m} a_{k_{l}}.

Suppose P is a path in T of length κ. We let I = {a_{i}|P (i) = 1} and note that by our conditions for terminating paths in T, I is a prime ideal of R. (First, 0 ∈ I while 1 ∉ I by our fixing of the first two entries on T. If a_{i}, a_{j} ∈ I but a_{k} = a_{i} + a_{j} does not, then we would violate the defining condition. Similarly if a_{j} ∈ I but a_{k} = a_{i}a_{j} does not or if a_{i}, a_{j} ∉ I but a_{k} = a_{i}a_{j} does.) It is also clear that T is continuous at limit levels by the finite nature of the condition for termination. Thus, to get a path of length κ in S we only need to show that if some node σ of limit length λ has no successors at some level γ > λ then some τ ⊆ σ not of limit length also has no successors at some level γ̂. (As T will then be of finite character and so have a path of length κ in S.) This however, is immediate from the classical proof. If one begins with σ such that there is no violation of the defining condition with only the j_{l} and k_{l} restricted to be less than |σ|, i.e. no linear combination of elements already in I gives a product of elements already determined to not be in I, then a maximal extension of the set defined by σ with this property is a prime (indeed maximal) ideal and so σ has extensions on T at every level below κ. On the other hand, if σ does violate this unrestricted condition then some finite subset of it contained in some τ ⊆ σ not of limit length also violates it and so there is a level γ̂ at which the violating combination is found and so τ has no successors on T after γ̂.

We next provide a similar proof using Σ_{1}-Separation that does not rely explicitly on the classical argument. We begin with a list Q_{δ} of all i_{1}, …, i_{n}, j_{1}, …, j_{n}, k_{1}, …, k_{m} such that ∑_{l≤n} a_{i_{l}}a_{j_{l}} = ∏_{l≤m} a_{k_{l}}. We say that a string σ satisfies Q_{δ}, σ ⊨ Q_{δ}, if σ(j_{l}) = 1 for l ≤ n and σ(k_{l}) = 0 for l ≤ m. We now define disjoint Σ_{1}^{R} sets A and B of binary strings on κ by A = {σ ⊇ ⟨1, 0⟩ |∃δ(σˆ 0 ⊨ Q_{δ} & ∀γ ≤ δ(σˆ 1 ⊭ Q_{γ})} and B = {σ ⊇ ⟨1, 0⟩ |∃δ(σˆ 1 ⊨ Q_{δ} & ∀γ < δ(σˆ 0 ⊭ Q_{γ})}. Now let C ∈ S be a separating set for A and B. Define by recursion on κ a characteristic function beginning with ⟨1, 0⟩ and continuing at later steps σ by extending to σˆ C(σ). This gives a characteristic function f. We now set I = {a_{i}|f(i) = 1}. Clearly I ≤_{κ} C and so is in S. We claim that it is a prime ideal of R. We prove by induction on the length of initial segments σ of f that σ ⊭ Q_{δ} for every δ. This is clear for |σ| = 2 and at limit levels. At successor levels the only way it could fail would be for both σˆ 0 and σˆ 1 to satisfy some Q_{δ_{0}} and Q_{δ_{1}}. (If neither do, then there is nothing to prove. If only one does, then the definitions of A and B and the choice of C as a separator guarantees that σˆ (1 − C(σ)) does and so σˆ C(σ) does not.) So suppose, for the sake of a contradiction, that we have such examples and so, relabeling to reduce the number of subscripts, we have a_{i}, c_{j} ∈ σ, b_{k}, d_{l} ∉ σ and a = a_{|σ|} such that ∑ r_{i}a_{i} = a^{n} ∏ b_{k} and sa + ∑ s_{j}c_{j} = ∏ d_{l} for some r_{i}, s_{j}, s ∈ R and n ∈ ℕ. Multiplying both sides of the first equation by s^{n} gives ∑ r_{i}s^{n}a_{i} = (sa)^{n} ∏ b_{k}. Solving the second for sa gives sa = ∏ d_{l} − ∑ s_{j}c_{j}. Substituting the second result into the first gives ∑ r_{i}s^{n}a_{i} = ∏ b_{k}(∏ d_{l} − ∑ s_{j}c_{j})^{n}. Now expanding out the right hand side of this last equation gives ∏ b_{k}(∏ d_{l})^{n} plus a sum of terms all of which contain at least one c_{j}, Moving all of these terms over to the left hand side makes that side into a linear combination of elements in σ with coefficients in R while leaving the right hand side a product of elements declared not in σ for the desired contradiction.

We conclude with the reversal by showing the existence of prime ideals implies Σ_{1}- Separation. Suppose we have X ∈ S and disjoint Σ_{1}^{X} sets W_{e}^{X} and W_{i}^{X} (with enumerations of W_{e,γ}^{X} and W_{i,γ}^{X} κ-recursive in X such that at most one element is enumerated at any γ) for which we want to find a separator in S. Note that if either of the enumerations is bounded then the set is κ-finite and separation is immediate so we assume that they are unbounded. We begin with the ring of polynomials over the rationals generated by variables x_{β} and y_{β} for β < κ, R_{0} = Q[x_{β}, y_{β}|β < κ]. Let B = {x_{α}y_{δ}|α ∈ W_{e,δ}^{X}} ∪ {x_{β}y_{γ} − 1|β ∈ W_{i,at γ}^{X}} and I_{0} be the ideal generated in R_{0} by B. It is clear that B ≤_{κ} X. We also claim that I_{0} ≠ R_{0}: The only way that 1 could be in I_{0} is if there are α and δ such that α ∈ W_{e,δ}^{X} and α ∈ W_{i,at δ}^{X} but this would contradict the disjointness of W_{e}^{X} and W_{i}^{X}.

We now define a ring R isomorphic to R_{0}/I_{0} by choosing representatives of the equivalence classes and defining the operations accordingly. Every member of R is given initially as a finite sum of terms of the form q ∏ x_{β_{i}} ∏ y_{δ_{j}} for rational q and finite sequences β_{i} and δ_{j}. We prescribe a procedure to reduce such terms to a canonical form modulo I_{0}. Let δ be larger than every β_{i} and δ_{j} appearing in this sum. For each pair β_{i}, δ_{j} appearing ask if β_{i} ∈ W_{e,δ_{j}}^{X}, if so set all terms containing both x_{β_{i}} and y_{δ_{j}} to 0. If not, see if β_{i} ∈ W_{i,at δ_{j}}^{X} and remove x_{β_{i}} and y_{δ_{j}} from any term containing them. Note that for each β_{i} there is at most one δ_{j} for which β_{i} ∈ W_{i,at δ_{j}}^{X} and vice versa so that this procedure has only one possible outcome. We take the range of this procedure on R_{0} as the universe of our desired ring R. The ring operations are defined as expected. We perform the operations in R_{0} and the apply the procedure to produce the canonical representative in R. It is routine to check that this endows R with the structure of a ring over Q. Moreover, this ring is κ-recursive in X as the reduction procedure only needs W_{e,δ}^{X} and W_{i,δ}^{X} where δ is larger than all the subscripts appearing in a given term. Thus R ∈ S.

Now suppose that I ∈ S is a prime ideal in R. If β ∈ W_{e}^{X} then x_{β}y_{δ} ∈ I for all sufficiently large δ. On the other hand, as the enumeration of W_{i}^{X} is unbounded there are arbitrarily large δ such that, for some ν, (x_{ν}y_{δ} − 1) ∈ B. No such y_{δ} can be in I as if it were, then x_{ν}y_{δ} and hence 1 would also be in I. Thus x_{β} ∈ I. On the other hand, if β ∈ W_{i}^{X} then for some δ, β ∈ W_{i,at δ}^{X} and so (x_{β}y_{δ} − 1) ∈ B and so again as 1 ∉ I, x_{β} ∉ I. Thus {β|x_{β} ∈ I} is a separating set for W_{e}^{X} and W_{i}^{X} which is κ-recursive in I and so in S as required.

An obvious issue here is whether FCTP_{κ} and closure under κ-jump are different conditions. They are, of course, for κ = ω and we believe they are for certain uncountable κ of countable cofinality but, in general, it seems an interesting question.

Problem 3.8. Is FCTP_{κ} a strictly weaker condition on κ-closed sets than closure under κ-jump for every uncountable κ.

4 ATR and Π_{1}^{1}-CA in α-recursion theory

A natural candidate for the analog of Π_{1}^{1}-CA_{0} is, of course, closure under definability by formulas with a single second order quantifier. We have not yet looked for any equivalences at this level.

Problem 4.1. What mathematical theorems are computably equivalent (in the sense of α-recursion theory) to closure under definability over L_{κ} by formulas with a single second order quantifier.

It is not clear what the appropriate basic yardstick corresponding to ATR_{0} should be. A candidate for analysis here is König’s Duality Theorem (KDT) which is equivalent to ATR_{0} in the countable case [2],[19]. The arguments of [2] show that KDT is strictly stronger than closure under first order definability for every κ, i.e. it is not computably entailed by closure under the κ-jump. We do not know what reasonable closure notion (if any) might κ-computably entail KDT for uncountable κ but one possibility is suggested by the analysis of KDT in [2] is a direct analog of the definition of the H sets.

Definition 4.2. We say that a κ-closed set S is κ-hyperarithmetically closed if it is closed under projections (i.e. if S ∈ S then {x|∃β(⟨x, β⟩ ∈ S} ∈ S and under κ-recursive unions (i.e. if there is a sequence ⟨S_{β}|β < λ⟩ for some λ < κ of sets given uniformly κ-recursively as projections at successor levels and as effective unions at limit levels, then the effective join, {⟨β, x⟩ |β < λ & x ∈ S_{β}}, is also in S.

The analysis of KDT in [2] shows that it κ-computably entails hyperarithmetic closure. It is far from clear if any reversal is possible.

Problem 4.3. Is hyperarithmetic closure equivalent to KDT for every κ? What about comparability of well orderings (of subsets of κ)? (Note that if cf(κ) > ω then being well-founded is a co-κ-r.e. relation so the situation in general for well-orderings is quite different than in the countable case.) If this is not the “right” analog for ATR_{0} in α-recursion theory, then what is?

5 E-recursion and related systems

Turning to analysis and related subjects about ℝ, we just note that an old result of Grilliot [8] can be seen from our point of view as showing that the existence of a noncontinuous functional is computably equivalent to the existence of ^{2}E. In this setting there are also proof theoretic approaches that correspond to Kleene recursion in higher types as the classical proof theoretic systems do to Turing computability (see [11] where other examples from E-recursion are analyzed proof theoretically).

Problem 5.1. Analyze the classical theorems of analysis in terms of computable entailment and equivalence with computation taken to be Kleene Recursion in higher types, E-recursion or Blum-Shub-Smale computability.

References

[1] Aharoni, R., König’s duality theorem for infinite bipartite graphs, J. Lon. Math. Soc. (3) 29 (1984), 1-12.

[2] Aharoni, R., Magidor, M., and Shore, R. A., On the strength of König’s duality theorem for infinite bipartite graphs, J. Combin. Theory Ser. B 54 (1992) 257–290.

[3] Blum, Lenore, Cucker, Felipe, Shub, Michael and Smale, Steve, Complexity and Real Computation, Springer-Verlag, New York, 1998.

[4] Chong, C. T. Techniques of Admissible Recursion Theory, LNM 1106, Springer-Verlag, Berlin, 1984.

[5] Fenstad, Jens Erik, .General Recursion Theory: An Axiomatic Approach, Perspectives in Mathematical Logic, Springer-Verlag, Berlin-New York, 1980.

[6] Friedman, H., Higher set theory and mathematical practice, Ann. Math. Logic 2 (1971), 326-357.

[7] Friedman, H., Some systems of second order arithmetic and their use, Proc. Intl. Cong. Math., Vancouver 1974, v. 1, Can. Math. Congress, 1975, 235-242.

[8] Grilliot, T. J. On effectively discontinuous type-2 objects. J. Symbolic Logic 36 (1971) 245–248.

[9] Hirst, J., Marriage theorems and reverse mathematics, in Logic and Computation (Pittsburgh, PA, 1987), Contemporary Mathematics 106, Amer. Math. Soc., Providence, RI, 1990, 181–196 .

[10] Jockusch, C. G. jr. and Soare, R. I., Π_{1}^{0} classes and the degrees of theories, Tran. AMS 173 (1972), 33-56.

[11] Kohlenbach, U., Higher order reverse mathematics in Reverse mathematics 2001, S. Simpson ed., 281–295, Lect. Notes Log. 21, Assoc. Symbol. Logic and A. K. Peters, Wellesley MA 2005.

[12] Lovasz, L. and Plummer, M. D., Matching Theory, Ann. Discrete Math. 29, North-Holland, Amsterdam, 1986.

[13] Metakides, G. and Nerode, A., Recursively enumerable vector spaces, Ann. Math. Logic 11 (1977), 147-171.

[14] Moldestad, J., Computations in Higher Types, LNM 574, Springer-Verlag, Berlin, 1977.

[15] Mummert, C. and Simpson, S. G. [2005], Reverse Mathematics and Π_{2}^{1} comprehension, Bulletin of Symbolic Logic 11, 526–533.

[16] Montalbán, A. and Shore, R. A. [2011], The limits of determinacy in second order arithmetic, to appear.

[17] Sacks, Gerald E., Higher recursion theory, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1990.

[18] Shore, R. A., On the jump of an α-recursively enumerable set, Trans. AMS 217 (1976), 351-364.

[19] Simpson, S., On the strength of König’s duality theorem for countable bipartite graphs, J. Symbolic Logic 59 (1994) 113–123.

[20] Simpson, S., Subsystems of Second Order Arithmetic, 2nd edition, Perspectives in Logic, Association for Symbolic Logic and Cambridge University Press, New York, 2009.