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


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


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


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


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


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


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.


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


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


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


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.


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


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


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


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!


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


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


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.


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


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