87
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 ...

- 20.3k

68
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 ...

- 67.1k

46
votes

### Is there a database for tracking the dependencies of mathematical theorems?

The reverse mathematics zoo, founded by Damir Dzhafarov and with recent development by Eric Astor, aims to be a database showing the relations and dependencies of mathematical theorems as described in ...

- 198k

43
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 ...

- 109k

37
votes

### Why is this new result such a big deal?

The statement in question, frequently denoted $\mathsf{RT}^2_2$ in the context of reverse mathematics, is the instance of the infinite Ramsey theorem for unordered pairs and two colors. Specifically, ...

- 42.5k

34
votes

### Is there a database for tracking the dependencies of mathematical theorems?

It's important to distinguish between two types of "dependencies."
The cleanest type of dependency is the kind that is studied in reverse mathematics: Theorem T depends on Axiom A if T is actually ...

- 67.1k

25
votes

Accepted

### What is the reverse mathematical strength of the fundamental theorem of algebra?

Tanaka and Yamazaki (in the volume Reverse Mathematics 2001, see review) show that a substantial portion of field theory can be done in the weak base theory RCA$_0$, by proving in RCA$_0$ the ...

- 23.9k

24
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 Mathematics: ...

- 67.1k

21
votes

### Is there a database for tracking the dependencies of mathematical theorems?

The Stacks Project provides an example of what you're looking for. Every definition, lemma, theorem, etc. is given a tag, and the tags are used as references in proofs. They even provide an API for ...

- 27.6k

18
votes

### Is there a database for tracking the dependencies of mathematical theorems?

Not an answer, just
a diagram from the Stacks Project, mentioned by Paul Siegel,
illustrating dependencies of "the results needed to prove Chow’s Lemma" (the Noetherian case):
&...

- 145k

18
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 ...

- 23.9k

17
votes

### Why is this new result such a big deal?

They show that $\DeclareMathOperator{\WKL}{WKL}\DeclareMathOperator{\RT}{RT}\DeclareMathOperator{\RCA}{RCA} \RT^2_2$ is $\Pi^0_3$-conservative over $\RCA_0$. Thus, there is no way that $\RT^2_2$ can ...

- 23.9k

16
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 ...

- 2,024

15
votes

### What is the reverse mathematical strength of the fundamental theorem of algebra?

Bjørn Kjos-Hanssen has answered the stated question but I think it would help to make a few clarifying comments.
Let BWQ denote the statement, "Every bounded infinite sequence from $\mathbb Q$ has an ...

- 67.1k

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 ...

- 14.7k

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 ...

- 3,370

12
votes

### "Family Tree" of Theorems

The idea of "dependencies" is somewhat ill-defined. The Reverse Mathematics Program has one way of defining dependencies by comparing the theorems over a very weak base theory called RCA0. To see nice ...

- 42.5k

11
votes

### Reverse mathematics of (co)homology?

Have any reverse mathematicians taken a look at sheaf cohomology as a subject to be "deconstructed"?
Colin McLarty has made a study of what it takes to define derived functor cohomology (with sheaf ...

- 31.5k

11
votes

Accepted

### Can noncomputable sets be distinguishable in $RCA_0$?

Yes.
Claim. There is a noncomputable $\Delta^0_2$ set $X$ which is distinguishable from every set it computes.
To ensure distinguishability, we must create a machine $\Phi$ such that for every ...

- 2,204

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 ...

- 156

11
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 ...

- 20.3k

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\...

- 4,208

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\...

- 40.3k

10
votes

### What is the reverse mathematical strength of the fundamental theorem of algebra?

It is perhaps instructive to see how Todd's proof of the FTA steps outside of $\mathsf{RCA}_0$ and how it could be modified to fit into $\mathsf{RCA}_0$.
First, let's review some aspects of ...

- 42.5k

10
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 ...

- 26.7k

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 ...

- 14.7k

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)&...

- 1,596

9
votes

Accepted

### What can be achieved by liberalizing induction for $RCA_0$?

One answer is trivially "Yes" - fix some first-order sentence $\varphi$ which is provable from $X\Sigma_n$ but not $RCA_0$ alone and consider the formula $$\psi(x)\equiv (\varphi \vee \neg(x\in 0'))$$ ...

- 20.3k

9
votes

Accepted

### Comprehension axiom who 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 ...

- 20.3k

8
votes

### Consistency strength needed for applied mathematics

Edited 3/10/2017
Very large cardinals around the rank-into-rank area potentially have applications in cryptography. Rank-into-rank cardinals produce self-distributive algebras which may be used as ...

- 23.8k

Only top scored, non community-wiki answers of a minimum length are eligible

#### Related Tags

reverse-math × 137lo.logic × 108

computability-theory × 32

proof-theory × 25

theories-of-arithmetic × 20

reference-request × 16

set-theory × 14

constructive-mathematics × 12

model-theory × 9

descriptive-set-theory × 6

foundations × 6

soft-question × 5

nt.number-theory × 4

co.combinatorics × 4

real-analysis × 4

computational-complexity × 4

axiom-of-choice × 4

nonstandard-analysis × 4

metamathematics × 4

gn.general-topology × 3

large-cardinals × 3

mathematical-philosophy × 3

ordinal-analysis × 3

ac.commutative-algebra × 2

forcing × 2