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

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 ERNA and Friedman's Reverse Mathematics

2011 ◽  
Vol 76 (2) ◽  
pp. 637-664 ◽  
Author(s):  
Sam Sanders
Keyword(s):  
Nonstandard Analysis ◽  
Reverse Mathematics ◽  
Consistency Proof ◽  
Transfer Principles ◽  
Weak König’S Lemma ◽  
König’S Lemma

AbstractElementary 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 RCA0 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 RCA0 and that transfer for universal formulas corresponds to WKL.

scholarly journals Constructing sequences one step at a time

2020 ◽  
Vol 20 (03) ◽  
pp. 2050017
Author(s):  
Henry Towsner
Keyword(s):  
Reverse Mathematics ◽  
New Method ◽  
Well Quasi Order ◽  
Thin Set ◽  
One Step ◽  
Quasi Order ◽  
Weak König’S Lemma ◽  
König’S Lemma

We propose a new method for constructing Turing ideals satisfying principles of reverse mathematics below the Chain–Antichain ([Formula: see text]) Principle. Using this method, we are able to prove several new separations in the presence of Weak König’s Lemma ([Formula: see text]), including showing that [Formula: see text] 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 [Formula: see text] and the Ascending/Descending Sequences principle, even in the presence of [Formula: see text].

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 Ekeland’s variational principle in weak and strong systems of arithmetic

2020 ◽  
Vol 26 (5) ◽  
Author(s):  
David Fernández-Duque ◽  
Paul Shafer ◽  
Keita Yokoyama
Keyword(s):  
Variational Principle ◽  
Reverse Mathematics ◽  
Continuous Functions ◽  
Ekeland’S Variational Principle ◽  
Ekeland's Variational Principle ◽  
Compact Spaces ◽  
Logical Strength ◽  
Order Arithmetic ◽  
Weak König’S Lemma ◽  
König’S Lemma

AbstractWe analyze Ekeland’s variational principle in the context of reverse mathematics. We find that that the full variational principle is equivalent to $$\Pi ^1_1\text{- }\mathsf {CA}_0$$ Π 1 1 - CA 0 , a strong theory of second-order arithmetic, while natural restrictions (e.g. to compact spaces or to continuous functions) yield statements equivalent to weak König’s lemma ($$\mathsf {WKL}_0$$ WKL 0 ) and to arithmetical comprehension ($$\mathsf {ACA}_0$$ ACA 0 ). We also find that the localized version of Ekeland’s variational principle is equivalent to $$\Pi ^1_1\text{- }\mathsf {CA}_0$$ Π 1 1 - CA 0 , even when restricted to continuous functions. This is a rare example of a statement about continuous functions having great logical strength.

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

Sign in / Sign up

Export Citation Format

Share Document