Talk:Secondorder arithmetic
WikiProject Mathematics  (Rated Bclass, Midimportance)  


Contents
Criticizing the move from reverse mathematics[edit]
(Preliminary remark: I wrote essentially all of the reverse mathematics article, including the section that was moved to form this new article.) While I agree that it is, at least in principle, a very good idea to split the article (something I should have done from the start), I think the way it was done is hasty at best, and a lot of things now don't make much sense. To start with, second order arithmetic is not a number of systems, it is one system, “classical analysis”, here described as “the full system”, and the others, which reverse mathematics studies, are merely subsystems of secondorder arithmetic. The content is the same, but the emphasis is entirely different. So the comments about “the base system” and “stronger systems” don't make much sense here: they should have remained in the article on reverse mathematics or, better, be rewritten in a more sensible way to account for the new setting. Conversely, the article on reverse mathematics should be updated to at least summarize what is said here: for example, recursive comprehension should be defined there, not here (though it may be mentioned in both), since one may know all there is to know about secondorder arithmetic without knowing what “recursive comprehension” means. And so on: I don't have the time to make the changes myself, unfortunately, so I hope the initiator of the split can do it. GroTsen 00:32, 7 February 2006 (UTC)
Changes as of 2006320[edit]
Please excuse any mistakes I have made in formatting, as I am new to wikipedia.
I have thoroughly edited reverse mathematics and secondorder arithmetic. I am very familiar with reverse math; I received my PhD with Simpson as my advisor. I tried to keep as much as I could, while removing things that were either false or disagreed with the terminology in the literature.
One key distinction, unspoken but observed in the literature:
 Arithmetical comprehension is an axiom scheme, but it doesn't include the basic axioms or any induction
 ACA_0 is arithmetical comprehension, arithmetical induction, and the base axioms
 ACA is ACA_0 plus full induction (this was studied in the 1960s and 1970s until they realized ACA_0 is more amenable). Some authors, however, use ACA as an abbreviation for arithmetical comprehension axiom, meaning the arithemtical comprehension scheme.
You can say that a theorem is equivalent to ACA_0 over RCA_0, or to arithmetical comprehension over RCA_0, because these are equivalent statements. But it doesn't match the terminology in the literature to say that RCA_0 is the same as recursive comprehension or that the subsystem ACA_0 is called arithmetical comprehension
A more subtle point is that it is going out of fashion to use the word recursive in mathematical logic; the word computable is usually used except in fixed abbreviations like r.e., DNR, or RCA. In particular, almost the entire community of computability theorists now use the term computable instead of recursive. Simpson is holdout.
CMummert 02:08, 20 March 2006 (UTC)
 That's all right, I wrote the article initially, but mathematical logic is not at all my domain (I'm in algebraic geometry and number theory), so in case you disagree with what I wrote you are obviously the one who's right, and I'm sorry if I made any bad mistakes (I just glanced over the diff, so I don't know). I also plead guilty for the metonymy of using the term "Weak König's Lemma" to designate the whole system KWL_{0} (rather than just the axiom) and so on: basically that's because I'm of the oldfashioned school which believes that any interesting mathematical theorem should be expressible in English without any formalism whatsoever (i.e., no "kaydoubleuellzero"); if that's not the case in reverse mathematics, it is most unfortunate, but there's nothing I (or even you) can do about it. :) (But if there is some standard English phrase which can be used rather than "kaydoubleuellzero" to refer to the system, please mention it. Also, I would be mildly of the opinion of letting the English names stand for the section titles, unless you think even that is abhorrent.) GroTsen 22:04, 20 March 2006 (UTC)
 There weren't any really false statements. Simpson's book has a narrow focus and so doesn't mention things like secondorder semantics that are important to the general study of secondorder arithemtic but not to reverse math. In my changes to the secondorder arithmetic page, I tried to give it a broader viewpoint than just reverse math. Over on the reverse math page, I have now changed the section titles back to English, which is indeed more attractive. I also added a paragraph explaining the difference between WKL_0 and weak Konig's lemma. The Englishonly phrase for WKL_0 is “The subsystem (of secondorder arithmetic) consisting of Delta^0_1 comprehension, Sigma^0_1 induction, the base axioms, and weak Konig's lemma” which is why everybody uses the abbreviation. I would appreciate any changes you would like to make to make the exposition clearer for nonlogicans; my motivation in editing the pages at all is to have some sort of accessible introduction online. When a nonlogican hears the term reverse mathematics and looks it up on wikipedia, I would like the page to be informative and understandable. CMummert 02:55, 21 March 2006 (UTC)
Planned style changes[edit]
I plan to make the following changes to improve the exposition:
 Consistently refer to first order variables as number variables and second order variables as set variables.
 Remove firstperson phrasing (we define ...) to make the tone encyclopedic.
Are there any serious objections to this? CMummert 16:00, 28 June 2006 (UTC)
Induction axiom[edit]
Looks like the first arrow in the induction axiom should be "and". (I don't have time to play with the mathematical wikinotation now, so I'm leaving it alone.) HFuruseth 19:37, 16 November 2006 (UTC)
 Well, it is a tautology that , and means in some circles, so the axioms were stated correctly. The version with only avoids some parentheses. But I changed the article to the more usual version that uses for clarity. CMummert 20:00, 16 November 2006 (UTC)
 Oooh, I see. I've been reading as shorthand for , resulting in quite a bit of headscratching. (In some other math articles too, I think. Will check.) HFuruseth 16:40, 20 November 2006 (UTC)
categoricity[edit]
I'm just a clueless dweeb so please help me out, I'm confused. I wonder if someone could expand the article to say something about how PA2 (the twosorted first order system described in the article) compares with "CPA" (the classical Peano axioms with the induction axiom stated in second order logic, dunno if that's the standard notation). In particular what happens to CPA's categoricity? CPA is supposed to have just one model (up to isomorphism). But Gödel's incompleteness theorem says there are sentences φ in PA2 that are true in some models but false in others, i.e. there are models of PA2 that are not isomorphic. And yet, as the PA2 axioms are written, it looks like you can turn any CPA proof into a PA2 proof (am I missing something)?. Can it be that all the undecidable formulas of PA2 are nonarithmetic formulas? That seems too good to be true. It raises hope that tossing a few more axioms into ZFC about some nonset entities turns set theory decidable, which seems unlikely. —Preceding unsigned comment added by 75.62.4.229 (talk • contribs) 03:02, 30 October 2007
 Well, it's too something to be true; I don't know if the word is "good". PA2 neither proves nor (presumably) refutes its own consistency, which is an arithmetic proposition. The difference is not the theory but the logic. PA2 interpreted in twosorted firstorder logic is like any other firstorder theory subject to the incompleteness theorems. The exact same collection of axioms, interepreted in secondorder logic, becomes categorical (that's your CPA). Trovatore 03:07, 30 October 2007 (UTC)
 This is what I mean, I'm having trouble understanding what the difference is. CPA (i.e. 2nd order logic) has only one sort of object (i.e. natural numbers), but you can quantify over sets of them. PA2 also lets you quantify over sets of natural numbers, by inserting them into the universe as first order objects. So how is it that you don't get the same models, at least as far as arithmetic statements are concerned? What happens if you try to transfer the CPA categoricity proof to PA2? Thanks. —Preceding unsigned comment added by 75.62.4.229 (talk) 03:44, 30 October 2007 (UTC)
 A model of PA2 has two universes, one over which the naturalnumber variables range, and one over which the setofnaturalnumbers variables range. A sentence is interpeted in the usual Tarskian manner using these two universes.
 On the other hand, a model of your CPA has only one universe, for the naturalnumber variables, and the set variables are interpreted as ranging over subsets of that.
 In a model of PA2 where the first universe contains nonstandard naturals, the universe for the setsofnaturals will necessarily fail to contain some subset of the first universe. Trovatore 04:00, 30 October 2007 (UTC)
 I'm sorry to be dense (maybe it sounds like I know more about this stuff than I do) but do you understand what my confusion is? I hadn't realized PA2 had two universes, as opposed to one universe where the objects all have little labels stuck to them saying either "number" or "set"is that different? I'm having trouble understanding how there can be such a thing as nonstandard naturals in the numbervariable part of PA2. (By Tarskian interpretation do you just mean "S is true iff S is true in every model"?). Let's say we have some arithmetic formula (maybe the twin primes conjecture) that's undecidable over ZFC. It's still either true or false in N (the unique model of CPA). Can it somehow be true in CPA but false in some model of PA2? What difference between PA2 and CPA lets such a thing happen? It can't merely be the allowability of quantification over sets of naturals in CPA, since PA2 can also do that. I also missed earlier what you were getting at about consistency, but it occurs to me, are you saying that CPA asserts its own consistency (I can believe that, but I hadn't realized it)? I guess it could do that since it's a finite axiomatization which PA2 is not. But I'd expect PA2 could assert CPA's consistency the same way? Again I'm having trouble understanding how PA2 numbers can be different from CPA numbers. —Preceding unsigned comment added by 75.62.4.229 (talk) 04:15, 30 October 2007 (UTC)
 This is what I mean, I'm having trouble understanding what the difference is. CPA (i.e. 2nd order logic) has only one sort of object (i.e. natural numbers), but you can quantify over sets of them. PA2 also lets you quantify over sets of natural numbers, by inserting them into the universe as first order objects. So how is it that you don't get the same models, at least as far as arithmetic statements are concerned? What happens if you try to transfer the CPA categoricity proof to PA2? Thanks. —Preceding unsigned comment added by 75.62.4.229 (talk) 03:44, 30 October 2007 (UTC)
 The version with the little labels is not any different; you can think of it that way if you like. I don't have time to answer the other questions at the moment. Maybe tomorrow, or maybe someone else will pick it up. Trovatore 04:25, 30 October 2007 (UTC)
 Thanks, I don't want to take up more of your time. If you can suggest some further reading for me that would be appreciated. I've spent some head scratching over this article and related ones but I'm still not getting it. —Preceding unsigned comment added by 75.62.4.229 (talk) 04:29, 30 October 2007 (UTC)
 The version with the little labels is not any different; you can think of it that way if you like. I don't have time to answer the other questions at the moment. Maybe tomorrow, or maybe someone else will pick it up. Trovatore 04:25, 30 October 2007 (UTC)
 (←)The difference between
 CPA  Peano arithmetic in secondorder logic
 PA2  A firstorder theory of natural numbers and sets of natural numbers
 is the semantic meaning of the set quantifiers. In a model of PA2, there will be a particular collection of "natural numbers" N and a particular collection P of sets of those natural numbers, but some subsets of N may not be in P. When the induction axiom
 says , in that model of PA2 the quantifier only ranges over . In secondorder logic (CPA), the universal set quantifier by definition ranges over all subsets of N. That's why the only model of the secondorder theory is the standard model  because if there really was a subset of N that failed to be inductive, the set quantifier would capture that subset. Note that this is not a proof in CPA.
 (←)The difference between
 A concrete way of getting nonstandard models of PA2 is to use the compactness theorem of firstorder logic. Secondorder logic has no compactness theorem, and worse yet has no complete proof system. So it doesn't really make sense to talk about undecidable sentences in secondorder logic  not even all the tautologies of secondorder logic are provable, much less all the logical consequences of an arbitrary theory.
 You might start by reading secondorder logic, which describes the semantics and why they are different than firstorder semantics. — Carl (CBM · talk) 12:27, 30 October 2007 (UTC)
 Thanks, this gets more directly to what I was asking about. I'm going to have to keep trying to digest it. I liked the Vaananen article linked from secondorder logic and am going to have to read that again too. —Preceding unsigned comment added by 75.62.4.229 (talk) 16:40, 30 October 2007 (UTC)
 You might start by reading secondorder logic, which describes the semantics and why they are different than firstorder semantics. — Carl (CBM · talk) 12:27, 30 October 2007 (UTC)
Goodstein's theorem[edit]
Does anyone know if Goodstein's theorem (a theorem about integers, that is provable in set theory but unprovable in PA1) can be proven in PA2? Any idea if there's a reasonable "classical" proof of the theorem? By "classical" I mean no fancy set theory or ordinals, but it's ok to use calculus, complex analysis, etc. that are inaccessible to first order PA. By "reasonable" I mean something that looks like normal math (analytic number theory), not some kind of reverse construction based on deriving PA2 from the real number axioms. Thanks.
 The answer is that PA2 does prove Goodstein's theorem. Each formal theory of arithmetic has a "proof theoretic ordinal" which is the supremum of the order types of ordinal notations for which the system supports transfinite induction. For PA this ordinal is ε_{0} and for secondorder arithmetic it is very large (and has no name as far as I know; current research is still working on the ordinals of subsystems of PA2, not PA2 itself or stronger theories like ZF).
 Essentially, any theory with proof theoretic ordinal larger than ε_{0} will be able to prove Goodstein's theorem. This is because the ordinal assigned to each natural number in the proof of Goodstein's theorem is always less than ε_{0}. The problem is that PA has ordinal exactly ε_{0}, which means that PA supports transfinite induction on any ordinal less than ε_{0} but not on ε_{0} itself.
 I don't know of a proof of Goodstein's theorem that doesn't use ordinals; that would be interesting. — Carl (CBM · talk) 12:25, 2 November 2007 (UTC)
A silly misunderstanding[edit]
I am a mathematician but not at all expert in logic. I was confused by the phrase: "A subsystem of secondorder arithmetic L is a theory in the language of L whose axioms are theorems of L." just because is was not written "whose axioms are SOME theorems of L". After a minute I've understood, but still: should we add this "SOME" (or something like that)? Boris Tsirelson (talk) 18:48, 20 September 2008 (UTC)
 The entire lede could use improvement. I gave it a first pass. — Carl (CBM · talk) 19:09, 21 September 2008 (UTC)
 Nice; thank you.Boris Tsirelson (talk) 19:40, 21 September 2008 (UTC)
Unbound variable in Axiom 9[edit]
All of the other axioms have only bound variables, but Axiom 9 has the variable "n" unbound. I think this is an error and A9 should get an ∀n prepended, but maybe I'm missing something about the semantics of free variables in secondorder logic. JLM~enwiki (talk) 05:12, 3 January 2016 (UTC)
 I think it was just an oversight. Free variables in axioms work the same in first and second order logic, so leaving out the quantifier doesn't really make a difference  axioms are implicitly universally quantified  but for the sake of consistency I agree that we should include the quantifier in #9. I added it just now. Thanks for commenting on this, — Carl (CBM · talk) 15:35, 3 January 2016 (UTC)