Classically, weak König's lemma and Brouwer's fan theorem for detachable bars are equivalent. We give a direct constructive proof that the former implies the latter.

We show how to interpret weak Kőnig's lemma in some recently defined theories of nonstandard arithmetic in all finite types. Two types of interpretations are described, with very different verifications. The celebrated conservation result of Friedman's about weak Kőnig's lemma can be proved using these interpretations. We also address some issues concerning the collecting of witnesses in herbrandized functional interpretations.

We develop measure theory in the context of subsystems of second order arithmetic with restricted induction. We introduce a combinatorial principleWWKL (weak-weak König's lemma) and prove that it is strictly weaker thanWKL (weak König's lemma). We show thatWWKL is equivalent to a formal version of the statement that Lebesgue measure is countably additive on open sets. We also show thatWWKL is equivalent to a formal version of the statement that any Borel measure on a compact (...) metric space is countably additive on open sets. (shrink)

By , we denote the system of second-order arithmetic based on recursive comprehension axioms and Σ10 induction. is defined to be plus weak König's lemma: every infinite tree of sequences of 0's and 1's has an infinite path. In this paper, we first show that for any countable model M of , there exists a countable model M′ of whose first-order part is the same as that of M, and whose second-order part consists of the M-recursive sets and (...) sets not in the second-order part of M. By combining this fact with a certain forcing argument over universal trees, we obtain the following result : if proves X!Y with arithmetical, so does . We also discuss several improvements of this results. (shrink)

We provide a fine‐grained analysis on the relation between König's lemma, weak König's lemma, and the decidable fan theorem in the context of constructive reverse mathematics. In particular, we show that double negated variants of König's lemma and weak König's lemma are equivalent to double negated variants of the general decidable fan theorem and the binary decidable fan theorem, respectively, over a nearly intuitionistic system containing a weak countable choice only. This implies that (...) the general decidable fan theorem is not equivalent to the binary decidable fan theorem in the absence of a strong countable choice. In addition, we introduce a principle which fills the gap between König's lemma and weak König's lemma, and show that König's lemma is equivalent to weak König's lemma plus this principle. We also solve several problems arising from the investigation. (shrink)

We introduce a herbrandized functional interpretation of a first-order semi-intuitionistic extension of Heyting Arithmetic and study its main properties. We then extend the interpretation to a certain system of second-order arithmetic which includes a (classically false) formulation of the FAN principle and weak König's lemma. It is shown that any first-order formula provable in this system is classically true. It is perhaps worthy of note that, in our interpretation, second-order variables are interpreted by finite sets of natural numbers.

The so-called weak König's lemma WKL asserts the existence of an infinite path b in any infinite binary tree . Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are Π 2 0 -conservative over primitive recursive arithmetic PRA . In Kohlenbach 1239–1273) we established such conservation results relative to finite type extensions PRA ω of PRA . In this setting one can consider also (...) a uniform version UWKL of WKL which asserts the existence of a functional Φ which selects uniformly in a given infinite binary tree f an infinite path Φf of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in Kohlenbach [10] actually can be used to eliminate even this uniform weak König's lemma provided that PRA ω only has a quantifier-free rule of extensionality QF-ER instead of the full axioms of extensionality for all finite types. In this paper we show that in the presence of , UWKL is much stronger than WKL: whereas WKL remains to be Π 2 0 -conservative over PRA, PRA ω ++ UWKL contains full Peano arithmetic PA. We also investigate the proof–theoretic as well as the computational strength of UWKL relative to the intuitionistic variant of PRA ω both with and without the Markov principle. (shrink)

We continue the work of [14, 3, 1, 19, 16, 4, 12, 11, 20] investigating the strength of set existence axioms needed for separable Banach space theory. We show that the separation theorem for open convex sets is equivalent to WKL 0 over RCA 0 . We show that the separation theorem for separably closed convex sets is equivalent to ACA 0 over RCA 0 . Our strategy for proving these geometrical Hahn-Banach theorems is to reduce to the finite-dimensional case (...) by means of a compactness argument. (shrink)

We continue the work of [14, 3, 1, 19, 16, 4, 12, 11, 20] investigating the strength of set existence axioms needed for separable Banach space theory. We show that the separation theorem for open convex sets is equivalent to WKL$_0$ over RCA$_0$. We show that the separation theorem for separably closed convex sets is equivalent to ACA$_0$ over RCA$_0$. Our strategy for proving these geometrical Hahn-Banach theorems is to reduce to the finite-dimensional case by means of a compactness argument.

In this paper, we show within RCA 0 that weak Konig's lemma is necessary and sufficient to prove that any (separable) compact group has a Haar measure. Within WKL 0 , a Haar measure is constructed by a non-standard method based on a fact that every countable non-standard model of WKL 0 has a proper initial part isomorphic to itself [10].

In this paper, we propose a weak regularity principle which is similar to both weak König's lemma and Ramsey's theorem. We begin by studying the computational strength of this principle in the context of reverse mathematics. We then analyze different ways of generalizing this principle.

We study the computational content of the Brouwer Fixed Point Theorem in the Weihrauch lattice. Connected choice is the operation that finds a point in a non-empty connected closed set given by negative information. One of our main results is that for any fixed dimension the Brouwer Fixed Point Theorem of that dimension is computably equivalent to connected choice of the Euclidean unit cube of the same dimension. Another main result is that connected choice is complete for dimension greater than (...) or equal to two in the sense that it is computably equivalent to Weak Kőnig’s Lemma. While we can present two independent proofs for dimension three and upward that are either based on a simple geometric construction or a combinatorial argument, the proof for dimension two is based on a more involved inverse limit construction. The connected choice operation in dimension one is known to be equivalent to the Intermediate Value Theorem; we prove that this problem is not idempotent in contrast to the case of dimension two and upward. We also prove that Lipschitz continuity with Lipschitz constants strictly larger than one does not simplify finding fixed points. Finally, we prove that finding a connectedness component of a closed subset of the Euclidean unit cube of any dimension greater than or equal to one is equivalent to Weak Kőnig’s Lemma. In order to describe these results, we introduce a representation of closed subsets of the unit cube by trees of rational complexes. (shrink)

We consider the relation between versions of Ramsey’s Theorem and König’s Infinity Lemma, in the absence of the axiom of choice.

We consider the relation between versions of Ramsey’s Theorem and König’s Infinity Lemma, in the absence of the axiom of choice.

We prove constructively that the weak König lemma and quantifier-free number-number choice imply that every pointwise continuous function from Cantor space into Baire space has a modulus of uniform continuity.

In this paper, we discuss uniform versions of some axioms of second order arithmetic in the context of higher order arithmetic. We prove that uniform versions of weak weak König's lemma WWKL and Σ01 separation are equivalent to over a suitable base theory of higher order arithmetic, where is the assertion that there exists Φ2 such that Φf1 = 0 if and only if ∃x0 for all f. We also prove that uniform versions of some well-known theorems (...) are equivalent to or the axiom of the existence of the Suslin operator. (shrink)

We apply the method of asymmetric interpretation to the basic fragment of bounded arithmetic, endowed with a weak collection schema, and to a system of “feasible analysis”, introduced by Ferreira and based on weak König's lemma, recursive comprehension and NP-notation induction. As a byproduct, we obtain two conservation results.

We determine the computational complexity of the Hahn-Banach Extension Theorem. To do so, we investigate some basic connections between reverse mathematics and computable analysis. In particular, we use Weak König's Lemma within the framework of computable analysis to classify incomputable functions of low complexity. By defining the multivalued function Sep and a natural notion of reducibility for multivalued functions, we obtain a computational counterpart of the subsystem of second-order arithmetic WKL0. We study analogies and differences between WKL0 and (...) the class of Sep-computable multivalued functions. Extending work of Brattka, we show that a natural multivalued function associated with the Hahn-Banach Extension Theorem is Sep-complete. (shrink)

König, D. [1926. ‘Sur les correspondances multivoques des ensembles’, Fundamenta Mathematica, 8, 114–34] includes a result subsequently called König's Infinity Lemma. Konig, D. [1927. ‘Über eine Schlussweise aus dem Endlichen ins Unendliche’, Acta Litterarum ac Scientiarum, Szeged, 3, 121–30] includes a graph theoretic formulation: an infinite, locally finite and connected graph includes an infinite path. Contemporary applications of the infinity lemma in logic frequently refer to a consequence of the infinity lemma: an infinite, locally finite tree with (...) a root has a infinite branch. This tree lemma can be traced to [Beth, E. W. 1955. ‘Semantic entailment and formal derivability’, Mededelingen der Kon. Ned. Akad. v. Wet., new series 18, 13, 309–42]. It is argued that Beth independently discovered the tree lemma in the early 1950s and that it was later recognized among logicians that Beth's result was a consequence of the infinity lemma. The equivalence of these lemmas is an easy consequence of a well known result in graph theory: every connected, locally finite graph has among its partial subgraphs a spanning tree. (shrink)

We explore the connections between Dickson’s lemma and weak Ramsey theory. We show that a weak version of the Paris–Harrington principle for pairs in c colors and miniaturized Dickson’s lemma for c-tuples are equivalent over \. Furthermore, we look at a cascade of consequences for several variants of weak Ramsey’s theorem.

In this paper we study a reducibility that has been introduced by Klaus Weihrauch or, more precisely, a natural extension for multi-valued functions on represented spaces. We call the corresponding equivalence classes Weihrauch degrees and we show that the corresponding partial order induces a lower semi-lattice. It turns out that parallelization is a closure operator for this semi-lattice and that the parallelized Weihrauch degrees even form a lattice into which the Medvedev lattice and the Turing degrees can be embedded. The (...) importance of Weihrauch degrees is based on the fact that multi-valued functions on represented spaces can be considered as realizers of mathematical theorems in a very natural way and studying the Weihrauch reductions between theorems in this sense means to ask which theorems can be transformed continuously or computably into each other. As crucial corner points of this classification scheme the limited principle of omniscience LPO, the lesser limited principle of omniscience LLPO and their parallelizations are studied. It is proved that parallelized LLPO is equivalent to Weak Kőnig's Lemma and hence to the Hahn—Banach Theorem in this new and very strong sense. We call a multi-valued function weakly computable if it is reducible to the Weihrauch degree of parallelized LLPO and we present a new proof, based on a computational version of Kleene's ternary logic, that the class of weakly computable operations is closed under composition. Moreover, weakly computable operations on computable metric spaces are characterized as operations that admit upper semi-computable compact-valued selectors and it is proved that any single-valued weakly computable operation is already computable in the ordinary sense. (shrink)

Halin in 1965 proved that if a graph has [Formula: see text] many pairwise disjoint rays for each [Formula: see text] then it has infinitely many pairwise disjoint rays. We analyze the complexity of this and other similar results in terms of computable and proof theoretic complexity. The statement of Halin’s theorem and the construction proving it seem very much like standard versions of compactness arguments such as König’s Lemma. Those results, while not computable, are relatively simple. They only (...) use arithmetic procedures or, equivalently, finitely many iterations of the Turing jump. We show that several Halin-type theorems are much more complicated. They are among the theorems of hyperarithmetic analysis. Such theorems imply the ability to iterate the Turing jump along any computable well ordering. Several important logical principles in this class have been extensively studied beginning with work of Kreisel, H. Friedman, Steel and others in the 1960s and 1970s. Until now, only one purely mathematical example was known. Our work provides many more and so answers Question 30 of Montalbán’s Open Questions in Reverse Mathematics in 2011. Some of these theorems including ones in Halin in 1965 are also shown to have unusual proof theoretic strength as well. (shrink)

In this paper, we show within ${\mathsf{RCA}_0}$ that both the Jordan curve theorem and the Schönflies theorem are equivalent to weak König’s lemma. Within ${\mathsf {WKL}_0}$ , we prove the Jordan curve theorem using an argument of non-standard analysis based on the fact that every countable non-standard model of ${\mathsf {WKL}_0}$ has a proper initial part that is isomorphic to itself (Tanaka in Math Logic Q 43:396–400, 1997).

Many existence propositions in constructive analysis are implied by the lesser limited principle of omniscience LLPO; sometimes one can even show equivalence. It was discovered recently that some existence propositions are equivalent to Bouwer's fan theorem FAN if one additionally assumes that there exists at most one object with the desired property. We are providing a list of conditions being equivalent to FAN, such as a unique version of weak König's lemma. This illuminates the relation between FAN and (...) LLPO. Furthermore, we give a short and elementary proof of the fact that FAN is equivalent to each positive valued function with compact domain having positive infimum. (shrink)

This paper addresses the strength of Ramsey's theorem for pairs ($RT^2_2$) over a weak base theory from the perspective of 'proof mining'. Let $RT^{2-}_2$ denote Ramsey's theorem for pairs where the coloring is given by an explicit term involving only numeric variables. We add this principle to a weak base theory that includes weak König's Lemma and a substantial amount of $\Sigma^0_1$-induction (enough to prove the totality of all primitive recursive functions but not of all primitive (...) recursive functionals). In the resulting theory we show the extractability of primitive recursive programs and uniform bounds from proofs of $\forall\exists$-theorems. There are two components of this work. The first component is a general proof-theoretic result, due to the second author, that establishes conservation results for restricted principles of choice and comprehension over primitive recursive arithmetic PRA as well as a method for the extraction of primitive recursive bounds from proofs based on such principles. The second component is the main novelty of the paper: it is shown that a proof of Ramsey's theorem due to Erdős and Rado can be formalized using these restricted principles. So from the perspective of proof unwinding the computational content of concrete proofs based on $RT^2_2$ the computational complexity will, in most practical cases, not go beyond primitive recursive complexity. This even is the case when the theorem to be proved has function parameters f and the proof uses instances of $RT^2_2$ that are primitive recursive in f. (shrink)

Concepts of L1 space, integrable functions and integrals are formalized in weak subsystems of second order arithmetic. They are discussed especially in relation with the combinatorial principle WWKL (weak-weak König's lemma and arithmetical comprehension. Lebesgue dominated convergence theorem is proved to be equivalent to arithmetical comprehension. A weak version of Lebesgue monotone convergence theorem is proved to be equivalent to weak-weak König's lemma.

Elementary Recursive Nonstandard Analysis, in short ERNA, is a constructive system of nonstandard analysis with a PRA consistency proof, proposed around 1995 by Patrick Suppes and Richard Sommer. Recently, the author showed the consistency of ERNA with several transfer principles and proved results of nonstandard analysis in the resulting theories (see [12] and [13]). Here, we show that Weak König's lemma (WKL) and many of its equivalent formulations over RCA₀ from Reverse Mathematics (see [21] and [22]) can be (...) 'pushed down' into the weak theory ERNA, while preserving the equivalences, but at the price of replacing equality with equality 'up to infinitesimals'. It turns out that ERNA plays the role of RCA₀ and that transfer for universal formulas corresponds to WKL. (shrink)

An infinite binary sequence X is Kolmogorov–Loveland random if there is no computable non-monotonic betting strategy that succeeds on X in the sense of having an unbounded gain in the limit while betting successively on bits of X. A sequence X is KL-stochastic if there is no computable non-monotonic selection rule that selects from X an infinite, biased sequence.One of the major open problems in the field of effective randomness is whether Martin-Löf randomness is the same as KL-randomness. Our first (...) main result states that KL-random sequences are close to Martin-Löf random sequences in so far as every KL-random sequence has arbitrarily dense subsequences that are Martin-Löf random. A key lemma in the proof of this result is that for every effective split of a KL-random sequence at least one of the halves is Martin-Löf random. However, this splitting property does not characterize KL-randomness; we construct a sequence that is not even computably random such that every effective split yields two subsequences that are 2-random. Furthermore, we show for any KL-random sequence A that is computable in the halting problem that, first, for any effective split of A both halves are Martin-Löf random and, second, for any computable, nondecreasing, and unbounded function g and almost all n, the prefix of A of length n has prefix-free Kolmogorov complexity at least n−g. Again, the latter property does not characterize KL-randomness, even when restricted to left-r.e. sequences; we construct a left-r.e. sequence that has this property but is not KL-stochastic and, in fact, is not even Mises–Wald–Church stochastic.Turning our attention to KL-stochasticity, we construct a non-empty class of KL-stochastic sequences that are not weakly 1-random; by the usual basis theorems we obtain such sequences that in addition are left-r.e., are low, or are of hyperimmune-free degree.Our second main result asserts that every KL-stochastic sequence has effective dimension 1, or equivalently, a sequence cannot be KL-stochastic if it has infinitely many prefixes that can be compressed by a factor of α<1. This improves on a result by Muchnik, who has shown that were they to exist, such compressible prefixes could not be found effectively. (shrink)

Dini's theorem says that compactness of the domain, a metric space, ensures the uniform convergence of every simply convergent monotone sequence of real-valued continuous functions whose limit is continuous. By showing that Dini's theorem is equivalent to Brouwer's fan theorem for detachable bars, we provide Dini's theorem with a classification in the recently established constructive reverse mathematics propagated by Ishihara. As a complement, Dini's theorem is proved to be equivalent to the analogue of the fan theorem, weak König's (...) class='Hi'>lemma, in the original classical setting of reverse mathematics started by Friedman and Simpson. (shrink)

Leo Harrington showed that the second-order theory of arithmetic WKL 0 is ${\Pi^1_1}$ -conservative over the theory RCA 0. Harrington’s proof is model-theoretic, making use of a forcing argument. A purely proof-theoretic proof, avoiding forcing, has been eluding the efforts of researchers. In this short paper, we present a proof of Harrington’s result using a cut-elimination argument.

The Stone's Separation Theorem is equivalent to Weak König's Lemma.

The Stone's Separation Theorem is equivalent to Weak König's Lemma.

Let ${2-\textsf{RAN}}$ be the statement that for each real X a real 2-random relative to X exists. We apply program extraction techniques we developed in Kreuzer and Kohlenbach (J. Symb. Log. 77(3):853–895, 2012. doi:10.2178/jsl/1344862165), Kreuzer (Notre Dame J. Formal Log. 53(2):245–265, 2012. doi:10.1215/00294527-1715716) to this principle. Let ${{\textsf{WKL}_0^\omega}}$ be the finite type extension of ${\textsf{WKL}_0}$ . We obtain that one can extract primitive recursive realizers from proofs in ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} + 2-\textsf{RAN}}$ , i.e., if ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} + 2-\textsf{RAN} (...) \, {\vdash} \, \forall{f}\, {\exists}{x} A_{qf}(f,x)}$ then one can extract from the proof a primitive recursive term t(f) such that ${A_{qf}(f,t(f))}$ . As a consequence, we obtain that ${{\textsf{WKL}_0}+ \Pi^0_1 - {\textsf{CP}} + 2-\textsf{RAN}}$ is ${\Pi^0_3}$ -conservative over ${\textsf{RCA}_0}$. (shrink)

We investigate the provability or nonprovability of certain ordinary mathematical theorems within certain weak subsystems of second order arithmetic. Specifically, we consider the Cauchy/Peano existence theorem for solutions of ordinary differential equations, in the context of the formal system RCA 0 whose principal axioms are ▵ 0 1 comprehension and Σ 0 1 induction. Our main result is that, over RCA 0 , the Cauchy/Peano Theorem is provably equivalent to weak Konig's lemma, i.e. the statement that (...) every infinite {0, 1}-tree has a path. We also show that, over RCA 0 , the Ascoli lemma is provably equivalent to arithmetical comprehension, as is Osgood's theorem on the existence of maximum solutions. At the end of the paper we digress to relate our results to degrees of unsolvability and to computable analysis. (shrink)

We present a new functional interpretation, based on a novel assignment of formulas. In contrast with Gödel’s functional “Dialectica” interpretation, the new interpretation does not care for precise witnesses of existential statements, but only for bounds for them. New principles are supported by our interpretation, including the FAN theorem, weak König’s lemma and the lesser limited principle of omniscience. Conspicuous among these principles are also refutations of some laws of classical logic. Notwithstanding, we end up discussing some applications (...) of the new interpretation to theories of classical arithmetic and analysis. (shrink)

In this paper we study a new approach to classify mathematical theorems according to their computational content. Basically, we are asking the question which theorems can be continuously or computably transferred into each other? For this purpose theorems are considered via their realizers which are operations with certain input and output data. The technical tool to express continuous or computable relations between such operations is Weihrauch reducibility and the partially ordered degree structure induced by it. We have identified certain choice (...) principles such as co-finite choice, discrete choice, interval choice, compact choice and closed choice, which are cornerstones among Weihrauch degrees and it turns out that certain core theorems in analysis can be classified naturally in this structure. In particular, we study theorems such as the Intermediate Value Theorem, the Baire Category Theorem, the Banach Inverse Mapping Theorem, the Closed Graph Theorem and the Uniform Boundedness Theorem. We also explore how existing classifications of the Hahn—Banach Theorem and Weak Kőnig's Lemma fit into this picture. Well-known omniscience principles from constructive mathematics such as LPO and LLPO can also naturally be considered as Weihrauch degrees and they play an important role in our classification. Based on this we compare the results of our classification with existing classifications in constructive and reverse mathematics and we claim that in a certain sense our classification is finer and sheds some new light on the computational content of the respective theorems. Our classification scheme does not require any particular logical framework or axiomatic setting, but it can be carried out in the framework of classical mathematics using tools of topology, computability theory and computable analysis. We develop a number of separation techniques based on a new parallelization principle, on certain invariance properties of Weihrauch reducibility, on the Low Basis Theorem of Jockusch and Soare and based on the Baire Category Theorem. Finally, we present a number of metatheorems that allow to derive upper bounds for the classification of the Weihrauch degree of many theorems and we discuss the Brouwer Fixed Point Theorem as an example. (shrink)

We construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with Σ b 1 -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.

A function is diagonally non-computable if it diagonalizes against the universal partial computable function. D.n.c. functions play a central role in algorithmic randomness and reverse mathematics. Flood and Towsner asked for which functions h, the principle stating the existence of an h-bounded d.n.c. function implies Ramsey-type weak König’s lemma. In this paper, we prove that for every computable order h, there exists an ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\omega}$$\end{document} -model of h-DNR which is not (...) a not model of the Ramsey-type graph coloring principle for two colors and therefore not a model of RWKL. The proof combines bushy tree forcing and a technique introduced by Lerman, Solomon and Towsner to transform a computable non-reducibility into a separation over ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\omega}$$\end{document} -models. (shrink)

We analyze the pointwise convergence of a sequence of computable elements of L1 in terms of algorithmic randomness. We consider two ways of expressing the dominated convergence theorem and show that, over the base theory RCA0, each is equivalent to the assertion that every Gδ subset of Cantor space with positive measure has an element. This last statement is, in turn, equivalent to weak weak Königʼs lemma relativized to the Turing jump of any set. It is also (...) equivalent to the conjunction of the statement asserting the existence of a 2-random relative to any given set and the principle of Σ2 collection. (shrink)

This research is motivated by the program of Reverse Mathematics. We investigate basic part of complex analysis within some weak subsystems of second order arithmetic, in order to determine what kind of set existence axioms are needed to prove theorems of basic analysis. We are especially concerned with Cauchy’s integral theorem. We show that a weak version of Cauchy’s integral theorem is proved in RCAo. Using this, we can prove that holomorphic functions are analytic in RCAo. On the (...) other hand, we show that a full version of Cauchy’s integral theorem cannot be proved in RCAo but is equivalent to weak König’s lemma over RCAo. (shrink)

IΣ n andBΣ n are well known fragments of first-order arithmetic with induction and collection forΣ n formulas respectively;IΣ n 0 andBΣ n 0 are their second-order counterparts. RCA0 is the well known fragment of second-order arithmetic with recursive comprehension;WKL 0 isRCA 0 plus weak König's lemma. We first strengthen Harrington's conservation result by showing thatWKL 0 +BΣ n 0 is Π 1 1 -conservative overRCA 0 +BΣ n 0 . Then we develop some model theory inWKL 0 (...) and illustrate the use of formalized model theory by giving a relatively simple proof of the fact thatIΣ 1 provesBΣ n+1 to be Π n+2-conservative overIΣ n . Finally, we present a proof-theoretic proof of the stronger fact that theΠ n+2 conservation result is provable already inIΔ 0 + superexp. ThusIΣ n+1 proves 1-Con (BΣ n+1) andIΔ 0 +superexp proves Con (IΣ n )↔Con(BΣ n+1). (shrink)

We propose a new method for constructing Turing ideals satisfying principles of reverse mathematics below the Chain–Antichain (CAC) Principle. Using this method, we are able to prove several new separations in the presence of Weak König’s Lemma (WKL), including showing that CAC+WKL does not imply the thin set theorem for pairs, and that the principle “the product of well-quasi-orders is a well-quasi-order” is strictly between CAC and the Ascending/Descending Sequences principle, even in the presence of WKL.