Non-Successor Element of Peano Structure is Unique

From ProofWiki
Jump to navigation Jump to search


Let $\struct {P, s, 0}$ be a Peano structure.


$P \setminus s \sqbrk P$ is a singleton


$\setminus$ denotes set difference
$s \sqbrk P$ denotes the image of the mapping $s$.

It follows that the non-successor element $0$ is the only element of $P$ with this property.


Let $T = P \setminus s \sqbrk P$.

From Axiom $(P4)$ we know that $T \ne \O$.

Now suppose that $t_1 \in T$ and $t_2 \in T$.

Aiming for a contradiction, suppose that $t_1 \ne t_2$.

Define $A = P \setminus \set {t_2}$.

Thus $t_1 \in A \ne P$.

Moreover, by the nature of $t_2$:

$x \in A \implies \map s x \in A$

Thus, by the induction axiom $(P5)$, $A = P$.

From this contradiction it follows that $P \setminus s \sqbrk P$ cannot contain two different elements.