In Whitehead & Russell's PM, does every Series contain a $P_1$ (immedeately precedes)?

Question

✳204.7 $\vdash: P \in Ser .\supset. P_1 \in 1 \rightarrow 1$

Which says if $P$ is a series, then $P_1$ is one-one.

---

✳201.63 $\vdash: P \in trans \cap Rl‘J .\supset. P_1 = P \overset{.}{-}P^2$

Which says if $P$ is transitive and asymetrical, then $P_1=P\overset{.}{-}P^2$

---

Where

$P_1$ is "immediately precedes" as defined in ✳121.02 :

✳121.02 $P_v = \hat{x} \hat{y}\{ N_0c‘P(x|-|y)=v+_c1 \}$ Df where $v=1$

and $P^2 = P|P$ as defined in ✳34.02

---

Let R be "less than confined to the real interval [0,1]," then R is transitive, asymmetrical and connected. Therefore, by definition, $R$ is a series. But there is no term in $R$'s field that immediately precedes any other terms. In other words, $R_1$ does not seem to exist. If I'm not mistaken, the premises of 204.7 should include $\overset{.}{\exists}!P_1$ as a hypothesis.

Answer 1

If I understood well the definition, it is trivial that in $[0,1]$ there is an element which precedes any other element : it is $0$.

But to say that for any element different from $0$ there is an immediate predecessor, we have to use something like the Well-ordering Theorem proved by Zermelo in 1904 (thus known to W&R at time of writing PM) using the Axiom of Choice (the Multiplicative Axiom in PM).

This theorem says that any set can be well-ordered, and so also $[0,1]$.

But the proof is non-constructive: thus it gives us no clue about the way of finding the immediate predecessor of (say) $1$.

Answer 2

Given a set $\mu$,

Let $Q=\hat{ \alpha}\hat{\beta}\{\alpha,\beta \in Cl_{ex}‘\mu.\beta \subset \alpha.\beta \neq \alpha \}$

Let $S \in \epsilon_\Delta‘Cl_{ex}‘\mu$

Let $R=\hat{\alpha}\hat{\beta}\{\alpha \in Cl_{ex}‘\mu.\beta=\alpha - \iota ‘S‘\alpha \}$

Then $Q_{R\mu}$ is $Q$ confined to the transfinite posterity of $\mu$, and $S^;Q_{R\mu}$ is Well-ordered over the field of $\mu$.

To construct $S^;Q_{R\mu}$, all we need is to construct a selector $S$ which selects one term out of each of $\mu$'s subclasses.