Questions tagged [reverse-math]

The general enterprise of calibrating the strength of classical mathematical theorems in terms of the axioms, typically of set existence, needed to prove them; originated in its modern form in the 1970s by H. Friedman and S. G. Simpson (see R.A. Shore, "Reverse Mathematics: The Playground of Logic", 2010).

Filter by
Sorted by
Tagged with
0 votes
0 answers
62 views

What is the weakest subsystem of Second-order Arithmetic (or its first-order part) that proves Szemeredi's Regularity Lemma?

The question is in the title. Szemeredi's Regularity Lemma is the following (according to the Wikipedia entry): For every $\epsilon$ $\gt$ 0 and positive integer $m$ there exists an integer $M$ such ...
user avatar
2 votes
0 answers
50 views

Weaker uniformisation theorems

An interesting topic in Reverse Mathematics is uniformisation theorems (see VI.2 and VII.6 in Simpson's SOSOA). Now, these theorems all express the following: for a suitable formula $\varphi$, there ...
user avatar
  • 1,879
8 votes
2 answers
391 views

Comprehension axiom who helps in the opposite direction

Usually, having more comprehension axiom means the more you can prove. We wonder if the converse can be the case. Is there a natural problem $\mathsf{P}$ so that $\mathsf{P}+\neg(\Gamma-\mathsf{...
user avatar
  • 909
2 votes
1 answer
348 views

Two questions regarding the reverse mathematics of Siegel's lemma

In a short proof of the Roth theorem regarding the rational approximation of algebraic reals I found online (which made use of Siegel's Lemma), it was stated that "Siegel's lemma is a corollary ...
user avatar
8 votes
2 answers
255 views

Reverse Mathematics strength of fixed radius covering theorem

I am curious about the reverse math status of the below statement. Note that we work in second-order RM, i.e. 'closed set' is interpreted as in Simpson's excellent SOSOA. For any closed $E\subset [0,...
user avatar
  • 1,879
3 votes
0 answers
293 views

Different definitions of 'countable set'

There are a number of different definitions of 'countable set', all equivalent given a strong enough (classical) system. The obvious ones (injection to $\mathbb{N}$, bijection to $\mathbb{N}$, ...
user avatar
  • 1,879
3 votes
1 answer
284 views

Does ACA prove categoricity of the reals?

$\def\f#1{\text{#1}}$Does $\f{ACA}$ prove that any two internally complete ordered fields are isomorphic? Here internal completeness is expressed roughly as "every sequence of reals with an upper ...
user avatar
  • 2,649
9 votes
0 answers
239 views

Coding third-order objects via second-order ones

As is well-known, the language of second-order arithmetic only has variables for natural numbers and sets of natural numbers. Higher-order objects, like functions on $\mathbb{R}$, have to be ...
user avatar
  • 1,879
8 votes
3 answers
232 views

Relationship between provable in $RCA_0$ and effectively true

Question: What is the relationship between provability in $RCA_0$ and effectively true? In other words: Given a problem, if a statement asserting the existence of a solution of the problem is provable ...
user avatar
3 votes
0 answers
139 views

Is anything known about $\Delta_n$ bounding?

For a class $\Gamma \in \{ \Sigma_n, \Pi_n, \Delta_n \}$ in the arithmetical hierarchy, we can consider the induction, bounding, and least number principles for $\Gamma$: $\mathsf{I}\Gamma$ is $\big[ ...
user avatar
1 vote
1 answer
158 views

Can $\mathsf{RCA}_0$ prove that every nonempty c.e. set $A \subseteq \mathbb{N}$ has a least element?

In other words, can $\mathsf{RCA}_0$ prove that for every function $f\colon \mathbb{N} \to \mathbb{N}$, there is $b \in \mathbb{N}$ such that $$ \exists k \in \mathbb{N},\ f(k) = b\quad \land\quad \...
user avatar
1 vote
0 answers
117 views

Why doesn't $\mathsf{B}\Sigma_2$ hold in $\mathsf{RCA}_0$?

For a formula $\varphi(i,u)$ of arithmetic, the bounding principle for $\varphi$ is the statement $$\forall m \, \Big( \big( \forall i<m\ \exists u\ \varphi(i,u) \big) \to \big( \exists v\ \forall ...
user avatar
7 votes
1 answer
217 views

Independence of $\Pi^1_1$-induction from ATR$_0$

Is it known that $\Pi^1_1$-induction is independent of ATR$_0$? Simpson's book shows this for $\Pi^1_1$ transfinite induction ($\Pi^1_1$-TI), but I'm only interested in inducting on $\omega$. I can ...
user avatar
  • 2,179
10 votes
1 answer
330 views

What is the Turing degree of the monadic theory of the real line?

The monadic theory of the real line is the set of all sentences in the monadic second-order language of order which are true in $\mathbb{R}$. In this 1982 paper, Gurevich and Shelah show that true ...
user avatar
8 votes
1 answer
234 views

Paris-Harrington principles parametrized by functions $f:\mathbb N \to \mathbb N$

Recall that the Paris-Harrington Principle, $\mathsf{PH}$, is the statement that for each $e, r, k < \omega$ there is an $N < \omega$ so that given any coloring $c:[N]^e \to r$ there is an $H \...
user avatar
3 votes
1 answer
501 views

What is the strength of the second-order statement 'an uncountable closed set in $\mathbb{R}$ has a limit point'?

Perhaps surprisingly, we work in the language of second-order arithmetic. I was wondering if the strength of the following statement LP was known: An uncountable closed set in $\mathbb{R}$ has a ...
user avatar
  • 1,879
5 votes
1 answer
232 views

From Vitali to Heine-Borel in reverse mathematics

The Vitali and Heine-Borel covering theorems are house-hold names of analysis, and rightly well-studied in reverse mathematics. As shown in Simpson's excellent monograph [1], for countable coverings ...
user avatar
  • 1,879
9 votes
0 answers
145 views

Connection between second-order arithmetic and Hilbert-Bernays' Grundlagen

What is the exact (historical) connection between second-order arithmetic and Hilbert-Bernays' Grundlagen der Mathematik? Some background: the literature on Reverse Mathematics contains a number of ...
user avatar
  • 1,879
7 votes
1 answer
381 views

What subsystem of third order arithmetic proves the real numbers are Dedekind complete?

Reverse mathematics is mainly about subsystems of second-order arithmetic, but in recent years it’s expanded to cover subsystems of third-order arithmetic as well. Now the fact that the real numbers ...
user avatar
8 votes
1 answer
282 views

What subsystem of second-order arithmetic is needed for the recursion theorem?

In its simplest version, the recursion theorem states that for any $m\in\mathbb{N}$ and any function $g:\mathbb{N}\rightarrow\mathbb{N}$, there exists a function $f:\mathbb{N}\rightarrow\mathbb{N}$ ...
user avatar
17 votes
2 answers
744 views

Reverse mathematics of Cousin's lemma

This paper by Normann and Sanders apparently caused a stir in the reverse mathematics community when it came out a couple years ago. It says that Cousin's lemma, which is an extension of the Heine-...
user avatar
  • 1,107
10 votes
1 answer
338 views

How to understand the interface of the consistency strength hierarchy, reverse mathematics, and proof-theoretic ordinal analysis?

I am aware of three major "hierarchies" of mathematical theories, but I don't know how to relate these hierarchies to one another. Here are the hierarchies I have in mind: Consistency strength. My ...
user avatar
  • 49.6k
2 votes
1 answer
172 views

Detecting comprehension topologically

This question basically follows this earlier question of mine but shifting from standard systems of nonstandard models of $PA$ to $\omega$-models of $RCA_0$. For $X$ a Turing ideal we get the map $c_X$...
user avatar
6 votes
1 answer
280 views

Every complex number has a square root via LLPO without weak countable choice

Is it possible to prove that every complex number has a square root using analytic LLPO, but avoiding Weak Countable Choice or Excluded Middle? Unique Choice is allowed. (Analytic LLPO is the ...
user avatar
  • 3,370
1 vote
2 answers
242 views

The "higher topology" of countable Scott sets

Fix some computable bijection $b$ between $\omega$ and $2^{<\omega}$. For $r\in 2^\omega$, let $$[r]=\{f\in 2^\omega: \forall\sigma\prec f(b^{-1}(\sigma)\in r)\}$$ be the closed subset of Cantor ...
user avatar
7 votes
0 answers
278 views

$0^\#$ in weak theories vs large cardinals in $L$

To better understand the transition from large cardinal axioms consistent with the constructible universe $L$ to large cardinal axioms transcending $L$, I am looking for natural equiconsistencies ...
user avatar
6 votes
2 answers
632 views

Uncountability of the real numbers from LLPO without countable choice

Does there exist a proof of the uncountability of the real numbers that uses analytic LLPO (the statement that any real number $x$ satisfies either $x \leq 0$ or $x \geq 0$) but avoids Excluded Middle ...
user avatar
  • 3,370
10 votes
1 answer
430 views

Examples of proofs using induction or recursion on a big recursive ordinal

There are many proofs use induction or recursion on $\omega$, or on an arbitary (may be uncountable) ordinal. Are there some good examples of proofs which use a big but computable ordinal? The ...
user avatar
  • 445
4 votes
0 answers
216 views

An axiom that shows that the real numbers are weakly countable?

Is there a model of Intuitionistic Higher-Order Logic in which the following axiom is true? Covering Axiom: Any true statement of the form $\forall x \in A, \exists y \in B, \phi(x,y)$ gives rise to ...
user avatar
  • 3,370
5 votes
1 answer
466 views

BISH: If a function is pointwise positive, is its infimum positive?

Let $f:[0,1] \to \mathbb R$ be a uniformly continuous function such that each value of $f(x)$ is greater than zero. Is its infimum greater than zero in BISH? I believe that it is indeed the case if ...
user avatar
  • 3,370
13 votes
2 answers
2k views

Why is weak Kőnig's lemma weaker than Kőnig's lemma?

Kőnig's lemma states that any finitely-branching tree with infinitely many nodes contains an infinite path. Weak Kőnig's lemma states the same thing about binary trees. It's known that these are not ...
user avatar
3 votes
0 answers
210 views

Proof theory and subsystems of second-order arithmetic: in particular the reverse mathematics of Godel's system $T$

While doing some research on reverse mathematics, I came across the following document under the address, http://www.andrew.cmu.edu/user/avigad/Talks/survey1.pdf: Proof theory and Subsystems of ...
user avatar
20 votes
2 answers
2k views

Is it possible to constructively prove that every quaternion has a square root?

Is it possible to constructively prove that every $q \in \mathbb H$ has some $r$ such that $r^2 = q$? The difficulty here is that $q$ might be a negative scalar, in which case there might be "too many"...
user avatar
  • 3,370
4 votes
1 answer
388 views

Proof-theoretic ordinals: inevitable consistency?

There are various different notions of the proof-theoretic ordinal of a theory; most of these are "notation-dependent" in that they're only nontrivial once we restrict attention to a class of "natural"...
user avatar
5 votes
1 answer
254 views

Why restrict to $\Sigma_1^0$ formulas in $RCA_0$ induction?

I recently asked this question over on math.se, warmly welcomed by crickets. I hope it's appropriate here. I'm reading Stillwell's Reverse Mathematics, and the induction axiom was just introduced. ...
user avatar
  • 545
6 votes
2 answers
579 views

Cases where multiple induction steps are provably required

I am looking for references for theorems of the form: 1) Any proof of theorem $X$ requires $n$ applications of induction axioms and especially 2) Any proof of theorem $X$ requires $n$ nested ...
user avatar
  • 195
10 votes
0 answers
500 views

Reverse Mathematics of Euclid's theorem

Euclid's theorem that there are infinitely many prime numbers has multiple proofs, ranging from Euclid's original theorem that constructs a new prime from a finite list of such, to Euler's proof that ...
user avatar
9 votes
1 answer
627 views

van der Waerden's theorem in Reverse Mathematics

What is known about weak systems of axiomata that allow one to prove van der Waerden's theorem? van der Waerden's theorem can be used to show that there are infinitely many primes (see below). Is ...
user avatar
13 votes
1 answer
466 views

reverse mathematics of the Lebesgue measurability of analytic sets

Can the fact that all analytic sets are Lebesgue measurable be proven in $Z_2$, or in some weak subsystem such as $\Pi^1_1\text{-CA}_0$? Conversely, can certain set existence axioms be derived from ...
user avatar
  • 2,008
4 votes
3 answers
743 views

How can you formalize the metamathematics conventionally used to state Godel’s theorem?

Gödel’s incompleteness theorem states that for any sufficiently strong formal system $T$ there exists a statement $G$ such that if $T$ is consistent, then $G$ is true but not provable in $T$. But I’m ...
user avatar
4 votes
0 answers
133 views

Does comprehension for formulas in the analytical hierarchy imply comprehension for all formulas in second-order arithmetic?

The proof that all formulas of second-order arithmetic are $\Pi^1_n$ for some $n$ (i.e. can be written with a bloc of second-order quantifiers followed by an arithmetical formula) uses the axiom of ...
user avatar
  • 2,008
11 votes
2 answers
358 views

Are all generalized Scott sets realized as generalized standard systems?

Below, I've focused on PA when lots of other theories would do. If replacing PA with a different theory leads to a more answerable question, feel free to do so. The standard system of a nonstandard ...
user avatar
6 votes
1 answer
274 views

Am I counting quantifiers correctly?

I think this is right but I want to check. The theory $\mathsf{WKL}^*_0$ is conservative over EFA for $\Pi^0_2$ sentences. And the first order part of $\mathsf{WKL}^*_0$ is axiomatized by EFA plus ...
user avatar
3 votes
0 answers
214 views

Are there amenable groups without explicit Folner sets?

This is essentially a follow-up to this previous discussion on how, in the absence of choice, the "invariant mean" and "Folner set" characterizations of amenability are no longer equivalent. Recently ...
user avatar
3 votes
1 answer
101 views

If one adds an inductive subset to a model of $ACA_0$, do we always get a new model of $ACA_0$?

Suppose $(M, \mathcal X) \models ACA_0$. Recall that a subset $A \subseteq M$ is $inductive$ over $M$ if $M$ satisfies all instances of induction in the expanded language with a predicate for $A$. ...
user avatar
14 votes
1 answer
2k views

What is known about the relationship between Fermat's last theorem and Peano Arithmetic?

As far as I know, whether Fermat's Last Theorem is provable in Peano Arithmetic is an open problem. What is known about this problem? In particular, what is known about the arithmetic systems $PA + \...
user avatar
  • 4,160
4 votes
0 answers
158 views

A forcing which can build weird models of $\neg$ADS

There is a class of forcing notions I've been playing around with recently. They have a couple nice properties, and all have the same theme, but I've found them difficult to analyze beyond the basics. ...
user avatar
60 votes
8 answers
8k views

What does it mean to suspect that two conjectures are logically equivalent?

Here's a familiar conversation: Me: Do you think Conjecture A and Conjecture B are equivalent? Friend: Yes, because I think they're both true. Me: [eye roll] You know what I mean... Does there ...
user avatar
2 votes
0 answers
74 views

Is there a connection between the subsystems of second-order arithmetic and computational complexity?

The "big five subsystems of second-order arithmetic" in reverse arithmetic reveal the stratification of the structure of mathematics. What if any is the connection of these strata with complexity ...
user avatar
5 votes
1 answer
272 views

A game with boldface strength

This is a problem which has been bothering me for a while now; it doesn't seem inherently too hard, but I haven't been able to make any real headway, so I'm putting it out in the open since at this ...
user avatar