84

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 without having a proof of either conjecture, so this is a meaningful situation. Of course, it will (hopefully) later become trivial, when we prove or disprove the ...

answered Oct 23 '17 at 19:37

Noah Schweber

29.5k44 gold badges7777 silver badges216216 bronze badges

66

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 mathematics isn't necessarily the end of the story.
The Wikipedia entry on Sperner's lemma says (as of this writing):
In mathematics, Sperner's lemma is a ...

answered Oct 24 '17 at 3:00

Timothy Chow

58.5k1919 gold badges259259 silver badges441441 bronze badges

46

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 the theory of reverse mathematics. An enormous number of the theorems of classical mathematics are now included in the reverse mathematical hierarchy, and ...

answered Sep 8 '16 at 22:51

Joel David Hamkins

191k3333 gold badges584584 silver badges10321032 bronze badges

43

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 true in the same situations. For example:
Observe that the fundamental theorem of algebra is equivalent to $0 = 0$, but in a trivial sense since they are ...

answered Oct 23 '17 at 22:17

Qiaochu Yuan

105k3232 gold badges377377 silver badges669669 bronze badges

37

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, the theorem is that given any graph on the set of natural numbers contains an infinite clique or an infinite anticlique. This is an infinitary theorem since the ...

answered May 27 '16 at 0:06

34

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 unprovable in the absence of A. Folks who study reverse mathematics make it their job to track dependencies of this type. Proof assistants such as Coq also ...

answered Sep 8 '16 at 20:45

Timothy Chow

58.5k1919 gold badges259259 silver badges441441 bronze badges

26

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 fundamental theorem of algebra as well as quantifier elimination for the theory of real closed fields.
So the FTA is weaker than BW.

answered Jun 30 '15 at 1:35

Bjørn Kjos-Hanssen

23.3k33 gold badges4747 silver badges107107 bronze badges

22

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: Horizons of Truth (Cambridge University Press, 2011).
There are a a couple of reasons why one might wonder whether the proof of FLT can be formalized in PA.
The ...

answered Feb 16 '18 at 2:45

Timothy Chow

58.5k1919 gold badges259259 silver badges441441 bronze badges

21

Before I attempt to address your specific questions, let me give a thought provoking non-answer:
Reverse mathematics is impossible (and irrelevant) in HoTT!
This is because HoTT fully supports proof-relevant mathematics, so when you refer to a theorem you necessarily refer to a proof of that theorem. The question whether the hypotheses are necessary ...

answered Jul 10 '13 at 2:39

21

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 visualizing the tag graph using d3.js. Of course the scope of the project is limited to algebraic geometry and related topics, and I'm not sure whether or not ...

answered Sep 8 '16 at 18:12

Paul Siegel

26.5k1515 gold badges118118 silver badges188188 bronze badges

18

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):
(Image from MathBabe blog.)
And here's a link to a larger image.

answered Sep 9 '16 at 0:56

Joseph O'Rourke

141k2626 gold badges298298 silver badges839839 bronze badges

18

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 be computably bounded.
So $f$ may not "exist" in your model. (Even though the model knows that for each $\sigma$ such an $n$ exists.)
However $ACA_0$ is ...

answered Nov 1 '19 at 21:44

Bjørn Kjos-Hanssen

23.3k33 gold badges4747 silver badges107107 bronze badges

17

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 be essential in a proof of simple first-order statements like for instance the twin prime conjecture, that have a $\Pi^0_3$ form:
$$
(\forall n)(\exists p>n)(...

answered May 27 '16 at 0:04

Bjørn Kjos-Hanssen

23.3k33 gold badges4747 silver badges107107 bronze badges

15

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 infinite Cauchy subsequence." What Friedman has shown is not that BWQ implies Con(PA). (I've gotten confused on this point myself in the past.) Instead, ...

answered Jun 30 '15 at 15:20

Timothy Chow

58.5k1919 gold badges259259 silver badges441441 bronze badges

15

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 upper bounds for the Hales–Jewett function $HJ(m,n)$, and therefore for the van der Waerden function $W(m,n)$. This was originally shown in a paper of Shelah: ...

15

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 has impacted the reverse mathematics (RM) program, and what its significance is seen as. Could path integrals really require such powerful axioms?
First of all, ...

13

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 most one ai is nonzero, the following holds: either a2i = 0 for all i, or a2i+1 = 0 for all i, where a2i and a2i+1 are entries with even and odd index ...

12

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 diagrams stemming from this program, check out the Reverse Mathematics Zoo!

answered Jun 9 '15 at 17:08

11

BISH famously includes the full axiom of choice scheme (in the functional language of second-order arithmetic), which is utterly weak in that context but very strong when combined with the law of the excluded middle. This is precisely the context in which Bishop wrote that the axiom of choice follows from "the very meaning of existence".
Thus there are ...

11

It is provable in RCA0 that if $K$ is a finite Galois extension of $F$ with Galois group $G$ then $H^1(G,L^\times)$ is trivial (every cocycle $a:G \to L^\times$ is a coboundary).
The finite Galois theory in RCA0 was discussed by Friedman, Simpson and Smith in Countable algebra and set existence axioms [APAL 25 (1983), 141–181; MR0725732]. The ...

answered Jul 18 '13 at 13:08

11

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 functional $\Psi_e$ with $\Psi_e^X$ total and $\Psi_e^X \neq X$, there is a pair $(\sigma, \tau)$ with $\sigma \prec X$, $\tau = \Psi_e^\sigma$, $\tau \neq \sigma$, $...

11

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 proving", Logical Methods in Computer Science, Volume 13, Issue 4, doi:10.23638/LMCS-13(4:10)2017, arXiv:1704.01930
In Section 2.4 they show the following. Let $...

11

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 want at least to interpret $PRA$). That said, once we get to reasonably strong theories (basically anything above $\Pi^1_2$-$CA_0$) we don't know how to ...

answered Mar 21 '20 at 19:19

Noah Schweber

29.5k44 gold badges7777 silver badges216216 bronze badges

11

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\textsf{-Ind}$ over $\mathsf{RCA}_0^{\star}$. Here $\mathsf{RCA}_0^{\star}$ is $\mathsf{EA}+\Delta^0_1\text{-}\mathsf{CA}+\Delta^0_0\text{-}\mathsf{Ind}$ and $\...

10

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 cohomology as a special case given a topos of sheaves). He finds that finite-order arithmetic (the union of $Z_n$ for $n=1,2,\ldots$) suffices
The large ...

10

This fits in the program of reverse mathematics. For instance: a subtree of the set of all finite binary strings has an infinite path iff it is infinite. One direction is provable in RCA $_0$ and the other is not.

answered May 17 '14 at 20:52

Bjørn Kjos-Hanssen

23.3k33 gold badges4747 silver badges107107 bronze badges

10

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 compactness in subsystems of second-order arithmetic.
Totally bounded complete metric spaces can be formalized in $\mathsf{RCA}_0$ and it is straightforward to show in $...

answered Jul 1 '15 at 11:28

10

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 the logical strength, and it's not the same as the number of steps. What it means is more like "how much time would it take for an undergrad/grad/expert to ...

10

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 self-embedding theorem, which states that if $(M,\cal{X})$ is a countable nonstandard model of $WKL_0$, then $(M,\cal{X})$ is isomorphic to a proper initial ...

10

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)>\frac{1}{n}]$
(ii) The Fan Theorem FT
This was already proved in Julian, W.H., and Richman, F., 1984, “A uniformly continuous function on [0, 1] that is ...

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

#### Related Tags

reverse-math × 129lo.logic × 103

computability-theory × 30

proof-theory × 24

theories-of-arithmetic × 19

set-theory × 14

reference-request × 13

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

axiom-of-choice × 4

nonstandard-analysis × 4

metamathematics × 4

gn.general-topology × 3

computational-complexity × 3

large-cardinals × 3

mathematical-philosophy × 3

ordinal-analysis × 3

ac.commutative-algebra × 2

forcing × 2