Talk:Second-order arithmetic

Bizzare Summary in Wikipedia App

In the wikipedia app for Android the article headline says:

Second-order arithmetic

unseen energy

The second line is displayed in grey, the way sub-titles usually are. But where on earth does "unseen energy" come from?! It seems to be automatically generated? I cannot find any internal tags that would be responsible for this strange summary.

--Vkuncak (talk) 19:00, 15 October 2020 (UTC)

It's the short description, imported from Wikidata because there was no local short description. I've added a local short description so should be fine now; I'll go and correct the Wikidata one too. --Trovatore (talk) 19:20, 15 October 2020 (UTC)

Criticizing the move from reverse mathematics

(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 second-order 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 second-order 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. --Gro-Tsen 00:32, 7 February 2006 (UTC)

Changes as of 2006-3-20

Please excuse any mistakes I have made in formatting, as I am new to wikipedia.

I have thoroughly edited reverse mathematics and second-order 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:

1. Arithmetical comprehension is an axiom scheme, but it doesn't include the basic axioms or any induction
2. ACA_0 is arithmetical comprehension, arithmetical induction, and the base axioms
3. 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 hold-out.

--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₀ (rather than just the axiom) and so on: basically that's because I'm of the old-fashioned school which believes that any interesting mathematical theorem should be expressible in English without any formalism whatsoever (i.e., no "kay-double-u-ell-zero"); 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 "kay-double-u-ell-zero" 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.) --Gro-Tsen 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 second-order semantics that are important to the general study of second-order arithemtic but not to reverse math. In my changes to the second-order 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 English-only phrase for WKL_0 is “The subsystem (of second-order 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

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 first-person phrasing (we define ...) to make the tone encyclopedic.

Are there any serious objections to this? CMummert 16:00, 28 June 2006 (UTC)

Induction axiom

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 $(P\rightarrow (Q\rightarrow R))\leftrightarrow ((P\land Q)\rightarrow R)$, and $P\rightarrow Q\rightarrow R$ means $P\rightarrow (Q\rightarrow R)$ in some circles, so the axioms were stated correctly. The version with only $\rightarrow$ avoids some parentheses. But I changed the article to the more usual version that uses $\land$ for clarity. CMummert 20:00, 16 November 2006 (UTC)

Oooh, I see. I've been reading $P\rightarrow Q\rightarrow R$ as shorthand for $(P\rightarrow Q)\land (Q\rightarrow R)$, resulting in quite a bit of head-scratching. (In some other math articles too, I think. Will check.) HFuruseth 16:40, 20 November 2006 (UTC)

categoricity

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 two-sorted 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 non-arithmetic formulas? That seems too good to be true. It raises hope that tossing a few more axioms into ZFC about some non-set 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 two-sorted first-order logic is like any other first-order theory subject to the incompleteness theorems. The exact same collection of axioms, interepreted in second-order 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 natural-number variables range, and one over which the set-of-natural-numbers 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 natural-number 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 sets-of-naturals 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 number-variable 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)

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 difference between

CPA - Peano arithmetic in second-order logic

PA2 - A first-order 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

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

says $\forall X$, in that model of PA2 the quantifier only ranges over $P$. In second-order logic (CPA), the universal set quantifier by definition ranges over all subsets of N. That's why the only model of the second-order 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.

A concrete way of getting nonstandard models of PA2 is to use the compactness theorem of first-order logic. Second-order 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 second-order logic - not even all the tautologies of second-order logic are provable, much less all the logical consequences of an arbitrary theory.

You might start by reading second-order logic, which describes the semantics and why they are different than first-order 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 second-order 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)

Goodstein's theorem

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 ε₀ and for second-order 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 ε₀ 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 ε₀. The problem is that PA has ordinal exactly ε₀, which means that PA supports transfinite induction on any ordinal less than ε₀ but not on ε₀ 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

I am a mathematician but not at all expert in logic. I was confused by the phrase: "A subsystem of second-order 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

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 second-order 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)

Arithmetical stronger than no quantifying over sets?

The article states just below the list of "basic" (i.e. first order ?) axioms:

That is, all variables range over the natural numbers and not sets thereof, a fact even stronger than their being arithmetical.

Emphasis mine.

What does this mean? How is that a stronger property than their being arithmetical? I thought that was precisely the definition of arithmetical. Earlier in the article (Under Definition#Syntax) we find

A formula with no bound set variables (that is, no quantifiers over set variables) is called arithmetical.

Which seems to say the same thing. Over at arithmetical hierarchy we find a similar definition: a arithmetical set is one whose formula is written in the language of first order with no set parameters.

So what does the first sentence quoted above mean? -lethe ^{talk +} 03:13, 7 December 2020 (UTC)

I'm niot an expert in higher-order logics, but my understanding of the sentence is this: an arithmetical formula is still allowed to have free set variables; the axioms, however, don't have set variables at all (apparently, "S", "+", "*", "=", and "<" are considered to be constants), neither free nor bound ones. - Jochen Burghardt (talk) 10:12, 7 December 2020 (UTC)