Talk:Reverse mathematics

ExpertContribution

{{ExpertContribution|Gro-Tsen (David Madore), CBM and some others. I thank them. Boris Tsirelson (talk) 20:52, 18 October 2008 (UTC)}}

Criticizing the move to second-order arithmetic

See the discussion page there. (Just mentioning it here for reference.) --Gro-Tsen 00:35, 7 February 2006 (UTC)

Changes on 2006-3-20

See my comment in the discussion under second-order arithmetic --CMummert 02:10, 20 March 2006 (UTC)

Saving a phrase

I moved this from the main page. I don't think it should be deleted, so I am putting it here until I can work it back into the article.

For example, while usual (forward) mathematics is done in 
the language of set theory and in the system of  
Zermelo-Fraenkel set theory with the axiom of choice 
(which, unless the contrary is explicitly stated, is assumed 
to be the foundation system taken for granted by working
mathematicians), this system is really much stronger than is necessary.  

CMummert 15:39, 28 June 2006 (UTC)

Does RCA₀ stand for Recursive Comprehension?

I am a mathematician, but not at all expert in logic. After seeing "...than recursive comprehension can..." under the title "Additional systems" I was puzzled. A minute after I'he guessed that "recursive comprehension" and "RCA₀" are probably the same. But still, should we replace the title "The base system" with "The base system: recursive comprehension" (or something like that)? Boris Tsirelson (talk) 18:59, 20 September 2008 (UTC)

Yes, RCA stands for "recursive comprehension axiom", and the 0 indicates that the subsystem only includes induction axioms for Σ^0_1 formulas. Similarly, ACA stands for "arithmetical comprehension axiom". I added the explanation of RCA to the article. Please feel free to edit the articles yourself, as well. — Carl (CBM · talk) 18:55, 21 September 2008 (UTC)

Thank you! It is definitely better than what I would do myself. I guessed that the last A means "arithmetic", and had no guess about the 0.Boris Tsirelson (talk) 19:34, 21 September 2008 (UTC)

Jordan curve theorem

I added the Jordan curve theorem to the list of WKL0-equivalent statements, based on a mention and citation that I found in the Jordan curve theorem article. I hope this was correct. 69.228.171.150 (talk) 16:05, 22 October 2009 (UTC)

Yes, it's correct to add it here. Thanks for noticing it. — Carl (CBM · talk) 16:10, 22 October 2009 (UTC)

I guess my concern was over whether the statement needed to be qualified in some way. I'll leave that part to you, if there is any issue. 69.228.171.150 (talk) 16:15, 22 October 2009 (UTC)

redirect

I changed the redirect for Weak König's lemma to point to a section of this article instead of to second-order arithmetic. It may have been left from before the article forked. Was that right? If yes, then there are a bunch of other such redirects that I can also change. 69.228.171.150 (talk) 17:04, 22 October 2009 (UTC)

I think you are right; the other article doesn't even mention the lemma. — Carl (CBM · talk) 18:59, 22 October 2009 (UTC)

elementary arithmetic

http://www.andrew.cmu.edu/user/avigad/Papers/elementary.pdf may be useful for this article. 69.228.171.150 (talk) 14:48, 24 October 2009 (UTC)

That paper doesn't seem to be about reverse mathematics per se. Of course Avigad has done a lot of work in reverse mathematics as well.

One main difference between that topic and the reverse math program is that in reverse mathematics one is generally interested in $\Pi _{2}^{1}$ theorems of mathematics (or theorems higher in the analytical hierarchy). That particular paper by Avigad is talking about arithmetical theorems.

A second difference is that the topic of that paper is mainly formalization of proofs within elementary arithmetic. The reverse mathematics program is not concerned with formalization alone, but with precise determination of the axioms necessary. So, on its own, a result that such-and-such theorem is provable in some system is not a reverse mathematics result. Such formalization results are of interest, they just aren't reverse mathematics.

There may be a tenuous relationship between the topic of that paper and reverse mathematics, but I think it would be too tenuous to try to include in an encyclopedia article. — Carl (CBM · talk) 01:57, 25 October 2009 (UTC)

Oh that is interesting. I had never caught on that reverse mathematics is primarily about non-arithmetical statements. That seems worth mentioning in its own right. I think there should be some coverage in wikipedia of the power of these weak subsystems of PA for proving arithmetic statements, but I guess this article isn't the place for that. Thanks. 69.228.171.150 (talk) 03:06, 25 October 2009 (UTC)

I do think that the article here should have a section on reverse mathematics over weaker systems than RCA₀, although it should be a later section in the article. Right now there is just one paragraph under "Additional sections", which could be expanded some. Actually, this whole article could be expanded a lot, along with the articles on subsystems of PA, such as PRA and elementary arithmetic. — Carl (CBM · talk) 11:50, 25 October 2009 (UTC)

That would be great, though I'm thinking of even weaker systems than that, like bounded arithmetic and predicative arithmetic. These show up in complexity theory among other places, but possibly not in analysis. 69.228.171.150 (talk) 08:40, 31 October 2009 (UTC)

You'll have to watch out for terminology there; most reverse math people think of ACA as a "predicative" theory. More precisely, ACA is "predicative given the natural numbers", but everyone just says "predicative". So E. Nelson's book is not about that.

Here is my impression of the status of reverse mathematics over extremely weak subsystems: (1) Everyone thinks it could be done, in principle. (2) Nobody in the mathematical logic computability community has actually done very much with it. I do know of a few publications in the area, though (some are even mentioned in Simpson's book).

Your questions here have inspired me to expand this article some. Right now, it is essentially a "50 minute introduction" to reverse math, in the sense that it has about enough content for a 50 minute talk. Over time, I'll try to expand it to a "3 hour introduction". I do not agree with people who think every detail, no matter how trivial, should be in an encyclopedia article; some things should only be alluded to here, or just left to the references. But there is enough reasonable material to fill out the article some. — Carl (CBM · talk) 12:59, 31 October 2009 (UTC)

Thanks for the expansion! I've been learning a lot from your articles. Yes, I understand that Nelson's idea of predicativity is much more restrictive than (e.g.) Feferman's. It's still pretty interesting from a foundational perspective, and its applicability to complexity theory is potentially important. Predicative recursion in Nelson's sense gives a syntactic characterization of PTIME functions--I've been wanting to read Bellantoni's dissertation [1] about this. Of course the complexity topic does get away from reverse mathematics. 69.228.171.150 (talk) 22:04, 31 October 2009 (UTC)

Oh neat, I just found this. 69.228.171.150 (talk) 06:28, 1 November 2009 (UTC)

There are also some slides by Steve Cook:[2] 71.141.88.54 (talk) 01:29, 3 March 2011 (UTC)

WKL0 and ZF

The article says

In a sense, weak König's lemma is a form of the axiom of choice (although, as stated, it can be proven in classical Zermelo-Fraenkel set theory without the axiom of choice).

This is somewhat confusing; the WKL0 section also says that WKL0 proves the Hahn-Banach theorem, yet it's well known that ZF doesn't prove Hahn-Banach. I'll see if I can figure out the explanation, but a bit more exposition would help. 69.228.171.150 (talk) 07:10, 28 October 2009 (UTC)

WKL0 proves the Hahn-Banach theorem for separable Banach spaces. ZF does prove this; it's the Hahn-Banach theorem for arbitrary spaces that is not provable in ZF. The same also goes, mutatis mutandis, for many consequences of WKLO, including:

1. Gödel's completeness theorem (for a countable language).
2. Every countable commutative ring has a prime ideal.

These are special cases of principles that are not provable in ZF, however the countability assumption makes the special cases provable in ZF. Without the countability assumption the statements are not even expressible in second-order arithmetic, so the issue of provability is vacuous.

More generally, since ZF proves that the standard model of second-order arithmetic is a model of Z₂, ZF proves everything about the natural numbers and sets thereof that is provable in Z₂. — Carl (CBM · talk) 10:19, 28 October 2009 (UTC)

I added this to the article. — Carl (CBM · talk) 10:55, 28 October 2009 (UTC)

"is the need to use restrict general mathematical theorems" — really so? "to restrict"? "to use restricted"? Boris Tsirelson (talk) 16:22, 28 October 2009 (UTC)

Thanks, that was an extra word. "Another effect of using second-order arithmetic is the need to restrict general mathematical theorems to forms that can be expressed within arithmetic." — Carl (CBM · talk) 17:13, 28 October 2009 (UTC)

Thanks, the new addition helps. 69.228.171.150 (talk) 09:52, 31 October 2009 (UTC)

induction and subscript

Adding a note about the subscript 0 is a good idea. The only thing that's tricky is the usual definitions make it hard to give a one-line summary of what's going on. I think that the regular editors here, like R.e.b., are aware of this, but for other people, here's a summary of the situation.

RCAo has the $\Sigma _{1}^{0}$ induction scheme, which happens to have the particular "second order induction axiom"

$[0\in A\land (\forall n)(n\in A\to n+1\in A)]\to (\forall n)(n\in A).$

For systems ACAo and stronger, that one axiom would be enough, since those systems have sufficient comprehension to construct the sets for which induction proofs are used. For RCAo, the whole scheme of $\Sigma _{1}^{0}$ induction is needed, because only $\Delta _{1}^{0}$ comprehension is included, and we regularly prove things about properly $\Sigma _{1}^{0}$ sets by induction. — Carl (CBM · talk) 11:18, 20 October 2010 (UTC)

Theorems into coffee

Is that quote from Rényi verified? He died in 1970, before reverse mathematics was invented according to the article. I have also heard a category-theoretic version of the same saying: a comathematician is a machine for turning cotheorems into ffee. A cotheorem is of course something one deduces from a rollary. 71.141.88.54 (talk) 10:50, 14 February 2011 (UTC)

I'm sure it was a joke. It was added by a non-logged-in editor from Cambridge [3]. — Carl (CBM · talk) 12:46, 14 February 2011 (UTC)

RCA0 as a constructive system

To this extent, RCA0 is a constructive system, although it does not meet the requirements of the program of constructivism because it is a theory in classical logic including the excluded middle.

There may be a confusion here, because the fact that the system is constructive does depend on the fact that the system is defined on classical or intuitionistic logic; you may extract from a classical proof a constructive one if every definable object is computable. This is a standard technique in logical systems, so either this is possible and the remark is unjustified, or it would deserve some further explanation.

--W1r3d2 (talk) 12:15, 25 April 2012 (UTC)

"Constructive" has many different meanings. The sentence and precedig one seem to be very clear about exactly what is being claimed: that RCAo is constructive in the sense that any set of numbers that can be proved to exist is computable. — Carl (CBM · talk) 13:05, 25 April 2012 (UTC)

I agree with User:Wlr3d2. What "does not meet the requirements of the program of constructivism" about applying excluded middle to *computable* sets? I have changed it to just "To this extent, RCA0 is a constructive system." --David-Sarah Hopwood ⚥ (talk) 03:22, 5 July 2012 (UTC)

RCA_0 has the law of excluded middle for all formulas, not just the recursive ones. As such, it is clearly not a constructive theory in the usual technical sense of the word. The fact that one may extract constructive proofs from nonconstructive ones under some restrictions has nothing to do with it, and anyway the same is true for a wide variety of much stronger classical theories.

Keep in mind the following. If $\phi$ is a formula of arbitrarily high complexity, RCA_0 proves that there exists a number n such that $(\phi \land n=0)\lor (\neg \phi \land n=1)$. (If you insist on making it a set, the theory proves there exists an X such that $\forall n\,[n\in X\to (\phi \land n=0)\lor (\neg \phi \land n=1)]\land \exists n\,(n\in X)$.) There is no way to make this proof constructive. Note that the defined object here is indeed computable (it is a constant, or a finite set), but this is not provable constructively, so W1r3d2’s original claim is highly misleading, if not outright wrong.—Emil J. 11:02, 5 July 2012 (UTC)

I stand corrected. The original statement didn't make that at all clear, though. Perhaps the point you make here can be added to the article; I think it's worth it and would clear up a potential misconception. --David-Sarah Hopwood ⚥ (talk) 23:45, 7 July 2012 (UTC)

Is not Gödel's first incompleteness theorem states the impossibility of this task?

Gödel's first_incompleteness_theorem — Preceding unsigned comment added by Константин Конь (talk • contribs) 13:34, 19 December 2019 (UTC)

Which task do you mean? Boris Tsirelson (talk) 16:35, 19 December 2019 (UTC)

Ah, maybe I understand; you mean that we cannot prove that a given theorem cannot be proven without a given axiom, since maybe the remaining axioms are contradictory... True. But really we prove something else: that the given axiom follows from the given theorem (and the remaining axioms). Usually it is believable (though not provable in the given system; but often provable in a reasonable stronger system) that the given axiom is not superfluous (that is, does not follow from the remaining axioms); assuming this we get the "impossible task". Boris Tsirelson (talk) 17:07, 19 December 2019 (UTC)

I mean the task of reversing mathematics. There will always be true statements that can not be proved (thus, not theoremes). Constantine^hehe 07:41, 1 January 2020 (UTC)

I'm not sure your conclusion follows from Gödel's first incompleteness theorem. The theorem says that in a system containing arithmetic, there exists a statement which can be neither proved nor disproved. That is, ${\textstyle S\nvdash \phi \land S\nvdash \neg \phi }$. But although we know there is an unprovable statement $\phi$, we can't be sure that there is such an unprovable statement which is actually true, i.e. one where all models of S satisfy $\phi$, $S\models \phi$. The conditions of the incompleteness theorem would be met if there was a $\phi$ such that there were models of S where it holds and other models where it does not. FrankP (talk) 17:17, 1 January 2020 (UTC)

@Константин Конь If your question is about how reverse mathematics deals with true unprovable statements, the fact that Godel's first incompleteness theorem holds is the reason why the subject holds up. If a weak theory like RCA₀ was complete, even proving statements we know have high strength like Cantor-Bendixson theorem and Robertson-Seymour theorem, reverse mathematics wouldn't do much as RCA₀ would be enough of an assumption for any theorem. (We would still be able to ask if over a weaker still base theory, from assuming the theorem we can derive RCA₀, but then we have no need for the Big Five and by RCA₀'s completeness there is no need for most of the subject.)

@Boris Tsirelson Not only that, but often the proof the axiom is not superfluous is done in a weak theory like RCA₀, like in Subsystems of Second-order Arithmetic. C7XWiki (talk) 06:56, 23 August 2022 (UTC)

Ulm's theorem

Should Ulm's theorem be included under ATR_0? The formulation in the article Ulm's theorem looks like the statement in Simpson's theorem V.7.1, which is provable in RCA_0. After proving theorem V.7.1, Simpson says that the logical strength to reach ATR_0 is in asserting that the Ulm extensions exist, and instead theorem V.7.3 is the equivalence with ATR_0. Usually a theorem stated like "for any gizmos G, H, their widgets are equivalent" will include the assertion "the widgets of G and H exist" in its statement, as it is formulated as $\forall (G,H\in \mathrm {Gizmos} )\exists W,Z(W,Z{\text{ are widgets of }}G,H\land W\equiv Z)$, however Ulm's theorem appears to be "for all gizmos G, H, if their widgets are equivalent, then ...", with existence of widgets before the conditional. C7XWiki (talk) 18:16, 5 June 2024 (UTC)