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).
166
questions
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 ...
- 5,461
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[ ...
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 \...
60
votes
8
answers
9k
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 ...
- 19.1k
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 ...
11
votes
1
answer
379
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 ...
- 19.1k
8
votes
2
answers
864
views
What is the status of Cantor-Schroder-Bernstein in Reverse Math?
I'd like to know which of the set theories in SOSOA prove what versions of Cantor-Schroder-Bernstein? For my own purposes I can use arbitrarily high quantifier complexity, but I wonder how little ...
- 3,969
8
votes
1
answer
264
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 \...
- 60.2k
3
votes
1
answer
2k
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 ...
- 2,678
11
votes
3
answers
1k
views
New research on coding in reverse mathematics?
Coding is obviously a fundamental tool in reverse mathematics, and practitioners take care to both demonstrate the correctness of their coding mechanisms and point out their limitations. Harvey ...
- 3,969
9
votes
1
answer
693
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 ...
- 33.9k
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 ...
- 3,969
10
votes
0
answers
270
views
Strength of claims about extensions of partial preorders and orders to linear ones
Consider these two axioms:
Every partial order extends to a linear order.
Every partial preorder (reflexive and transitive relation) extends to a linear preorder while preserving strict orderings: i....
- 2,383
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 ...
- 3,969
8
votes
1
answer
374
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}$ ...
- 60.2k
10
votes
1
answer
487
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 ...
CommunityBot
- 1
6
votes
2
answers
739
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 ...
- 4,843
12
votes
1
answer
456
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 ...
- 19.1k
2
votes
1
answer
181
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$...
- 19.1k
1
vote
2
answers
259
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 ...
- 19.1k
7
votes
1
answer
380
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 ...
- 43.7k
7
votes
0
answers
307
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 ...
- 6,102
17
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 + \...
- 51.6k
5
votes
0
answers
237
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 ...
- 4,843
5
votes
1
answer
551
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 ...
- 4,843
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 ...
- 2,090
4
votes
0
answers
252
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 ...
- 19.1k
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"...
- 4,843
5
votes
1
answer
332
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.
...
- 9,603
6
votes
2
answers
689
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 ...
- 225k
14
votes
0
answers
595
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 ...
CommunityBot
- 1
14
votes
4
answers
3k
views
"Family Tree" of Theorems
Is anyone aware of any attempt to describe the dependencies of theorems (perhaps in mathematics generally, perhaps in some limited areas) in the form of a "family tree"? That is, each node on the ...
13
votes
1
answer
580
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 ...
- 19.1k
5
votes
0
answers
144
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 ...
- 2,090
6
votes
1
answer
286
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 ...
- 7,125
3
votes
0
answers
257
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 ...
- 578
3
votes
1
answer
110
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$. ...
- 17.1k
4
votes
0
answers
165
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. ...
- 19.1k
10
votes
2
answers
787
views
Proof complexity of two directions of equivalency?
This question is not precise, but I believe has a precise formulation.
Consider a mathematical theorem which gives an equivalency between two conditions. As an extreme example:
Theorem.
A ...
- 255
12
votes
1
answer
966
views
What is known about the reverse mathematics of algebraic number fields?
I know work on the reverse mathematics of countable algebraic field extensions including Galois theory, notably including Dorais, Hirst, and Shafer http://arxiv.org/pdf/1209.4944v2.pdf. But algebraic ...
- 10.8k
2
votes
0
answers
78
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 ...
CommunityBot
- 1
5
votes
1
answer
290
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 ...
- 7,654
3
votes
2
answers
738
views
Is any Cauchy sequence for completion of rational semicomputable?
For the definition of a semicomputable real, see An Introduction to Kolmogorov Complexity and its Applications by Li and Vitanyi (1997). In fact, it is not true that every Cauchy sequence for ...
- 60.2k
6
votes
1
answer
271
views
Bounded-width Konig's lemma in reverse math
We define $\mathsf{BWKL}$ as follows:
Every infinite binary tree of bounded width has an infinite path.
This obviously follows from $\mathsf{WKL}$. Is this principle true in $\mathsf{RCA}_0$? If not, ...
- 256
2
votes
1
answer
307
views
Is there a model of ZF+ACC where transfer fails for the definable hyperreals?
In 2003 Kanovei and Shelah constructed a definable hyperreal field. The ultrapower used exploits a fairly large index set so that it is clear that the usual proof of Los and transfer does not go ...
- 15.1k
7
votes
1
answer
329
views
Axiomatizations of arithmetical parts of theories
For common theories that talk about something more general than first-order arithmetic (e.g. set theories and subsystems of second-order arithmetic), are there nice axiomatizations of their arithmetic ...
- 43.7k
1
vote
1
answer
315
views
How does $RCA_0$ achieve weak completeness?
Few days ago I asked about $WKL_0$ and the role of binary trees to provide for completeness for first order theories, and the question was nicely answered by Joel David Hamkins: Does $WKL_0$ plus CON(...
- 52.4k
2
votes
1
answer
139
views
Does $WKL_0$ plus CON(PA+X) give a binary tree model of PA+X?
In the context of reverse mathematics $WKL_0$ is considered equivalent to Gödel's completeness theorem over $RCA_0$. Does this mean that e.g. $WKL_0$ plus the consistency statement CON(PA+X) gives a ...
- 225k
21
votes
6
answers
2k
views
Consistency strength needed for applied mathematics
Given that we can never proof the consistency of a theory for the foundations of mathematics in a weaker system, one could seriously doubt whether any of the commonly used foundational frameworks (ZFC ...
CommunityBot
- 1
1
vote
2
answers
1k
views
Can Goodstein's theorem been proven with first order PA + Constructive Omega Rule?
I am trying to understand transfinite induction and Gentzen's theories.
But I was wondering, if there is any connection with the Constructive Omega Rule (COR).
With COR I mean that if you can proof:
...
CommunityBot
- 1