15
[25C]Vale questo risultato
\[ ∀ y∈ℕ, y≠ ∅⇒ ∃ x∈ℕ , S(x)=y \]
questo può essere dimostrato per induzione, come in [1YP], o mostrando che se
\[ ∃ y∈ℕ, y≠ ∅∧ ∀ x∈ℕ , S(x)≠ y \]
allora \(ℕ ⧵ \{ y\} \) sarebbe un insieme S-saturo più piccolo di \(ℕ\), una contraddizione. In particolare da [1YM] si ottiene che la funzione successore
\[ S:ℕ → ℕ⧵\{ 0\} \]
è bigettiva.
Se \(n\neq 0\) chiameremo \(S^{-1}(n)\) il predecessore di \(n\).