Talk:Peano axioms

Archives: 1, 2

Successor

Currently Successor function redirects here, yet its definition is deep in the middle of a section and rather brief. I feel this might not be enough explination for the layman to follow, and it could do with a little expansion. It might also be worth considering reverting Successor function back to a non redirect version. --Salix alba (talk) 16:31, 23 March 2007 (UTC)

Axiom 9

Axiom 9 is a little ambiguous about what K can be. Is it OK for K to contain numbers other than the naturals? --Salix alba (talk) 16:35, 23 March 2007 (UTC)

Sure; K can contain lots of other sets. The axiom is phrased that way because Peano phrased it that way. In the modern context of ZF, you could start with a set K and then use a separation axiom to extract the set of natural numbers in K, so it would be natural to restrict the axiom to sets that only contain natural numbers. But Peano was doing this in 1889 well before axiomatic set theory; the word set in axiom 9 should be read in a natural-language way. CMummert · talk 17:12, 23 March 2007 (UTC)

Peano arithmetic

This sections is lacking in historical info, who first formalised it in this way? The text quotes Kaye 1991, but mathworld has two references with the name before that date:[1]

• Kirby, L. and Paris, J. "Accessible Independence Results for Peano Arithmetic." Bull. London Math. Soc. 14, 285-293, 1982.
• Paris, J. and Harrington, L. "A Mathematical Incompleteness in Peano Arithmetic." In Handbook of Mathematical Logic (Ed. J. Barwise). Amsterdam, Netherlands: North-Holland, pp. 1133-1142, 1977.

I found that the formula

1. $\forall x,y,z((x+y)+z=x+(y+z))$

might need a little typesetting. It took a second reading to realise that z was not a fuction. --Salix alba (talk) 19:21, 23 March 2007 (UTC)

The idea that addition and multiplication of naturals can be obtained from just successor dates back to at least 1920 (Skolem, "Foundations of elementary arithmetic"). The idea of expressing arithmetic as a first-order rather than second-order theory was certainly known in the 1930s and probably before; it was a subject of interest because the Lowenheim-Skolem theorem had just been proved and its meaning was not yet understood. Kaye (1991) is just used as a contemporary standard reference; the subject of first-order arithmetic is extremely classical. You're right that the article would benefit from a paragraph on this. CMummert · talk 19:57, 23 March 2007 (UTC)

Logical symbols ⊆ mathematical symbols

"Peano's paper employs a logical symbolism and maintains a clear distinction between mathematical and logical symbols (...)."

I think that logical symbols are mathematical symbols. Should it be "clear distinction between arithmetical and logical symbols"? Jayme 02:13, 21 April 2007 (UTC)

The way things are ordinarily conceived in mathematical logic today, logical symbols such as $\forall$ and $\exists$ (and often including $=$) are not considered "mathematical" per se. Symbols that go beyond the basic logical symbols are considered "mathematical" because they are used to develop mathematical theories using the logic as a starting point. Your viewpoint would be correct if all of logic was commonly viewed as a subfield of mathematics, but it isn't, and the distinction between the two is particularly important for mathematical logic. CMummert · talk 02:21, 21 April 2007 (UTC)

transfinite induction

I believe the addition:

The axiom excludes well-ordered sets of order type larger than ω. The more general transfinite induction requires a "limit case" property.

to be confusing and incorrect. Complete induction, although not quite correctly defined there, could also be used. For example, replacing:

$\forall {\bar {y}}(\phi (0,{\bar {y}})\land \forall x(\phi (x,{\bar {y}})\Rightarrow \phi (x+1,{\bar {y}}))\Rightarrow \forall x\phi (x,{\bar {y}}))$

by

$\forall {\bar {y}}(\forall x(\forall z(z<x\Rightarrow \phi (z,{\bar {y}}))\Rightarrow \phi (x,{\bar {y}}))\Rightarrow \forall x\phi (x,{\bar {y}}))$

may be an appropriate formalization of complete induction. — Arthur Rubin | (talk) 17:54, 18 July 2007 (UTC)

Perhaps my addition is not needed here. However, it is not clear what you try to say, what is wrong?--Patrick 09:51, 19 July 2007 (UTC)

I thought it was just out of place; the induction axiom also excludes various non-well-ordered models. The second sentence mentions transfinite induction, which I don't think is relevant to Peano arithmetic. — Carl (CBM · talk) 13:01, 19 July 2007 (UTC)

Category-theoretic vs. Categorical

I changed this sec-head b/c 'categorical' means something different (as in having only one model up to isomorphism) and this is one of those areas where this meaning might be the intended/expected. I, for one, came to that section expecting to find a discussion of the categoricity (or non-categoricity) of various formulations of the Peano postulates. Zero sharp 20:48, 10 September 2007 (UTC)

Rewrite

Let me say I fully support Kaustuv's rewrite of the article. It removes a great deal of accumulated redundancy and makes the article more accessible. — Carl (CBM · talk) 13:24, 13 September 2007 (UTC)

I'm afraid I fully oppose it. It uses set-theoretic terminology when the simpler logical terminology will do, and logical terminology where set-theoretic terminology is needed. My reason for reverting it turns out to be incorrect, but the full version of the induction axiom was moved to somewhere I didn't expect to see it. There are probably more things that I disagree with, and some I agree with, but those are the problems that first came to mind. — Arthur Rubin | (talk) 14:36, 13 September 2007 (UTC)

Certainly Kaustuv version isn't perfect, but I think it's a good step forward. I was planning to edit various parts once Kaustuv hd it in place. I'd like to switch back to Kaustuv's version, and I'll be glad to fix problems and address concerns raised here about it. Would that be acceptable? — Carl (CBM · talk) 15:01, 13 September 2007 (UTC)

OK, the structure is better in Kastuv's versions, but the facts are wrong, in some cases subtly. In addition to what I noted, formal mathematics should link to model theory rather than formal systems, where we place what is essentially proof theory. I'm not sure we should place form over substance. — Arthur Rubin | (talk) 15:15, 13 September 2007 (UTC)

We should not place form over substance, but in this case I think the only way to achieve both is to start with a better form and then correct the substance. I significantly edited this page in January to correct various problems with the content [2] , but I didn't pay enough attention to the form. I don't mind working on the new version to fix any problems with the content that might be introduced. I was planning to give the article a detailed copyedit once Kaustuv had finished his edits this morning. — Carl (CBM · talk) 15:26, 13 September 2007 (UTC)

OK, I've reverted my reversion, but I'll keep an eye on the article, as well. Another problem I have is with the form of the axiom. The "current" version of axiom 7 reads:

For every m, n ∈ N, if S(m) = S(n), then m = n.

I think it should either be:

For all natural numbers m and n, if S(m) = S(n), then m = n,

or the logical form

$(\forall m)(\forall n)(S(m)=S(n)\rightarrow m=n)$

or

$(\forall m\in \mathrm {N} )(\forall n\in \mathrm {N} )(S(m)=S(n)\rightarrow m=n)$,

The mixed logical/natural language forms bother me. — Arthur Rubin | (talk) 16:05, 13 September 2007 (UTC)

(←) I did some editing this afternoon. I sympathize with Arthur Rubin about the wording of the axioms; the previous version [3] shows a format I would vouch for. I am a little concerned with the unhistorical presentation of the axioms, because I don't want the article to claim things about the original 9 axioms that are more recent changes. In particular, the order of the axioms in the previous version is the order Peano presented them in, but the current version of the article has a different order. — Carl (CBM · talk) 18:03, 13 September 2007 (UTC)

I was afraid of strong negative reactions, which is why I didn't commit my rewrite in May. I just want to say that I don't care about this article at all really, so I am not going to argue for my version. Good luck. — Kaustuv Chaudhuri 19:52, 13 September 2007 (UTC)

On further reflection, I agree with Arthur's point above that the emphasis on set theory is unnecessary. I certainly am no fan of set theory; whenever I need to recall the Peano axioms and their standard properties that are listed in every logic textbook, I re-derive them from the only fact I have committed to memory: that nnos are initial in 1→X→X diagrams. I have changed the statements of the axioms to use a judgemental formulation (that is, using the "is a natural number" judgement). — Kaustuv Chaudhuri 04:24, 16 September 2007 (UTC)

Heyting arithmetic needs work

That stub should be expanded and there should be some sort of comparison made with PA with regard to realizability and various completness/independence results. Not sure what goes where and how much of it is on WP already as sub- or strangely named articles. Just a note for any interested persons. — Kaustuv Chaudhuri 19:10, 29 November 2007 (UTC)

Section Models:Nonstandard Models

This section is just wrong about categoricity. First-order PA has many nonstandard models within any particular model of ZFC, and second-order PA has one ('standard') model (up to isomorphism) within each ('standard' or not) model of ZFC. That is what categoricity means. You can't even define the same kind of an isomorphism between models in different set theories as you can between models in the same set theory.

It even contradicts the paragraph directly above.

Xplat (talk) 06:31, 11 December 2007 (UTC)

You're right that that second paragraph got reworded sometime so that instead of saying that each model of set theory has a model of PA that it believes to be standard, it just said each model of set theory has one model of PA. I reworded that paragraph, using the "smallest" model as a stand-in for the standard model because I think that is clearer. On the other hand, it is perfectly possible, working in ZFC, to define an isomorphism between two models of set theory, or between sets in different models of set theory. ZFC is not different from any other first-order theory in that respect. I don't think that the article talks about isomorphisms between different models of set theory, though, and probably shouldn't. — Carl (CBM · talk) 14:36, 11 December 2007 (UTC)

Heh, guess I wasn't quite clear when I said "you can't define the same kind of an isomorphism". What I meant was that an isomorphism between two internal structures in different internal models of ZFC is defined differently than an isomorphism between two structures considered as living directly in an instance of ZFC serving as the host theory of your model theory. The difference is one of detail more than principle, of course, but it's still significant. You can have things happen like two sets with the same elements having different powersets, for instance, which can't happen when working in a single model of ZFC.

In any case, that was a side issue; your edit addressed my concerns excellently.

Xplat (talk) 18:29, 11 December 2007 (UTC)

The paragraph before Carl's edit was confusing because of its context, not so much its content. When discussing categoricity of second-order PA interpreted in second-order logic, it's an unnecessary complication to bring up models of ZFC. What categoricity means is that (up to isomorphism), only one such model exists, period, Platonistically if you like.

You don't gain anything by relativizing to a model of ZFC. If you're a realist about models of ZFC, then you might as well be a realist, period, because models of ZFC can be compared level-by-level to see which one is missing subsets it ought to have, and therefore which one is wrong. If you're not willing to be a realist, period, then you might as well stop talking about models too (except as linguistic metaphors/mental images/convenient figures of speech/what have you). --Trovatore (talk) 18:37, 11 December 2007 (UTC)

So, does the "right" model of ZFC satisfy GCH or not?

If you actually take a look at the categoricity theorem for PA₂, there are two major steps to the argument: (1) all minimal models of PA₂ are isomorphic and (2) all models of PA₂ are minimal. ("Minimal" here means that the domain of first-order quantifiers contains only elements with numerals.) The first step itself divides into (1a) any two minimal models have a one-to-one relation on their domains of individuals that preserves 0 and S, (1b) administrivia extending this to a full isomorphism including any other predefined function or relation symbols in the theory, and (1c) the implicit assumption that the one-to-one relation on the domains of individuals will automatically extend to one between the domains of properties of individuals. This depends on a choice of the semantics of second-order logic, and for some choices it is untrue. For the standard semantics, it is true, but the standard semantics implicitly depends on a choice of some sort of set theory to ground the notion of 'arbitrary subsets of the domain'.

The step (1a) is another point where hidden assumptions come in. Under any metatheory, any reasonable variant of arithmetic will prove inequalities between any two numerals that are not identical, and this lets the proof carry through. However, one's metatheory may actually admit numerals with a nonstandard number of applications of S! This shows that although under any given metatheory, minimal models of PA₂ are isomorphic, what counts as a "minimal" model is metatheory-relative.

Step (2) again depends on your semantics for second-order logic, in both of the above ways. If you don't use the standard semantics of SOL, your semantics need to be strong enough to allow the property 'has every inductive property' to be defined. Furthermore, they need to imply a strong enough relationship between the domains of first-order and second-order variables that the statement 'every number has every inductive property' is actually equivalent to the metatheoretical statement 'every number has a numeral' for the proof to go through. On top of that, even once the proof has gone through, you still have the same ambiguity as in (1a) which only gives you one isomorphism class of models per metatheory.

Truly, I am not willing to be a realist, full stop, or even about models of ZFC. I don't believe there's a "True Arithmetic" actually Out There that is negation-complete, or a canonical set of natural numbers, or a canonical tabulation of halting Turing machines (which are actually all the same thing). Nonetheless model theory has its uses. But we might be getting off topic here...

Xplat (talk) 08:12, 15 December 2007 (UTC)

Look, it's fine that you're not a realist and you still want to think about model theory. That describes lots of people. But models either exist or they don't. If they exist then the levels of the von Neumann hierarchy exist and are unique up to unique isomorphisms, GCH is either really true or really false even if we don't know which, etc. If they don't exist then your statements about models have the same status as any mathematical statements referencing objects you presumably don't believe in either. So either way the claim that the full second-order Peano Axioms are categorical is a true statement of mathematics, period, no qualification needed. How you interpret that statement does depend on your foundational philosophy, but not whether you accept the statement itself.

If you don't believe in models as real objects, then the claim that there are different models of ZFC, having different (possibly non-isomorphic) candidates for the canonical model of second-order PA, must be interpreted however you personally go about interpreting claims containing terms (such as "model") that do not denote real objects. But whatever interpretation that is, it will also work for the claim that second-order PA is categorical in second-order logic.

By the way, you seem to be conflating models with theories in the above, particularly when you speak of "only one isomorphism class of models per metatheory". It's not "per methatheory" but rather "per model of the methatheory". It is very important to keep this distinction straight, whether you're a realist or not -- mixing the two things up can easily lead you to outright, unambiguous mathematical errors, not just philosophical errors. --Trovatore (talk) 21:25, 15 December 2007 (UTC)

Induction Axiom vs Induction Schema

The article claims the induction axiom is 2nd order and the induction schema is 1st order. But the way in which the two are stated reads almost identically, if one ignores the superfluous y vector. If there's a distinction here its a very fine one which ought to be made clearer Houseofwealth (talk)

Addition

In the section on Arithmetic, regarding + and x, the article states "The respective functions and relations are constructed in second-order logic" But then further down the article states "The arithmetical operations of addition and multiplication and the order relation can also be defined using first-orer axioms." This appears contradictory to me. If it isn't, it would be nice to make the distinction clearer. Houseofwealth (talk)