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
2 votes
0 answers
66 views

Reverse mathematics on lightface $\Pi^1_1$-uniformization for unary relation

It is known that the following form of $\Pi^1_1$-uniformization is equivalent to $\Pi^1_1$-Comprehension over $\mathsf{ATR}_0$ (cf. VI.2.6 of Simpson's book) : (Kondo's uniformization theorem) For ...
Hanul Jeon's user avatar
  • 2,774
3 votes
1 answer
106 views

Kleene normal form theorem for r.e. relations proven in arithmetical theories

After reading the relevant chapters of Classical Recursion Theory (freely available from here), I have the following questions concerning Theorem II.1.10 (Normal form theorem) and Theorem IV.1.9 (...
CBuch's user avatar
  • 31
3 votes
0 answers
176 views

Reverse-mathematical strength of Banach-Tarski

What is the reverse mathematical strength of the Banach-Tarski paradox? The usual proof of Banach-Tarski should carry out in $\mathrm{ZF}+\mathrm{AC}_\kappa$, where $\kappa$ is the supremum of the ...
C7X's user avatar
  • 1,176
7 votes
1 answer
307 views

Proving finiteness in Reverse Mathematics

In (second-order) Reverse Mathematics, a (code for an) open set $U\subset \mathbb{R}$ is given by two sequences of rationals $(a_n)_{n \in \mathbb{N}}, (b_n)_{n \in \mathbb{N}}$. The idea is that $U$ ...
Sam Sanders's user avatar
  • 3,901
12 votes
2 answers
396 views

Trading Choice for Comprehension (or Replacement)

This question is basically a request for clarification about a remark made by Sam Sanders in a comment to another question: IIUC what he's saying, there are statements that can be proved either with a ...
Gro-Tsen's user avatar
  • 29.8k
7 votes
1 answer
415 views

Proof of global Peano existence theorem in ZF?

By global Peano existence theorem I mean the existence of a maximal interval of solution of a first order ODE $x'=f(x,t)$ with continuous $f$. The proofs of the global Peano Theorem found in the ...
Mikhail Katz's user avatar
  • 15.1k
10 votes
1 answer
219 views

How much of second-order arithmetic do you need for $\mathbf{\Sigma}^1_1$-determinacy to give you countable transitive models of $\mathsf{ZFC}$?

This is in some sense a follow-up to this question. The answer there says that over $\mathsf{Z}_2$ (second-order arithmetic), (boldface) $\mathbf{\Sigma}^1_1$-determinacy is enough to entail the ...
James Hanson's user avatar
  • 10.3k
7 votes
1 answer
293 views

Strength of Borel determinacy

In this blog post by Gowers on Borel determinacy, Andres Caicedo says the following in a comment (slightly rephrased). Let $\mathsf{ZFC^-}$ be $\mathsf{ZFC}$ without power set and $\mathsf{ZC^-}$ be $...
new account's user avatar
18 votes
2 answers
1k views

What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?

There have been a couple of recent questions, here and here, regarding the role of the axiom of choice in real-analytic results with applicability to general relativity. This lead me to look at some ...
James Hanson's user avatar
  • 10.3k
9 votes
1 answer
447 views

Is "All hyperreal fields $C(\mathbb{R})/M$ are isomorphic" independent of ZFC+$\lnot$CH?

We work in ZFC. Let $C(X)$ be the ring of continuous functions $f:X\to\mathbb{R}$, and $M$ a maximal ideal. We call $C(X)/M$ a hyperreal field if it's not isomorphic to $\mathbb{R}$. A field $E$ is ...
Jakobian's user avatar
  • 715
4 votes
0 answers
103 views

Coding fourth-order objects in second-order Reverse Mathematics

Reverse Mathematics (RM for short) generally takes place in the language of second-order arithmetic. Thus, higher-order objects need to be "coded" or "represented" indirectly. ...
Sam Sanders's user avatar
  • 3,901
13 votes
1 answer
445 views

How much determinacy do you need for second order arithmetic to be as strong as ZFC?

From Wikipedia (I couldn't find the original source): $\text{ZFC} + \{\text{there are $n$ Woodin cardinals: $n$ is a natural number}\}$ is conservative over $\text{Z}_2$ with projective determinacy. ...
Christopher King's user avatar
5 votes
0 answers
91 views

Entailment in one-point extensions of standard-enough models

This is one of two questions about the power of "one-point extensions" in reverse mathematics. This one focuses on what separations can be achieved as one-point extensions of as-closed-as-...
Noah Schweber's user avatar
8 votes
0 answers
136 views

How strong is exponentiation with only open induction? (Or: "how low can we go?")

Do the strongest theories currently known to be unconstrained by Tennenbaum's theorem ($IOpen$ and some modest extensions) remain so when augmented with a definition of exponentiation and axiom $\...
Robin Saunders's user avatar
3 votes
0 answers
88 views

Logical strength of the pigeon-hole principle for measure spaces

In his book on measure theory, Tao discuss the pigeon-hole principle for measure spaces, which expresses that the union of measure zero sets is again measure zero. I am interested in the logical ...
Sam Sanders's user avatar
  • 3,901
13 votes
1 answer
521 views

Set-theoretical reverse mathematics of the reals

While reading through a nice old question/answer about the behavior of measures on the reals in $ZFC$ that popped back up today, I began to wonder how much of $ZFC$ is required for various things we ...
Alec Rhea's user avatar
  • 8,947
7 votes
0 answers
307 views

What is the strongest form of the Axiom of Choice available in $\mathsf{Z}_{2}$?

$\mathsf{Z}_{2}$ denotes second-order arithmetic. Some forms of AC are expressible in $\mathsf{Z}_{2}$; for example the $\mathsf{\Sigma}_{1}^{1}$ axiom of choice is part of the theory $\mathsf{ATR}_{0}...
Victor's user avatar
  • 2,076
4 votes
0 answers
247 views

What is the meaning and proof of Harvey Friedman’s ultrafinite incompleteness sentence?

On page 7 of his paper “Adventures in Incompleteness”, Harvey Friedman states the following: IN ANY LONG ENOUGH SEQUENCE $x_1,...,x_n$ FROM $\{1,2,3\}$, SOME $(x_i,...,x_{2i})$ IS A SUBSEQUENCE OF ...
Keshav Srinivasan's user avatar
7 votes
0 answers
157 views

Is the IVT internally true in Johnstone's topological topos?

By IVT, I mean that for any continuous function $f:[0,1]\to\mathbb R$ for which $f(0)\leq 0 \leq f(1)$, there is a $t \in [0,1]$ for which $f(t)=0$. I don't mean any "constructive" ...
wlad's user avatar
  • 4,792
6 votes
1 answer
223 views

Does $\text{ACA}_0$ + True Arithmetic prove the well-foundedness of every recursive ordinal?

As discussed in Noah Schweber's answer to What is the proof-theoretic ordinal of true arithmetic?, it is somewhat ambiguous what “the proof-theoretic ordinal of True Arithmetic” might mean. In one ...
Keshav Srinivasan's user avatar
12 votes
2 answers
569 views

Is the Intermediate Value Theorem strictly stronger than LLPO?

(The context is Intuitionistic ZF set theory, or HoTT, or the internal logic of a topos with a Natural Number Object. The real numbers here mean the Dedekind reals.) By LLPO, I mean the statement that ...
wlad's user avatar
  • 4,792
7 votes
2 answers
454 views

What is the strength of “if $c≥0$ then $[0,c] = c·[0,1]$” in constructive math (w.r.t., LPO, WLPO, LLPO, etc.)?

Context: This question is about constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF. (I wish to avoid the axiom of countable choice if possible, ...
Gro-Tsen's user avatar
  • 29.8k
14 votes
2 answers
1k views

When more is less in logic

I am looking for examples of theorems where adding a 'trivial' extra condition makes the theorem provable in weaker systems. By 'trivial' I mean that the extra condition is trivial in strong enough ...
Sam Sanders's user avatar
  • 3,901
6 votes
0 answers
112 views

Reverse mathematics of Banach-Mazur games

Given $\mathcal{A}\subseteq\omega^\omega$, the Banach-Mazur game with payoff set $\mathcal{A}$ consists of players $1$ and $2$ alternately playing nonempty finite strings of naturals with player $1$ ...
Noah Schweber's user avatar
2 votes
0 answers
100 views

Enumerating unions of arithmetical sets

In Simpsons's excellent Subsystems of Second-order Arithmetic, we find V.4.10 which tells us the following: The following is provable in ATR$_0$. Let $(A_n)_{n\in \mathbb{N}}$ be a sequence of ...
Sam Sanders's user avatar
  • 3,901
13 votes
1 answer
404 views

"At most one" versus "at most finitely many"

As shown in Simpson's excellent Subsystems of Second Order Arithmetic, the ‘big five’ system ATR$_0$ from second-order reverse mathematics is equivalent to the following principle: For arithmetical $\...
Sam Sanders's user avatar
  • 3,901
3 votes
1 answer
121 views

Equivalences between statements of (seemingly) different order

In Steve Simpson's excellent monograph SOSOA, we find Theorem X.4.4 which contains an equivalence (over RCA$_0^*$) between the following statements: The induction axiom for $\Sigma_1^0$-formulas (...
Sam Sanders's user avatar
  • 3,901
1 vote
0 answers
78 views

Doing reverse mathematics by regarding modal logic as weak first-order logic

Reverse mathematics seeks to find subsystems of second-order logic that are equivalent to certain mathematics theorems, say over $\mathsf{RCA}_0$. Modal logic can be regarded as a weak version of ...
Colin Tan's user avatar
  • 251
20 votes
1 answer
567 views

Is Monsky's theorem provable in $\mathsf{RCA}_0$?

Monsky's theorem states that it is not possible to dissect a square into an odd number of triangles of equal area. Monsky's proof attracted attention in part because it unexpectedly made use of the ...
Timothy Chow's user avatar
5 votes
2 answers
217 views

How does one prove the consistency of $\mathrm{PA}$ in $\mathrm{Z_2}$?

It is "well-known" (e.g. stated here without proof and sketched here) that $\mathrm{Z_2}$ proves $\mathrm{Con(PA)}$ using the "usual" model-theoretic proof, that is one can build a ...
cody's user avatar
  • 1,080
0 votes
0 answers
248 views

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

The question is in the title. Szemerédi'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 ...
Thomas Benjamin's user avatar
2 votes
0 answers
58 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 ...
Sam Sanders's user avatar
  • 3,901
8 votes
2 answers
479 views

Comprehension axiom that 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{...
Jiayi Liu's user avatar
  • 909
2 votes
1 answer
378 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 ...
Thomas Benjamin's user avatar
9 votes
2 answers
285 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,...
Sam Sanders's user avatar
  • 3,901
3 votes
0 answers
318 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}$, ...
Sam Sanders's user avatar
  • 3,901
4 votes
1 answer
346 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 ...
user21820's user avatar
  • 2,734
9 votes
0 answers
283 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 ...
Sam Sanders's user avatar
  • 3,901
8 votes
3 answers
265 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 ...
peterEller's user avatar
3 votes
0 answers
154 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[ ...
Jordan Mitchell Barrett's user avatar
2 votes
1 answer
191 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 \...
Jordan Mitchell Barrett's user avatar
1 vote
0 answers
135 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 ...
Jordan Mitchell Barrett's user avatar
7 votes
1 answer
288 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 ...
Dan Turetsky's user avatar
  • 2,678
11 votes
1 answer
378 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 ...
Keshav Srinivasan's user avatar
8 votes
1 answer
263 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 \...
Corey Bacal Switzer's user avatar
3 votes
1 answer
1k 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 ...
Sam Sanders's user avatar
  • 3,901
5 votes
1 answer
317 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 ...
Sam Sanders's user avatar
  • 3,901
9 votes
0 answers
184 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 ...
Sam Sanders's user avatar
  • 3,901
8 votes
1 answer
442 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 ...
Keshav Srinivasan's user avatar
8 votes
1 answer
373 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}$ ...
Keshav Srinivasan's user avatar