91 votes
Accepted
What does it mean to suspect that two conjectures are logically equivalent?
First of all, in practice when we say "Conjecture A is equivalent to Conjecture B," what we mean is "We have a proof that Conjecture A is true iff Conjecture B is true." We can have such a proof ...
71 votes
What does it mean to suspect that two conjectures are logically equivalent?
Noah Schweber's answer is in some sense the "right" answer, and I would have said something similar if he hadn't beaten me to it. However, I think that it's worth pointing out that reverse ...
47 votes
What does it mean to suspect that two conjectures are logically equivalent?
One way to say rigorously what it means for two true theorems to be equivalent is to find a meaningful way to generalize both of them to statements that aren't always true, and then prove that they're ...
34 votes
Accepted
What is known about the relationship between Fermat's last theorem and Peano Arithmetic?
The main reference for this topic is Angus Macintyre's appendix to Chapter 1 ("The Impact of Gödel's Incompleteness Theorems on Mathematics") of Kurt Gödel and the Foundations of ...
23 votes
What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?
$\text{ZF}+ \text{AC}_{\omega}$ is not $\Sigma^1_4$-conservative over ZF and ZF + DC is not $\Sigma^1_4$-conservative over $\text{ZF}+ \text{AC}_{\omega}.$ An example of the former: the sentence $\...
21 votes
Accepted
Why is weak Kőnig's lemma weaker than Kőnig's lemma?
The issue is that for a finitely branching subtree $T$ of $\omega^{<\omega}$, the function $f$ mapping $\sigma$ to the greatest $n$ such that the concatenation $\sigma ^\frown n$ is in $T$ may not ...
17 votes
Accepted
Reverse mathematics of Cousin's lemma
Sam Sanders here, one of the authors of the paper you mention. Thanks for the nice words. I will answer your questions based on my personal opinion. You write: [...] would like to know if it ...
16 votes
How to understand the interface of the consistency strength hierarchy, reverse mathematics, and proof-theoretic ordinal analysis?
Sorry this is a bit disjointed - there's a lot of stuff here. I hope this helps though. All of these notions are applicable in all contexts - or at least, all sufficiently rich contexts (we probably ...
15 votes
Accepted
van der Waerden's theorem in Reverse Mathematics
There is a powerful combinatorial theorem, known as the Hales–Jewett theorem, which readily implies van der Waerden's theorem. On the other hand, the paper below by Matet exhibits primitive recursive ...
15 votes
Accepted
Is "All hyperreal fields $C(\mathbb{R})/M$ are isomorphic" independent of ZFC?
In On ultra powers of Boolean algebras (Topology Proceedings 9 (1984) 269-291) Alan Dow proved (Corollary 2.3) that $\neg\mathsf{CH}$ implies there are two fields of the form $C(\mathbb{N})/M$ that ...
14 votes
Accepted
Is it possible to constructively prove that every quaternion has a square root?
Reduction to LLPO (Lesser Limited Principle of Omniscience). The statement LLPO is the following (from Wikipedia): For any sequence a0, a1, ... such that each ai is either 0 or 1, and such that at ...
14 votes
Are key theorems finitistically reducible?
There are various problems with finitistic reducibility as Simpson develops it; for a survey, see §5.3 of my Stanford Encyclopedia of Philosophy entry on reverse mathematics. I tend to agree that the ...
13 votes
Accepted
How much determinacy do you need for second order arithmetic to be as strong as ZFC?
Because ZFC proves soundness of $\text{Z}_2$, no consistent finite extension of $\text{Z}_2$ proves all second order arithmetic statements that are provable in ZFC (for example, the statement "...
12 votes
Is Monsky's theorem provable in $\mathsf{RCA}_0$?
This isn't an answer to your question because I have no idea whether this argument can be carried out in $RCA_0$, but this fact doesn't appear to be mentioned anywhere easily accessible through ...
12 votes
Accepted
Set-theoretical reverse mathematics of the reals
TL;DR: A most basic property of $\mathbb{R}$ is that it is not countable, which is surprisingly hard to prove (namely far beyond the Big Five you mention), as explored in [1, 2, 3]. The longer version....
11 votes
Accepted
Cases where multiple induction steps are provably required
Here is a reference for one way of making precise sense of your question and answering it: Stefan Hetzl and Tin Lok Wong (2017): "Some observations on the logical foundations of inductive theorem ...
11 votes
What does it mean to suspect that two conjectures are logically equivalent?
As has been said Timothy Chow's answer and the comments, what mathematicians really mean when they use "equivalent" in this setting is that it's easy to prove the equivalence. That's not the same as ...
11 votes
Accepted
What subsystem of second-order arithmetic is needed for the recursion theorem?
As Wojowu already pointed out $\mathsf{RCA}_0$ proves recursion theorem. You could find a proof in Simpson's book [1], Section II.3. In fact primitive recursion theorem is equivalent to $\Sigma^0_1\...
11 votes
Accepted
Reverse Mathematics strength of fixed radius covering theorem
The statement in provable in $\mathrm{WKL}_0$. Consider the following proof. Fix $k>1/\epsilon$, let $I=\{i<k:E\cap[i/k,(i+1)/k]\ne\varnothing\}$, and let $\{x_i:i\in I\}$ be such that $x_i\in E\...
11 votes
What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?
This is sort of an anti-answer, which I've accordingly made CW, but here goes: Whether $\mathsf{ZFC}$ is projectively conservative over $\mathsf{ZF}$ seems open; see Joel's answer from a while ago (...
Community wiki
10 votes
Accepted
Are all generalized Scott sets realized as generalized standard systems?
The question has a positive answer, not only when $M$ is a model of $PA$, but even when $M$ is a model of the fragment $I\Sigma_1$ of $PA$. The positive answer alluded to above follows from Tanaka's ...
10 votes
Why is weak Kőnig's lemma weaker than Kőnig's lemma?
Interestingly, even Kőnig's lemma restricted to subtrees of $\omega^\omega$ for which every node has at most two children is equivalent to the full Kőnig's lemma, not weak Kőnig's lemma. This is ...
10 votes
Accepted
BISH: If a function is pointwise positive, is its infimum positive?
In BISH the follwoing two statements are equivalent: (i) If $f:[0,1] \to \{y\in\mathbb R\, | \,y>0\}$ is uniformly continuous, then there is $n\in\mathbb N$ such that $\forall x \in [0,1]\ [f(x)&...
10 votes
Accepted
Comprehension axiom that helps in the opposite direction
David Belanger's work is relevant. The principle $\mathsf{WKL_0}$ (= "Every infinite subtree of $2^{<\omega}$ has an infinite path") is not literally a comprehension principle, so its ...
10 votes
Accepted
Strength of Borel determinacy
I don't know why you would want to work with $\mathrm{ZC}^{-}$, this is not a theory I would recommend to do math in. But as long as you only care about second order number theory, there is really no ...
10 votes
Accepted
Mathematical strength of the statement "Heyting Arithmetic admits Markov's rule"
$\def\ha{\mathsf{HA}}\def\down{{\downarrow}}\def\mr{\mathrel{\mathbf r}}$I believe this can be proved in a fairly weak fragment of arithmetic, such as $\mathsf{I\Delta_0+EXP}$, possibly even in a ...
10 votes
Accepted
$\mathit{RCA}_0$ without the law of the excluded middle
To work in constructive reverse mathematics, we typically switch to a system of arithmetic based on functions instead of systems based on sets. In this approach, instead of the second-order universe ...
9 votes
Reverse Mathematics strength of fixed radius covering theorem
Let me strengthen Emil's excellent answer to a finer reverse mathematical result. Recall that $\mathsf{RCA}_0^\star=\mathsf{EA}+\mathsf{I}\Delta^0_1+\Delta^0_1\textsf{-CA}$ and $\mathsf{WKL}_0^\star=\...
8 votes
Accepted
Proof-theoretic ordinals: inevitable consistency?
The ineventable consistency ordinals do not exist for all the computably axiomatizable extensions of $\mathsf{RCA}_0$. Indeed, for any given notation system $\alpha$ I'll construct a notation system $\...
8 votes
Why restrict to $\Sigma_1^0$ formulas in $RCA_0$ induction?
Roughly speaking, the choice of $\Sigma^0_1$ induction is a balance between (1) having enough induction to make most proofs straightforward and (2) keeping the first-order part of the theory simple. ...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
reverse-math × 193lo.logic × 157
computability-theory × 41
proof-theory × 29
set-theory × 27
theories-of-arithmetic × 25
constructive-mathematics × 20
reference-request × 18
descriptive-set-theory × 13
model-theory × 11
foundations × 11
axiom-of-choice × 10
real-analysis × 7
soft-question × 7
mathematical-philosophy × 6
ordinal-analysis × 6
nt.number-theory × 5
nonstandard-analysis × 5
metamathematics × 5
co.combinatorics × 4
gn.general-topology × 4
computational-complexity × 4
measure-theory × 3
large-cardinals × 3
ag.algebraic-geometry × 2