Express least and greatest fixed point using predicate and quantifiers

Question

Let $f$ be a function from $\mathbb{N}$ to $\mathbb{N}$. A fixed point of $f$ is an element $x \in \mathbb{N}$ such that $f(x) = x$. A least fixed point of $f$ is the smallest number $x \in \mathbb{N}$ such that $f(x) = x$. A greatest fixed point of $f$ is the largest number $x \in \mathbb{N}$ such that $f(x) = x$.

1. Express using the language of predicate logic the English statement: “$f$ has a least fixed point”. You may use the predefined function $f$ as well as the predefined predicates $=$ and $<$.
2. Express using the language of predicate logic the English statement: “$f$ has a greatest fixed point”. You may use the predefined function $f$ as well as the predefined predicates $=$ and $<$.

My attempt for 1 is $\exists x \forall y (x < y \ \&\ f(x)=x)$. I am not sure how I would start 2 with only $<$ and $=$.

Answer 1

Look again. Your $\exists x\forall y(x < y \text{ and } f(x)=x)$ says: there is a number $x$ which is smaller than every number $y$ and which is a fixed point of $f$ ... which is not what you wanted at all!

(1) says that there is a fixed point for $f$ such that any other fixed point is larger than it. So as a half-way Loglish rendition you want

$(\exists x)(x \text{ is fixed point } \land (\forall y)(y \text{ is fixed point } \to y \text{ greater than or equal to } x))$

which then becomes

$(\exists x)(fx = x \land (\forall y)(fy = y \to (x = y \lor x <y))$

or equivalently (why?)

$(\exists x)(fx = x \land (\forall y)((fy = y \land \neg x = y) \to x <y))$

With that model to follow, now do (2) in two similar steps (remembering that a fixed point is the greatest one if no number bigger than it is a fixed point).