Constructing a model of non-negative integers $\mathbb{N}$ I am attempting problem 3.43 of MIT's Discrete Mathematics text.

Let $\mathbf{\tilde0}$ be a constant symbol and next and prev be the successor ("+1") and predecessor("-1") total functions. The aim of this problem is to develop a series of predicate formulas using just the symbols $\mathbf{\tilde0}$, next and prev such that every model satisfying these formulas will contain a copy of the nonnegative integers  $\mathbb{N}$.
More precisely, the “copy” of $\mathbb{N}$ in a model will look like an infinite sequence of
distinct points starting with $e_0$ , with a next-arrow going from each point to the next point in the sequence so that next acts like plus one. We also want prev to act like minus one: whenever a next-arrow goes into an element e, then the prev-arrow out of e goes back to the beginning of the next-arrow.
Now prev($\mathbf{\tilde0}$) = $\mathbf{\tilde0}$, reflecting the convention
for nonnegative integers that subtracting from zero has no effect.
The predicate $$(1) \ \ \ \ \ \forall x.\ \mathbf{prev}(\mathbf{next}(x)) = x $$
formula (1) means that the prev-arrow out of any point $e$ goes back to the
beginning of any next-arrow into $e$. Of course this will not be possible if there is
more than one next-arrow into $e$.
There are some standard terms called numerals used to describe the elements
$e_0 , e_1...$ ; namely, the numeral for $e_0$ will be $\mathbf{\tilde0}$, and the numeral for $e_n$ will be the application n times of next to $\mathbf{\tilde0}$. For example, the numeral for three
would be:
$$\mathbf{\tilde3} = \mathbf{next(next(next(\tilde0)))}$$
(a) To make the interpretion $e_0$ of $\mathbf{\tilde0}$ behave like zero and to prevent formation of cycles in the model, write a predicate formula expressing the fact that the value of $\mathbf{\tilde0}$ is not plus-one of anything. Also, by convention, subtracting one from zero has no effect.
(b) Explain why two different numerals must have different values in any model
satisfying (1) and part (a).
It is worth seeing that the formula of part (a) together
with (1) do not ensure that their models consist solely of a copy of $\mathbb{N}$.
For example, a model might consist of two separate copies of $\mathbb{N}$.
(c) Write a formula such that any model has only one copy of $\mathbb{N}$, i.e. that there is only one zero-like element.
But the additional axiom of part (c) still leaves room for models that, besides
having a copy of $\mathbb{N}$, also have “extra stuff” with weird properties.
(d) Describe a model that satisfies the formula of part (c) along with (1), part (a)
and also satisfies
$$(d) \ \ \ \exists x. x = \mathbf{next(}x \mathbf{)} $$

I think the answer to part (a) is the predicate formula $$(a) \ \ \ \ \forall x. \mathbf{\tilde0} \neq \mathbf{next(}x \mathbf{)}$$
For part(b), if two different numerals $m, n$ had the same values in the model then, assuming $m>n$, that would imply that
$$(b) \ \ \ \underbrace{\mathbf{next \circ next\ \circ \ ... \ \circ \ next}}_{m-n\text{ times}}(\mathbf{\tilde0}) = \mathbf{\tilde0}.$$
which is false.
For part(c), to ensure only one zero-like element
$$(c) \ \ \ \mathbf {prev(}x\mathbf{)} = x \implies x = \mathbf{\tilde0}$$
I am having trouble with parts (b) and (d).
For (b) is my argument circular reasoning since I am assuming ordering of numerals? The text also mentions well-ordering property but I can't deduce how that would be applicable here.
Also for (d), if I assume $z$ such that $\mathbf{next(}z \mathbf{)} = z$, then from (1) and (c), $z = \mathbf{\tilde0}.$ which is false since (a). So what is the "weird-stuff" which can satisfy (1), (a), (c) and (d)?
My background is single-variable calculus and the first three chapters of the mentioned text.
 A: *

*Part (a) asks for two things.  You have only provided the first of the two.  You have not addressed "Also, by convention, subtracting one from zero has no effect."


*For part (b), you might benefit from introducing some notation.  For instance $\mathbf{next}^3(\mathbf{\tilde{0}}) = \mathbf{\tilde{3}}$.  Notice that the problem does not deny the existence of a $\Bbb{N}$ that you can use for this notation and to count applications of $\mathbf{next}$.  In fact, you are extracting properties from this $\Bbb{N}$ in an attempt to make a model of it, so it must exist and be available for use.  You also know that $\mathbf{next}$ is a well-defined function, so
$$ \mathbf{next}^{m-n} \circ \mathbf{next}^n(\mathbf{\tilde{0}}) = \mathbf{next}^m(0)$$
Additionally, you are given "whenever a next-arrow goes into an element $e$, then the prev-arrow out of $e$ goes back to the beginning of the next-arrow".  This says $\forall e. \mathbf{prev}(\mathbf{next}(e)) = e$.  Applying $\mathbf{prev}$ $n$-times to $\mathbf{next}^m(\mathbf{\tilde{0}}) = \mathbf{next}^n(\mathbf{\tilde{0}})$ yields $\mathbf{next}^{m-n}(\mathbf{\tilde{0}}) = \mathbf{\tilde{0}}$.  Since you have assumed $m > n$, you may write $\mathbf{next}(\mathbf{next}^{m-n-1}(\mathbf{\tilde{0}})) = \mathbf{\tilde{0}}$, using the convention that $\mathbf{next}^0$ is the identity function, to immediately get a contradiction to your statement in part (a) (by setting $x = \mathbf{next}^{m-n-1}(\mathbf{\tilde{0}})$).


*In part (c), you need the part you haven't supplied to part (a).  You have a way to characterize $\mathbf{\tilde{0}}$ and you want to ensure that there is only one element in your model that has that property.


*Well, a thing that would not violate the list of properties is an element $\mathbf{\tilde{\infty}}$ with the properties

*

*$\mathbf{next}(\mathbf{\tilde{\infty}}) \neq \mathbf{\tilde{\infty}}$.  You say this violates (1) and (c), but those both require an application of $\mathbf{prev}$, which is not present here.

*$\mathbf{prev}(\mathbf{\tilde{\infty}}) \neq \mathbf{\tilde{\infty}}$.  Informally, we are allowing ... $\infty + 2$, $\infty + 1$, $\infty$, $\infty - 1$, $\infty -2$, ... to be "extra stuff" in this model.
We've already ensured there is only one starting place for a sequence of points in the $\mathbf{next}$ direction, but we have not ensured there are no extra starting places for sequences of points in both directions.

The descending half of such bidirectional sequences need not be lower bounded.  If one is lower bounded, we have enforced that if its lower bound is $b$, satisfying, for some choice of $k \in \Bbb{N}$, $\mathbf{prev}^k(\mathbf{\tilde{\infty}}) = \mathbf{\tilde{b}}$ and $\mathbf{prev}(\mathbf{\tilde{b}}) = \mathbf{\tilde{b}}$, then it must be the case that $b = \mathbf{\tilde{0}}$.  (We have no requirement of the general shape $\mathbf{next} \circ \mathbf{prev}(x) = x$, so $\mathbf{\tilde{0}}$ is free to be the lower bound of any number of such sequences -- we descend from the chain to $\mathbf{\tilde{0}}$ then ascend to $\mathbf{\tilde{1}}$.)
For this specific type of problem, there is some opportunity for graphical help.  Suppose that we decide that numerals increase to the right, so except for self-loops any $\mathbf{next}$ arrow must point in the right half-space of its source and except for self-loops any $\mathbf{prev}$ arrow must point in the left half-space of its source.  Then, attending first to $\mathbf{next}$, we can have a fan-in of multiple points whose $\mathbf{next}$ is the point $e$ (only two are shown in the "fan", but there can be many more).  Two edges are dashed because either, but not both, can be present at any point.

Likewise, $\mathbf{prev}$ can fan-in and then proceed along the $\mathbf{prev}$ chain from $e$.

Then our various predicates cut down the number of options at each point.
(1) says "if you follow the red arrow from $e$ and the blue arrow from where you now are, you arrive back at $e$.  So either, there is an $f \neq e$ such that $\mathbf{next}(e) = f$ and $\mathbf{prev}(f) = e$, or $\mathbf{next}(e) = \mathbf{prev}(e) = e$.
Then we pick a distinguished point, labelled "$\mathbf{\tilde{0}}$" and notice the $\mathbf{next}$ chain starting from $\mathbf{\tilde{0}}$ could be a model of $\Bbb{N}$.  Then $\mathbf{\tilde{0}}$ is required to have no incoming red arrows.  So the red diagram around $\mathbf{\tilde{0}}$ has one arrow: $\mathbf{next}(\mathbf{\tilde{0}}) = \mathbf{\tilde{0}}$ or $\mathbf{next}(\mathbf{\tilde{0}}) \neq \mathbf{\tilde{0}}$.  Your answer to part (a) eliminates the first case, so there is a $\mathbf{next}$ chain starting at $\mathbf{\tilde{0}}$ (containing at least two distinct points: $\mathbf{\tilde{0}}$ and $\mathbf{next}(\mathbf{\tilde{0}})$).
Notice that we have made no restrictions affecting the blue diagram to reject or allow similar "starting points" for chains in the $\mathbf{prev}$ direction.  We get sort of close with the $\mathbf{prev}(\mathbf{next}(x))$ constraint, but this just says that for the points in the red fan-in of $e$, there is a distinguished one that is the target of hte blue arrow from e -- the real constraint here is that $\mathbf{prev}(e)$ is required to be one of the points having $e$ as its $\mathbf{next}$ (and not some other point that does not have $e$ as its $\mathbf{next}$).
By the time we get to part (d), we have that there are numerals, that the successor of a numeral, $n$, is not $n$, and that every point, whether a numeral or not has a successor.  (This last bit is part (d).)  So, at least the chain of numerals starting at $\mathbf{\tilde{0}}$ gives a model of $\Bbb{N}$, but there could be non-numerals.  A non-numeral point, $e$, ...

*

*... has a $\mathbf{prev}$ and $\mathbf{prev}(e) \neq e$.  The $\mathbf{prev}$ of $e$ can be a numeral, even $\mathbf{\tilde{0}}$.


*can be its own $\mathbf{next}$.  Nothing has prevented red self-loops.


*could belong to a cyclic chain.  The minimal example of this is: let $f$ be a non-numeral point with $e \neq f$.  Then set \begin{align*}
\mathbf{next}(e) &= f  \text{,}  \\
\mathbf{next}(f) &= e  \text{,}  \\
\mathbf{prev}(e) &= f  \text{, and}  \\
\mathbf{prev}(f) &= e  \text{.}
\end{align*}
That is, there can be more "weird stuff" than just chains descending from upper fixed points.
Notice that this set of arrows cannot be implemented using our convention for arrows going to the right or left.  Go back and re-read the setup for that : we made that choice to follow the model of $\Bbb{N}$ given by the numeral points.  We are talking about non-numeral points, so these arrows need not follow that convention.
