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).
173 questions
14
votes
1
answer
806
views
Are key theorems finitistically reducible?
Simpson writes on page 378 of his Subsystems of Second Order
Arithmetic:
"For example, all of the following key theorems of infinitistic
mathematics are provable in WKL$_0$ and therefore, by ...
- 16.6k
7
votes
2
answers
398
views
Numerical choice and reverse mathematics
Consider the following fragment of numerical choice in the language of second-order arithmetic:
for any arithmetical $\varphi$, we have:
$$
(\forall n\in \mathbb{N})(\exists m\in \mathbb{N})(\forall X\...
- 4,359
9
votes
0
answers
264
views
Consequences of recent claims of Ordinal Analysis of $Z_2$
Recently Toshiyasu Arai submitted "An ordinal analysis of $\Pi_{N}$-Collection" and Henry Towsner submitted "Proofs that Modify Proofs", both of which claim ordinal analysis of ...
- 161
7
votes
1
answer
224
views
Does the decomposability of $\mathbb{R}$ imply analytic LLPO?
By "BISH" I mean constructive mathematics without axiom of countable choice.
By $\mathbb{R}^f$ I mean real numbers as fundamental sequences of rational numbers and by $\mathbb{R}^d$ I mean ...
15
votes
0
answers
244
views
Natural examples of Borel surjections without right inverse
As discussed in this question, in general a Borel surjection $f:\mathbb{R}\rightarrow\mathbb{R}$ may not have a Borel right inverse, namely a $g$ such that $f\circ g=id$, although there is always a ...
- 623
4
votes
0
answers
146
views
Can one formalize the prevalence of the Big Five systems of reverse math?
Simpson's systems of second order arithmetic turn out to be five in
number; to simplify notation let's denote them A, B, C, D, E. What
seems to be an empirical observation is that most theorems in
...
- 16.6k
9
votes
2
answers
473
views
Completing half of Hilbert's program: Foundations that are conservative over Peano Arithmetic
The goal of the Hilbert program was to find a complete and consistent formalization of mathematics. Gödel's first incompleteness theorem establishes that completeness is impossible with first-order ...
- 6,353
3
votes
1
answer
170
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 ...
- 3,042
3
votes
1
answer
123
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 (...
- 31
3
votes
0
answers
203
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 ...
- 2,031
7
votes
1
answer
331
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$ ...
- 4,359
12
votes
2
answers
429
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 ...
- 32.5k
7
votes
1
answer
558
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 ...
- 16.6k
10
votes
1
answer
254
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 ...
- 12.4k
7
votes
1
answer
321
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 $...
- 867
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 ...
- 12.4k
9
votes
1
answer
586
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 ...
- 1,201
4
votes
0
answers
110
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. ...
- 4,359
13
votes
1
answer
523
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.
...
- 6,353
5
votes
0
answers
95
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-...
- 21.1k
8
votes
0
answers
156
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 $\...
- 3,612
3
votes
0
answers
107
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 ...
- 4,359
13
votes
1
answer
611
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 ...
- 10.1k
7
votes
0
answers
321
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}...
- 2,136
3
votes
0
answers
282
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 ...
- 4,587
7
votes
0
answers
168
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" ...
- 4,943
6
votes
1
answer
292
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 ...
- 4,587
12
votes
2
answers
599
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 ...
- 4,943
7
votes
2
answers
472
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, ...
- 32.5k
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 ...
- 4,359
6
votes
0
answers
117
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$ ...
- 21.1k
2
votes
0
answers
106
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 ...
- 4,359
13
votes
1
answer
454
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 $\...
- 4,359
3
votes
1
answer
129
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 (...
- 4,359
1
vote
0
answers
92
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 ...
- 331
20
votes
1
answer
612
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 ...
- 82.6k
5
votes
2
answers
238
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 ...
- 1,452
0
votes
0
answers
253
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 ...
- 6,132
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 ...
- 4,359
8
votes
2
answers
489
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{...
- 909
2
votes
1
answer
389
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 ...
- 6,132
9
votes
2
answers
294
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,...
- 4,359
3
votes
0
answers
336
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}$, ...
- 4,359
4
votes
1
answer
376
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 ...
- 2,912
9
votes
0
answers
306
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 ...
- 4,359
8
votes
3
answers
279
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 ...
- 83
3
votes
0
answers
160
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[ ...
- 788
2
votes
1
answer
198
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 \...
- 788
1
vote
0
answers
148
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 ...
- 788
8
votes
1
answer
299
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 ...
- 3,073