scholarly journals Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization

1992 ◽  
Vol 57 (4) ◽  
pp. 1239-1273 ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Approximation Theory ◽  
Classical Analysis ◽  
Functional Interpretation ◽  
Image Position ◽  
Weak König’S Lemma ◽  
König’S Lemma

AbstractWe show how to extract effective bounds Φ for ⋀u1⋀v ≤ytu⋁wηG0-sentences which depend on u only (i.e. ⋀u⋀v ≤y, tu⋁w ≤η ΦuG0) from arithmetical proofs which use analytical assumptions of the form(ϒ, δ, ρ, and τ are arbitrary finite types, η ≤ 2, G0 and F0 are quantifier-free, and s and t are closed terms). If τ ≤ 2, (*) can be weakened toThis is used to establish new conservation results about weak Konig's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers.

scholarly journals ON THE UNIFORM COMPUTATIONAL CONTENT OF RAMSEY’S THEOREM

2017 ◽  
Vol 82 (4) ◽  
pp. 1278-1316 ◽  
Author(s):  
VASCO BRATTKA ◽  
TAHINA RAKOTONIAINA
Keyword(s):  
Finite Number ◽  
Ramsey's Theorem ◽  
Borel Hierarchy ◽  
Ramsey’S Theorem ◽  
Homogeneous Set ◽  
Colored Version ◽  
Output Information ◽  
Image Position ◽  
Weak König’S Lemma ◽  
König’S Lemma

AbstractWe study the uniform computational content of Ramsey’s theorem in the Weihrauch lattice. Our central results provide information on how Ramsey’s theorem behaves under product, parallelization, and jumps. From these results we can derive a number of important properties of Ramsey’s theorem. For one, the parallelization of Ramsey’s theorem for cardinalityn≥ 1 and an arbitrary finite number of colorsk≥ 2 is equivalent to then-th jump of weak Kőnig’s lemma. In particular, Ramsey’s theorem for cardinalityn≥ 1 is${\bf{\Sigma }}_{n + 2}^0$-measurable in the effective Borel hierarchy, but not${\bf{\Sigma }}_{n + 1}^0$-measurable. Secondly, we obtain interesting lower bounds, for instance then-th jump of weak Kőnig’s lemma is Weihrauch reducible to (the stable version of) Ramsey’s theorem of cardinalityn+ 2 forn≥ 2. We prove that with strictly increasing numbers of colors Ramsey’s theorem forms a strictly increasing chain in the Weihrauch lattice. Our study of jumps also shows that certain uniform variants of Ramsey’s theorem that are indistinguishable from a nonuniform perspective play an important role. For instance, the colored version of Ramsey’s theorem explicitly includes the color of the homogeneous set as output information, and the jump of this problem (but not the uncolored variant) is equivalent to the stable version of Ramsey’s theorem of the next greater cardinality. Finally, we briefly discuss the particular case of Ramsey’s theorem for pairs, and we provide some new separation techniques for problems that involve jumps in this context. In particular, we study uniform results regarding the relation of boundedness and induction problems to Ramsey’s theorem, and we show that there are some significant differences with the nonuniform situation in reverse mathematics.

scholarly journals THE STRENGTH OF THE TREE THEOREM FOR PAIRS IN REVERSE MATHEMATICS

2016 ◽  
Vol 81 (4) ◽  
pp. 1481-1499 ◽  
Author(s):  
LUDOVIC PATEY
Keyword(s):  
Binary Tree ◽  
Reverse Mathematics ◽  
Theoretic Property ◽  
Ramsey's Theorem ◽  
Ramsey’S Theorem ◽  
Image Position ◽  
Weak König’S Lemma ◽  
König’S Lemma ◽  
Comprehension Axiom

AbstractNo natural principle is currently known to be strictly between the arithmetic comprehension axiom (ACA0) and Ramsey’s theorem for pairs ($RT_2^2$) in reverse mathematics. The tree theorem for pairs ($TT_2^2$) is however a good candidate. The tree theorem states that for every finite coloring over tuples of comparable nodes in the full binary tree, there is a monochromatic subtree isomorphic to the full tree. The principle $TT_2^2$ is known to lie between ACA0 and $RT_2^2$ over RCA0, but its exact strength remains open. In this paper, we prove that $RT_2^2$ together with weak König’s lemma (WKL0) does not imply $TT_2^2$, thereby answering a question of Montálban. This separation is a case in point of the method of Lerman, Solomon and Towsner for designing a computability-theoretic property which discriminates between two statements in reverse mathematics. We therefore put the emphasis on the different steps leading to this separation in order to serve as a tutorial for separating principles in reverse mathematics.

scholarly journals COMPARING THE STRENGTH OF DIAGONALLY NONRECURSIVE FUNCTIONS IN THE ABSENCE OF INDUCTION

2015 ◽  
Vol 80 (4) ◽  
pp. 1211-1235 ◽  
Author(s):  
FRANÇOIS G. DORAIS ◽  
JEFFRY L. HIRST ◽  
PAUL SHAFER
Keyword(s):  
Image Position ◽  
Weak König’S Lemma ◽  
König’S Lemma

AbstractWe prove that the statement “there is aksuch that for everyfthere is ak-bounded diagonally nonrecursive function relative tof” does not imply weak König’s lemma over${\rm{RC}}{{\rm{A}}_0} + {\rm{B\Sigma }}_2^0$. This answers a question posed by Simpson. A recursion-theoretic consequence is that the classic fact that everyk-bounded diagonally nonrecursive function computes a 2-bounded diagonally nonrecursive function may fail in the absence of${\rm{I\Sigma }}_2^0$.

Relative constructivity

1998 ◽  
Vol 63 (4) ◽  
pp. 1218-1238 ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Numerical Analysis ◽  
Approximation Theory ◽  
Free Choice ◽  
Functional Interpretation ◽  
Uniform Bounds ◽  
Free Variables ◽  
Image Position ◽  
Definable Functions ◽  
Classical Arithmetic

In a previous paper [13] we introduced a hierarchy (GnAω)n∈ℕ of subsystems of classical arithmetic in all finite types where the growth of definable functions of GnAω corresponds to the well-known Grzegorczyk hierarchy. Let AC-qf denote the schema of quantifier-free choice.[11], [13], [8] and [7] study various analytical principles Γ in the context of the theories GnAω + AC-qf (mainly for n = 2) and use proof-theoretic tools like, e.g., monotone functional interpretation (which was introduced in [12]) to determine their impact on the growth of uniform bounds Φ such thatwhich are extractable from given proofs (based on these principles Γ) of sentencesHere A0(u, k, v, w) is quantifier-free and contains only u, k, v, w as free variables; t is a closed term and ≤p is defined pointwise. The term ‘uniform bound’ refers to the fact that Φ does not depend on v ≤ptuk (see [12] for the relevance of such uniform bounds in numerical analysis and for concrete applications to approximation theory).

scholarly journals The Brouwer invariance theorems in reverse mathematics

2020 ◽  
Vol 8 ◽  
Author(s):  
Takayuki Kihara
Keyword(s):  
Reverse Mathematics ◽  
Base System ◽  
Open Problems ◽  
Explicit Algorithm ◽  
Topological Embedding ◽  
Weak König’S Lemma ◽  
König’S Lemma

Abstract In [12], John Stillwell wrote, ‘finding the exact strength of the Brouwer invariance theorems seems to me one of the most interesting open problems in reverse mathematics.’ In this article, we solve Stillwell’s problem by showing that (some forms of) the Brouwer invariance theorems are equivalent to the weak König’s lemma over the base system ${\sf RCA}_0$ . In particular, there exists an explicit algorithm which, whenever the weak König’s lemma is false, constructs a topological embedding of $\mathbb {R}^4$ into $\mathbb {R}^3$ .

scholarly journals Reverse mathematics and a Ramsey-type König's Lemma

2012 ◽  
Vol 77 (4) ◽  
pp. 1272-1280 ◽  
Author(s):  
Stephen Flood
Keyword(s):  
Reverse Mathematics ◽  
Ramsey's Theorem ◽  
Weak Regularity ◽  
Ramsey’S Theorem ◽  
Ramsey Type ◽  
Weak König’S Lemma ◽  
König’S Lemma

AbstractIn 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.

scholarly journals The Computational Strength of Extensions of Weak König’s Lemma

1998 ◽  
Vol 5 (41) ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Natural Number ◽  
Arbitrary Function ◽  
The Other ◽  
Binary Trees ◽  
Subsequent Paper ◽  
Bounded Functions ◽  
The One ◽  
Weak König’S Lemma ◽  
König’S Lemma

The weak König's lemma WKL is of crucial significance in the study of fragments of mathematics which on the one hand are mathematically strong but on the other hand have a low proof-theoretic and computational strength. In addition to the restriction to binary trees (or equivalently bounded trees), WKL<br />is also `weak' in that the tree predicate is quantifier-free. Whereas in general the computational and proof-theoretic strength increases when logically more complex trees are allowed, we show that this is not the case for trees which are<br />given by formulas in a class Phi where we allow an arbitrary function quantifier prefix over bounded functions in front of a Pi^0_1-formula. This results in a schema Phi-WKL.<br />Another way of looking at WKL is via its equivalence to the principle<br /> For all x there exists y<=1 for all z A0(x; y; z) -> there exists f <= lambda x.1 for all x, z A0(x, fx, z);<br />where A0 is a quantifier-free formula (x, y, z are natural number variables). <br /> We generalize this to Phi-formulas as well and allow function quantifiers `there exists g <= s'<br />instead of `there exists y <= 1', where g <= s is defined pointwise. The resulting schema is called Phi-b-AC^0,1.<br />In the absence of functional parameters (so in particular in a second order context), the corresponding versions of Phi-WKL and Phi-b-AC^0,1 turn out to<br />be equivalent to WKL. This changes completely in the presence of functional<br />variables of type 2 where we get proper hierarchies of principles Phi_n-WKL and<br />Phi_n-b-AC^0,1. Variables of type 2 however are necessary for a direct representation<br />of analytical objects and - sometimes - for a faithful representation of<br />such objects at all as we will show in a subsequent paper. By a reduction of<br />Phi-WKL and Phi-b-AC^0,1 to a non-standard axiom F (introduced in a previous paper) and a new elimination result for F relative to various fragment of arithmetic in all finite types, we prove that Phi-WKL and Phi-b-AC^0,1 do<br />neither contribute to the provably recursive functionals of these fragments nor to their proof-theoretic strength. In a subsequent paper we will illustrate the greater mathematical strength of these principles (compared to WKL).

scholarly journals Comparing DNR and WWKL

2004 ◽  
Vol 69 (4) ◽  
pp. 1089-1104 ◽  
Author(s):  
Klaus Ambos-Spies ◽  
Bjørn Kjos-Hanssen ◽  
Steffen Lempp ◽  
Theodore A. Slaman
Keyword(s):  
Reverse Mathematics ◽  
Axiom System ◽  
Recursive Functions ◽  
Weak König’S Lemma ◽  
König’S Lemma

Abstract.In Reverse Mathematics, the axiom system DNR. asserting the existence of diagonally non-recursive functions, is strictly weaker than WWKL0 (weak weak König's Lemma).

Sign in / Sign up

Export Citation Format

Share Document