Axiom talk:Peano's Axioms
Approach
I have some time to devote to this, seeing as I need some timeout from the PropLog section. Some not very subtle people have commented on the suboptimal state of this page in the past.
The most pressing issue is the treatment of $s: P \to P$. It's an intrinsic part of the Peano axioms, so it should be mentioned before the axioms are stated. This is in accord with Howson's (brief-as-always) treatment. This will probably have numerous ramifications for pages referring here, so it'll be a nice task.
The other part consists of the extra two sections about "Peano Structures" and the fact that Peano defines $\N$.
My draft to resolve the issues is below. Comments appreciated. We could think about using the version including $0$ instead, seeing as it is somewhat more insightful, particularly for $P4$. It also makes mentioning $0$ on the page that much easier. — Lord_Farin (talk) 14:43, 9 April 2014 (UTC)
- Good job.
- I am also a supporter of the $0$-based approach, as this is more modern, and makes the transition between it and the "natural ordered semigroup" approach so muc easier. However, it's worth at least a mention of the fact that there does exist a $1$-based approach.
- I wonder whether it might be worth raising a separate (sub)-page for each axiom, thereby giving us the room to digress about such details while keeping the main page clean and streamlined. --prime mover (talk) 16:54, 9 April 2014 (UTC)
- Well, there should in general only be two options: the current form and the below. Because the formulation of e.g. $P4$ depends quite heavily on the other three, it seems better to simply have two pages: with and without the named element (whether we call it $0$ or $1$ is immaterial). — Lord_Farin (talk) 17:03, 9 April 2014 (UTC)
Peano's Axioms are a set of properties which can be used to serve as a basis for logical deduction of the properties of the natural numbers.
Given a set $P$ and a mapping $s: P \to P$, the following four statements form Peano's Axioms:
| \((P1)\) | $:$ | \(\ds P \ne \varnothing \) | $P$ is not empty | ||||||
| \((P2)\) | $:$ | \(\ds \forall m, n \in P:\) | \(\ds s \left({m}\right) = s \left({n}\right) \implies m = n \) | $s$ is injective | |||||
| \((P3)\) | $:$ | \(\ds \operatorname{Im} \left({s}\right) \ne P \) | $s$ is not surjective | ||||||
| \((P4)\) | $:$ | \(\ds \forall A \subseteq P:\) | \(\ds \left({\left({\exists x \in A: \neg \exists y \in P: x = s \left({y}\right)}\right) \land
\left({\forall z \in A: s \left({z}\right) \in A}\right)}\right) \implies A = P \)
|
Principle of induction |
Subpage defining $s$ as the successor mapping, and $s(n)$ as the successor of $n$. Probably can be Definition:Successor Mapping, though I personally think that page should be updated and made a subpage of this one.
Subpage "Peano structure". One-line transclusion.
Having shortened the on-page treatment, the "Peano defines uniquely" section can be disposed of in favour of a simple Also see entry.